Matita
 | |
 Interfejs autorskiego rozwiązania Matita.
| |
| Deweloperzy | Zespół Matity |
|---|---|
| Pierwsze wydanie | 1999 |
| Napisane w | OCaml |
| System operacyjny | Linuks |
| Dostępne w | język angielski |
| Typ | Dowód twierdzenia |
| Licencja | GPL |
| Strona internetowa | http://matita.cs.unibo.it |
Matita jest asystentem eksperymentalnych dowodów w fazie opracowywania na Wydziale Informatyki Uniwersytetu Bolońskiego . Jest to narzędzie wspomagające opracowywanie formalnych dowodów we współpracy człowiek-maszyna, udostępniające środowisko programistyczne, w którym w naturalny sposób współistnieją formalne specyfikacje, wykonywalne algorytmy i automatycznie weryfikowalne certyfikaty poprawności.
Matita opiera się na systemie typów zależnych znanym jako Rachunek Konstrukcji (Ko)Indukcyjnych (pochodna Rachunku Konstrukcji ) i jest do pewnego stopnia kompatybilny z Coq .
Słowo „matita” oznacza po włosku „ołówek” (proste i rozpowszechnione narzędzie do edycji). Jest to stosunkowo mała i prosta aplikacja, której złożoność architektoniczna i programowa ma być opanowana przez studentów, zapewniając narzędzie szczególnie przydatne do testowania innowacyjnych pomysłów i rozwiązań. Matita przyjmuje tryb edycji oparty na taktyce; ( XML ) obiekty próbne są tworzone do przechowywania i wymiany.
Główne cechy
Zmienne egzystencjalne są natywne w Maticie, co pozwala na prostsze zarządzanie zależnymi celami.
Matita implementuje dwukierunkowy algorytm wnioskowania o typach , wykorzystujący zarówno typy wywnioskowane, jak i oczekiwane.
Siłę systemu wnioskowania o typach (refiner) dodatkowo zwiększa mechanizm podpowiedzi, który pomaga w syntezie unifikatorów w określonych przez użytkownika sytuacjach.
Matita obsługuje wyrafinowaną strategię ujednoznaczniania opartą na dialogu pomiędzy parserem a typecheckerem .
Na poziomie interaktywnym system realizuje małe krokowe wykonanie ustrukturyzowanej taktyki, co pozwala na znacznie lepsze zarządzanie rozwojem dowodu i naturalnie prowadzi do bardziej ustrukturyzowanych i czytelnych skryptów.
Aplikacje
Matita został zatrudniony w CerCo (Certified Complexity): Europejskim projekcie 7PR skupionym na opracowaniu formalnie zweryfikowanego, zachowującego złożoność kompilatora od dużego podzbioru języka C do asemblera mikroprocesora MCS -51 .
Dokumentacja
Samouczek Matita zapewnia pragmatyczne wprowadzenie do głównych funkcji interaktywnego programu do dowodzenia twierdzeń Matita, oferując przewodnik po zestawie nietrywialnych przykładów w dziedzinie specyfikacji i weryfikacji oprogramowania .
Zobacz też
- Korespondencja Curry – Howard
- Interaktywne dowodzenie twierdzeń
- Intuicjonistyczna teoria typów
- Lista asystentów dowodowych