Rozumowanie wspomagane komputerowo: studia przypadków ACL2

admin

This is the translation. The original web-page (oryginalna strona): https://www.cs.uTeksas.edu/~moore/publications/acl2-books/acs/index.html

Matt Kaufmann, Panagiotis Manolios, i J Strother Moore (red.), Kluwer Academic Publishers, Czerwiec 2000. (ISBN 0-7923-7849-0)

Opis

Ta książka ilustruje, w jaki sposób komputerowo wspomagany system rozumowania ACL2 może być używany w produktywnych i innowacyjnych sposobach projektowania, budowania i utrzymywania sprzętu i oprogramowania. Uwzględniono tutaj artykuły techniczne napisane przez dwudziestu jeden autorów, które przedstawiają samodzielne studia przypadków, z których niektóre to “odkażone” projekty przemysłowe. Zajmują się szeroką gamą pomysłów, w tym arytmetyką zmiennoprzecinkową, symulacją mikroprocesora, sprawdzaniem modeli, symboliczną oceną trajektorii, kompilacją, sprawdzaniem dowodów, analizą rzeczywistą i kilkoma innymi.

Książka jest przeznaczona dla dwóch odbiorców: tych, którzy szukają innowacyjnych sposobów szybszego i bardziej niezawodnego projektowania, budowania i utrzymywania sprzętu i oprogramowania oraz tych, którzy chcą się dowiedzieć, jak to zrobić. Do byłych odbiorców należą kierownicy projektów i studenci na kursach ankietowych. Ta ostatnia grupa odbiorców obejmuje studentów i profesjonalistów stosujących rygorystyczne podejście do inżynierii sprzętu i oprogramowania lub metod formalnych. Książka może być używana na kursach magisterskich i licencjackich wyższego stopnia z zakresu inżynierii oprogramowania, metod formalnych, projektowania sprzętu, teorii obliczeń, sztucznej inteligencji i automatycznego rozumowania.

Książka jest podzielona na dwie części. Część I zaczyna się od omówienia wysiłku związanego z używaniem ACL2. Zawiera również krótkie wprowadzenie do logiki ACL2 i jej mechanizacji, które ma dać czytelnikowi wystarczające podstawy do przeczytania studiów przypadku. Bardziej szczegółowe, podręcznikowe wprowadzenie do ACL2 można znaleźć w książce towarzyszącej Computer-Aided Reasoning: An Approach (Rozumowanie wspomagane komputerowo: podejście).

ACL2 jest ulepszoną i rozszerzoną wersją „dowodu twierdzenia Boyera-Moore’a”, Nqthm, dostosowaną do stosowanego Common Lispa. Redaktorzy Kaufmann i Moore są autorami systemu ACL2. (Bob Boyer również wniósł znaczący wkład w rozwój ACL2.) ACL2 można uzyskać bezpłatnie na warunkach Powszechnej Licencji Publicznej GNU ze strony Domowej ACL2, która zawiera nie tylko kod źródłowy i obszerną dokumentację hipertekstową, ale także wiele artykułów o ACL2 i jej aplikacje, wycieczki z przewodnikiem po systemie i listy mailingowe.

Sercem książki jest Część II, w której przedstawiono studia przypadków. Studia przypadków obejmują szeroki zakres zastosowań, od sprzętu (np. Arytmetyka zmiennoprzecinkowa, języki opisu sprzętu i analiza trajektorii symbolicznej) po oprogramowanie (np. Wyszukiwanie wykresów, kompilacja i algorytm sprawdzania modeli) i nie tylko (teoria liczb i rzeczywista analiza). Wszystkie są wykonywane w jednym mechanicznie obsługiwanym schemacie matematycznym: ACL2.

