This is the translation. The original web-page (oryginalna strona): http://www.cs.utexas.edu/~moore/publications/acl2-books/car/index.html
Matt Kaufmann, Panagiotis Manolios, i J Strother Moore, Kluwer Academic Publishers, Czerwiec 2000 r. (ISBN 0-7923-7744-3)
- Opis
- Tabela Zawartość oraz fragmenty (PDF .2Mb) (PS .8Mb).
- Załączniki („Korzystanie z systemu acl2”, „Dodatkowe funkcje”), bibliografia, i indeks (pdf)
- Errata
- Rozwiązania Ćwiczeń
- Informacje o zamawianiu
Opis
Ta książka jest podręcznikiem wprowadzającym do rozumowania wspomaganego komputerowo. Może być stosowany na studiach licencjackich i wyższych dla inżynierów oprogramowania lub metod formalnych. Nadaje się również w połączeniu z innymi książkami na kursach z zakresu projektowania sprzętu, dyskretnej matematyki lub teorii, zwłaszcza kursów podkreślających formalizm, dyscyplinę lub wsparcie zmechanizowane. Jest również odpowiedni dla kursów dotyczących sztucznej inteligencji lub automatycznego rozumowania.
Obecne systemy sprzętowe i programowe są często bardzo skomplikowane, a tendencja jest coraz większa. Modelując systemy matematyczne, otrzymujemy modele, które możemy udowodnić, że zachowują się poprawnie. Aby jeszcze bardziej zwiększyć zaufanie do naszego rozumowania, które może być złożone, możemy użyć programu komputerowego do sprawdzenia naszych dowodów, a nawet do zautomatyzowania niektórych ich konstrukcji.
W tej książce prezentujemy:
- Praktyczny funkcjonalny język programowania ściśle powiązany z Common Lisp, który służy do definiowania funkcji (które mogą modelować systemy komputerowe) i do zapewniania o zdefiniowanych funkcjach.
- Logika formalna, w której zdefiniowane funkcje odpowiadają aksjomatom; logika jest pierwszego rzędu, obejmuje indukcję i pozwala nam udowodnić twierdzenia o funkcjach.
- Wspomagany komputerowo system wnioskowania ACL2, który obejmuje język programowania, logikę i mechaniczne wsparcie procesu sprawdzania.
Ta książka nauczy Cię, jak formalizować rzeczy, jak konstruować dowody i jak używać mechanicznego narzędzia do sprawdzania tych dowodów.
Używamy konkretny formalizm i konkretny mechanizacji nim, a mianowicie acl2, który jest swobodnie dostępny zgodnie z warunkami licencji BSD od Strony głównej ACL2. ACL2 został napisany przez Kaufmanna i Moore’a i jest następcą twierdzenia Boyera-Moore’a, Nqthm. (Bob Boyer również wniósł znaczny wczesny wkład do ACL2.) Strona główna ACL2 zawiera podręcznik online, który jest dużym dokumentem hipertekstowym przeznaczonym przede wszystkim dla użytkowników systemu. Ta książka jest definitywnym wprowadzeniem do ACL2 i jak z niej korzystać.
Ucząc stosowania zmechanizowanego formalizmu, skupiamy się na problemach obliczeniowych, z którymi zwykle boryka się ktoś, kto używa formalnych metod analizy sprzętu komputerowego lub oprogramowania.
ACL2 jest stosowany w przemyśle. Pamiętasz błąd Intel FDIV? Pierwszy Pentium [znak towarowy, Intel, Inc] nie mógł poprawnie podzielić liczb zmiennoprzecinkowych i naprawienie kosztowało podobno 500 milionów Intel. W tym czasie używaliśmy ACL2, aby sprawdzić, czy mikrokod podziału zmiennoprzecinkowego na konkurencyjnym mikroprocesorze AMD, AMD-K5, był poprawny. AMD wykorzystało ACL2 do zweryfikowania podstawowych operacji zmiennoprzecinkowych dla niedawno wydanego Athlona. [Uwaga: AMD, logo AMD i ich kombinacje, AMD-K5, AMD-K7 i AMD Athlon są znakami towarowymi Advanced Micro Devices, Inc.] Tom towarzysz przedstawia studium przypadku ściśle związane.
System ACL2 z powodzeniem zastosowano w projektach o znaczeniu komercyjnym, w tym w modelowaniu mikroprocesorowym, weryfikacji sprzętu, weryfikacji mikrokodu i weryfikacji oprogramowania. Ta książka zawiera metodologię formalnego modelowania systemów obliczeniowych i uzasadnienia tych modeli ze zmechanizowaną pomocą. Praktyczność rozumowania wspomaganego komputerowo jest ponadto wykazać w książce towarzysz, Komputerowe uzasadnienie argumentacji: ACL2 studium przypadku.