Matita - Matita
 | |
 Autorizační rozhraní Matita proof. | |
| Vývojáři | Tým Matita |
|---|---|
| První vydání | 1999 |
| Napsáno | OCaml |
| Operační systém | GNU / Linux |
| K dispozici v | Angličtina |
| Typ | Věta dokazující |
| Licence | GPL |
| webová stránka | http://matita.cs.unibo.it |
Matita[1]je experimentální důkaz asistent ve vývoji na Počítačová věda Oddělení Boloňská univerzita. Jedná se o nástroj napomáhající rozvoji formálních důkazů pomocí spolupráce člověk-stroj, poskytující programovací prostředí, kde přirozeně existují formální specifikace, spustitelné algoritmy a automaticky ověřitelné certifikáty správnosti.
Matita je založena na a závislý typ Systém známý jako počet (Co) indukčních konstrukcí (derivace Počet konstrukcí ) a je do určité míry kompatibilní s Coq.
Slovo „matita“ znamená v italštině „tužka“ (jednoduchý a rozšířený nástroj pro úpravy). Je to přiměřeně malá a jednoduchá aplikace,[2] jejichž architektonická a softwarová složitost má být zvládnuta studenty, což poskytuje nástroj zvláště vhodný pro testování inovativních nápadů a řešení. Matita adoptuje a taktika - režim úprav na základě; (XML -kódované) se vyrábějí zkušební předměty pro skladování a výměnu.
Hlavní rysy
Existenční proměnné jsou v Matitě nativní, což umožňuje jednodušší správu závislých cílů.[3]
Matita implementuje obousměrně odvození typu algoritmus[4] využívající odvozené i očekávané typy.
Síla systému odvození typu (rafinér) je dále posílena mechanismem náznaků[5]který pomáhá při syntetizaci unifikátory v konkrétních situacích specifikovaných uživatelem.
Matita podporuje propracovanou strategii disambiguation[6] na základě dialogu mezi analyzátor a typecker.
Na interaktivní úrovni systém implementuje malý krok provedení strukturované taktiky[7]umožňuje mnohem lepší správu vývoje kontroly a přirozeně vede ke strukturovanějším a čitelnějším skriptům.
Aplikace
Matita byla zaměstnána v CerCo (Certifikovaná složitost): a 7. RP Evropský projekt zaměřený na vývoj formálně ověřeného kompilátoru zachovávajícího složitost z velké podskupiny C do asembleru MCS-51 mikroprocesor.
Dokumentace
Výukový program Matita[8] poskytuje pragmatický úvod do hlavních funkcí interaktivního testovacího teorému Matita a nabízí prohlídku s řadou netriviálních příkladů v oblasti specifikace a ověřování softwaru.
Viz také
Reference
- ^ Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi. „Poskytovatel interaktivní věty Matita“:CADE-23, LNCS 6803, 2011, s. 64-69.
- ^ Asperti, A .; Ricciotti, W .; Sacerdoti Coen, C .; Tassi, E. (2009). „Kompaktní jádro pro počet indukčních konstrukcí“. Sadhana. 34: 71–144. doi:10.1007 / s12046-009-0003-3.
- ^ Andrea Asperti, Wilmer Ricciotti, C Sacerdoti Coen, Enrico Tassi. „Nový typ taktiky“:Technická zpráva UBLCS-2009-14. Červen 2009.
- ^ Andrea Asperti, Wilmer Ricciotti, C Sacerdoti Coen, Enrico Tassi. „Algoritmus obousměrného upřesnění pro počet (Co) indukčních konstrukcí“Logické metody v informatice, V.8, n1
- ^ Andrea Asperti, Wilmer Ricciotti, C Sacerdoti Coen, Enrico Tassi. „Rady ve sjednocení“:LNCS V.5674, 2009, str. 84-98
- ^ Claudio Sacerdoti Coen, Stefano Zacchiroli „Efektivní nejednoznačná analýza matematických vzorců“LNCS V.3119, 2004, str. 347-362
- ^ Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli „Tinycals: Taktika krok za krokem“ENTCS V.174, č. 2, 2007, strany 125–142
- ^ Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen „Matita Tutorial“Journal of Formalized Reasoning, V.7, č. 2, 2014, strany 91-199