Pełne rozwiązanie każdego studium przypadku jest dostępne tutaj. Na przykład, gdy mówimy, że jedno ze studiów przypadku formalizuje mnożnik zmiennoprzecinkowy i udowadnia, że ​​jest poprawny, mamy na myśli, że nie tylko można przeczytać angielski opis modelu i tego, w jaki sposób został on sprawdzony, ale można uzyskać cały formalną treść projektu i, jeśli chcesz, powtórz odbitki próbne wraz z kopią ACL2. A zatem ta książka to dopiero początek. Jeśli naprawdę chcesz się dowiedzieć, jak udowodnić poprawność mnożnika zmiennoprzecinkowego lub kompilatora, przeczytaj artykuły, a następnie pobierz skrypty i powiel dowody. Następnie zmodyfikuj je i eksperymentuj.

Studia przypadków zawierają ćwiczenia, których rozwiązania znajdują się w sieci. Ponadto kompletne skrypty ACL2 niezbędne do sformalizowania modeli i udowodnienia, że ​​wszystkie omówione właściwości znajdują się w Internecie. Jeśli chcesz opanować techniki użyte do wykonania określonego projektu, wykonaj ćwiczenia w studiach przypadków, które wyglądają podobnie do twojego projektu.

Współtwórcy

Współautorzy tego tomu są wymienieni poniżej wraz z ich przynależnością w czasie pracy.

Piergiorgio Bertoli IRST – Istituto per la Ricerca
Scientifica e Tecnologica
Povo, Włochy
Dominique Borrione TIMA-UJF
Grenoble, Francja
John Cowles Katedra Informatyki

Uniwersytet Wyoming
Laramie, Wyoming
Arthur Flatau Advanced Micro Devices, Inc.
Austin, Teksas
Ruben Gamboa Logical Information Machines, Inc.
Austin, Teksas
Philippe Georgelin TIMA-UJF
Grenoble, Francja
Wolfgang Goerigk Institut fur Informatik und
Praktische Mathematik
Christian-Albrechts-Universitat zu Kiel
Kiel, Niemcy
David Greve Rockwell Collins
Centrum Zaawansowanych Technologii
Cedar Rapids, Iowa
David Hardin Ajile Systems, Inc.
Oakdale, Iowa
Warren A. Hunt, Jr. Laboratorium badawcze IBM Austin
Austin, Teksas
Damir A. Jamsek Laboratorium badawcze IBM Austin
Austin, Teksas
Matt Kaufmann Advanced Micro Devices, Inc.
Austin, Teksas
Panagiotis Manolios Wydział Informatyki
Uniwersytet Teksasu w Austin
Austin, Teksas
William McCune Matematyka i informatyka Podział
Narodowe laboratorium Argonne
Argonne, Illinois
J Strother Moore Wydział Informatyki
Uniwersytet Teksasu w Austin
Austin, Teksas
Vanderlei Rodrigues TIMA-UJF
Grenoble, Francja
(na urlopie od UFRGS,
Porto Alegre, Brazylia)
David M. Russinoff Advanced Micro Devices, Inc.
Austin, Teksas
Jun Sawada Wydział Informatyki,
Uniwersytet Teksasu w Austin
Austin, Teksas
Olga Shumsky Katedra Inżynierii Elektrycznej i Komputerowej
Uniwersytet Północno-Zachodni
Evanston, Illinois
Paolo Traverso IRST – Istituto per la Ricerca
Scientifica e Tecnologica
Povo, Włochy
Matthew Wilding Rockwell Collins
Centrum Zaawansowanych Technologii
Cedar Rapids, Iowa

Materiał pomocniczy do studiów przypadków, w tym rozwiązania ćwiczeń

Autorzy studiów przypadku dostarczyli pełne skrypty odtwarzające przedstawione wyniki. Ten „materiał pomocniczy” zawiera również rozwiązania ćwiczeń w każdym studium przypadku. Istnieje oddzielny katalog dla materiałów pomocniczych każdego studium przypadku, który można znaleźć w workshops/1999 katalogu, który można pobrać z http://acl2.org/index.html lub za pomocą SVN, jak wyjaśniono na   stronie projektu acl2-books. Istnieje plik najwyższego poziomu README, a każdy podkatalog zawiera READMEplik wyjaśniający jego zawartość.

