Die Version 8.12 (die letzte verfĂŒgbare Minor-Version zum Zeitpunkt der Erstellung dieser Nachricht â 8.12.1) des interaktiven Beweiswerkzeugs Coq (Hahn) ist erschienen.
Coq enthĂ€lt eine Programmiersprache mit abhĂ€ngigen Typen Gallina (Huhn), die auf der Theorie des KonstruktionskalkĂŒls basiert.
Das Coq-System ermöglicht die Entwicklung sowohl computergestĂŒtzter, ĂŒberprĂŒfbarer Beweise als auch Programme zusammen mit einem Nachweis ĂŒber die Ăbereinstimmung mit den Spezifikationen.
In der neuen Version wurde die Standardbibliothek und die Dokumentation erheblich ĂŒberarbeitet, und es wurden mehrere Fehler behoben.
Quelle: linux.org.ru
