ACL2 - ACL2
 | |
| Paradygmat | Funkcjonalny , meta |
|---|---|
| Zaprojektowany przez | Robert S. Boyer , J Strother Moore i Matt Kaufmann |
| Deweloper | Matt Kaufmann i J Strother Moore |
| Po raz pierwszy pojawiły się | 1990 (dystrybucja ograniczona), 1996 (dystrybucja publiczna) |
| Wersja stabilna | 8.4 / Sierpień 2021
|
| Dyscyplina pisania | Dynamiczny |
| OS | Wieloplatformowy |
| Licencja | BSD |
| Stronie internetowej | www |
| Wpływem | |
| Lisp zwyczajny , Nqthm | |
ACL2 ("A Computational Logic for Applicative Common Lisp") to system oprogramowania składający się z języka programowania , rozszerzalnej teorii w logice pierwszego rzędu oraz zautomatyzowanego dowodzenia twierdzeń . ACL2 jest przeznaczony do obsługi automatycznego wnioskowania w indukcyjnych teoriach logicznych, głównie w celu weryfikacji oprogramowania i sprzętu . Język wejściowy i implementacja ACL2 są napisane w Common Lisp . ACL2 to darmowe i otwarte oprogramowanie .
Przegląd
Język programowania ACL2 jest aplikacyjną ( wolną od skutków ubocznych ) odmianą Common Lisp. ACL2 jest bez typu. Wszystkie acl2 funkcje są całkowite - to znaczy, każda funkcja odwzorowuje każdy obiekt w acl2 wszechświata do innego obiektu w jego wszechświecie.
Teoria baza acl2 za axiomatizes na semantykę swojego języka programowania i jego funkcji wbudowanych. Definicje użytkownika w języku programowania, które spełniają zasadę definicyjną, rozszerzają teorię w sposób, który zachowuje logiczną spójność teorii .
Rdzeń dowodzenia twierdzeń ACL2 opiera się na przepisaniu terminów , a rdzeń ten jest rozszerzalny w tym sensie, że odkryte przez użytkownika twierdzenia mogą być używane jako techniki dowodowe ad hoc dla kolejnych przypuszczeń .
ACL2 ma być „przemysłową siłą” wersją dowodzącego twierdzenia Boyera-Moore'a, NQTHM . W tym celu ACL2 ma wiele funkcji wspierających czystą inżynierię interesujących teorii matematycznych i obliczeniowych. ACL2 czerpie również wydajność z budowania na Common Lisp; na przykład tę samą specyfikację, która jest podstawą weryfikacji indukcyjnej, można skompilować i uruchomić natywnie .
W 2005 roku autorzy rodziny dowodów Boyer-Moore, do której należy ACL2, otrzymali nagrodę ACM Software System Award „za pionierskie i inżynierskie opracowanie najbardziej efektywnego dowodzenia twierdzeń (...) jako formalnego narzędzia metod weryfikacji sprzętu krytycznego dla bezpieczeństwa i oprogramowanie."
Dowody
ACL2 ma wiele zastosowań przemysłowych. W 1995 roku J Strother Moore , Matt Kaufmann i Tom Lynch użyli ACL2 do udowodnienia poprawności operacji dzielenia zmiennoprzecinkowego mikroprocesora AMD K5 w następstwie błędu Pentium FDIV . Strona interesujących aplikacji w dokumentacji ACL2 zawiera podsumowanie niektórych zastosowań systemu.
Do przemysłowych użytkowników ACL2 należą AMD, Arm, Centaur Technology, IBM, Intel, Oracle i Rockwell Collins.