5. Ćwiczenie z teorii grafów (J Moore; katalog graph/)

Rozdział formalizuje i udowadnia poprawność kilku prostych algorytmów określania, czy istnieje ścieżka między dwoma węzłami skończonego grafu skierowanego.

6. Dowód modułowy: podstawowe twierdzenie rachunku różniczkowego (Matt Kaufmann; katalog calculus/)

Rozdział przedstawia modułową metodologię dowodu z góry na dół i używa jej do sformalizowania i udowodnienia Podstawowego twierdzenia rachunku różniczkowego. Strategia modułowa działa zarówno dla ACL2, jak i “ACL2(r)” (patrz Rozdział 18 poniżej); Podstawowe Twierdzenie jest udowodnione za pomocą ACL2(r).

7. Sprawdzanie modeli w Mu-Calculus (Panagiotis Manolios; katalog mu-calculus/)

Rozdział przedstawia formalne rozwinięcie składni i semantyki rachunku Mu, narzędzie do sprawdzania modelu w ACL2 oraz omówienie tłumaczenia innych logik czasowych na rachunek Mu. Sprawdzanie modelu jest poprawne.

8. Szybkie, analizowalne symulatory (David Greve, Matthew Wilding, David Hardin; katalog simulator/)

Szybkie modele symulacyjne są rutynowo opracowywane podczas projektowania złożonych systemów sprzętowych w celu przewidywania wydajności, wykrywania wad projektowych i umożliwienia wspólnego projektowania sprzętu i oprogramowania. Napisanie takiego wykonywalnego modelu w ACL2 niesie ze sobą dodatkowe korzyści wynikające z analizy formalnej; jednak trzeba dużo uwagi, aby zbudować model ACL2, który jest zarówno szybki, jak i analizowalny. W tym rozdziale opisano techniki konstruowania szybkich, formalnie analizowalnych symulatorów w ACL2. Ich użyteczność jest pokazana na prostym modelu procesora.

9. Weryfikacja prostego modelu maszyny z rurociągami (Jun Sawada; katalog pipeline/)

Zdefiniowano model ACL2 trójstopniowej maszyny z rurociągami wraz z modelem odpowiadającej mu maszyny sekwencyjnej. Następnie przedstawiono dowód równoważności między dwoma maszynami. Co ważniejsze, metoda dekompozycji dowodu ma zastosowanie do znacznie bardziej skomplikowanych architektur potokowych.

10. Język DE (Warren Hunt, Jr .; katalog de-hdl/)

Język DE jest językiem opisu zorientowanym na zdarzenia, który umożliwia hierarchiczną definicję maszyn o skończonych stanach w stylu języka opisu sprzętu. Składnia i semantyka języka są sformalizowane, a formalizacja służy do udowodnienia poprawności prostego obwodu sprzętowego. Takie formalne HDL zostały wykorzystane do udowodnienia właściwości znacznie bardziej skomplikowanych projektów.

11. Używanie makr do naśladowania języka VHDL (Dominique Borrione, Philippe Georgelin, Vanderlei Rodrigues; katalog vhdl/)

Celem tego projektu było sformalizowanie niewielkiego, dającego się zsyntetyzować, behawioralnego podzbioru języka VHDL, przy jak największym zachowaniu składniowego smaku języka VHDL i ułatwieniu weryfikacji poprzez symulację symboliczną i dowodzenie twierdzeń.

12. Symboliczna ocena trajektorii (Damir A. Jamsek; katalog ste/)

Symbolic Trajectory Evaluation (STE) to forma sprawdzania modelu zasadniczo oparta na symulacji symbolicznej. W tym rozdziale przedstawiono formalne podejście do STE, w tym dowody ACL2 wyników przedstawione w artykule Segera i Joyce’a “A Mathematically Precise Two-Level Formal Hardware Verification Methodology”.

13. Weryfikacja RTL: mnożnik zmiennoprzecinkowy (David M. Russinoff, Arthur Flatau; katalogu multiplier/)

W tym rozdziale opisano mechaniczny system sprawdzający dla projektów reprezentowanych w języku RTL Advanced Micro Devices. System składa się z translatora ACL2 oraz metodologii weryfikacji właściwości programów wynikowych przy użyciu narzędzia ACL2. Udowodniono poprawność prostego mnożnika zmiennoprzecinkowego.

14. Weryfikacja projektu wbudowanego weryfikatora krytycznego dla bezpieczeństwa (Piergiorgio Bertoli, Paolo Traverso; katalog embedded/)

Ten rozdział przedstawia użycie ACL2 do weryfikacji projektu oprogramowania krytycznego dla bezpieczeństwa, wbudowanego weryfikatora. Wbudowany weryfikator sprawdza online, czy każde wykonanie translatora krytycznego dla bezpieczeństwa jest poprawne. Translator jest elementem systemu oprogramowania używanego przez Union Switch i Signal do budowy pokładowych systemów sterowania. 

15. Ponowna weryfikacja kompilatora (Wolfgang Goerigk; katalog compiler/)

To badanie ilustruje fakt zaobserwowany przez Kena Thompsona w jego wykładzie z nagrodą Turinga: kod maszynowy poprawnego kompilatora może zostać zmieniony tak, aby zawierał konia trojańskiego, tak aby kompilator przeszedł prawie każdy test, w tym tak zwany “test bootstrap” w którym kompiluje własny kod źródłowy z identycznymi wynikami i nadal może generować “zły” kod. Kompilator, maszyna kodu wynikowego i eksperymenty są sformalizowane w ACL2.

16. Ivy: A Preprocessor and Proof Checker for First-Order Logic (William McCune, Olga Shumsky; katalog ivy/)

W tym studium przypadku sprawdzian dowodu dla logiki pierwszego rzędu okazał się słuszny dla skończonych interpretacji. Ponadto badanie pokazuje, w jaki sposób programy inne niż ACL2 mogą być łączone z funkcjami ACL2 w taki sposób, aby można było udowodnić przydatne właściwości programów złożonych. Nic nie zostało udowodnione na temat programów innych niż ACL2. Zamiast tego wyniki programów innych niż ACL2 są sprawdzane w czasie wykonywania przez funkcje ACL2, a właściwości tych funkcji sprawdzających są sprawdzane.

17. Knuth’s Generalization of McCarthy’s 91 Function (John Cowles; katalog knuth-91/)

W tym rozdziale zajmiemy się wyzwaniem Donalda Knutha dotyczącym “komputerowego dowodu” twierdzenia o jego uogólnieniu słynnej “funkcji 91 Johna McCarthy’ego”. Uogólnienie obejmuje liczby rzeczywiste, a studium przypadku wykorzystuje ACL2 do spełnienia wyzwanie poprzez mechaniczną weryfikację wyników nie tylko w zakresie wszystkich liczb rzeczywistych, ale także w odniesieniu do każdego podpola tego pola.

18. Ciągłość i różniczkowalność (Ruben Gamboa; katalog analysis/)

Ten rozdział pokazuje, w jaki sposób rozszerzona wersja ACL2 (nazwana  ACL2 (r)) i opisana może być użyta do wnioskowania o liczbach rzeczywistych i zespolonych przy użyciu niestandardowej analizy. Opisuje pewne modyfikacje ACL2, które wprowadzają nieracjonalne liczby rzeczywiste i zespolone do systemu liczbowego ACL2. Następnie pokazuje, jak zmodyfikowany ACL2 może dowieść klasycznych twierdzeń analizy, takich jak twierdzenia o wartości pośredniej i wartości średniej.