Computer-Aided Reasoning - 9781441949813

Rozumowanie wspomagane komputerowo: Studia przypadków ACL2 ilustrują, w jaki sposób system rozumowania wspomaganego komputerowo ACL2 może być używany w produktywny i innowacyjny sposób do projektowania, budowania i utrzymywania systemów sprzętu i oprogramowania. Zawarte są tu artykuły techniczne napisane przez dwudziestu jeden autorów, które przedstawiają niezależne studia przypadków, z których część to oczyszczone projekty przemysłowe. Artykuły dotyczą szerokiej gamy zagadnień, w tym arytmetyki zmiennoprzecinkowej, symulacji mikroprocesorowej, sprawdzania modeli, oceny symbolicznej trajektorii, kompilacji, sprawdzania dowodów, analizy rzeczywistej i kilku innych. Rozumowanie wspomagane komputerowo: Studia przypadków ACL2 są przeznaczone dla dwóch odbiorców: tych, którzy szukają innowacyjnych sposobów projektowania, budowania i utrzymywania systemów sprzętu i oprogramowania szybciej i bardziej niezawodnie, oraz tych, którzy chcą się dowiedzieć, jak to zrobić. Do pierwszej grupy odbiorców zaliczają się kierownicy projektów i studenci kursów opartych na ankietach. Ta ostatnia grupa odbiorców obejmuje studentów i specjalistów stosujących rygorystyczne podejście do inżynierii sprzętu i oprogramowania lub metod formalnych. Rozumowanie wspomagane komputerowo: Studia przypadków ACL2 można wykorzystać na studiach licencjackich i magisterskich na wyższych wydziałach w zakresie 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 rozpoczyna się od omówienia wysiłku związanego z używaniem ACL2. Zawiera także krótkie wprowadzenie do logiki ACL2 i jej mechanizacji, które ma na celu zapewnienie czytelnikowi wystarczającej wiedzy do zapoznania się ze studiami przypadków. Bardziej szczegółowe, podręcznikowe wprowadzenie do ACL2 można znaleźć w książce towarzyszącej Computer-Aided Reasoning: An Approach. Sercem książki jest Część II, w której zaprezentowano studia przypadków. Studia przypadków zawierają ćwiczenia, których rozwiązania znajdują się w sieci. Ponadto kompletne skrypty ACL2 niezbędne do sformalizowania modeli i udowodnienia wszystkich omawianych właściwości znajdują się w Internecie. Na przykład, gdy mówimy, że jedno ze studiów przypadków formalizuje mnożnik zmiennoprzecinkowy i udowadnia jego poprawność, mamy na myśli, że nie tylko można przeczytać angielski opis modelu i sposób, w jaki udowodniono jego poprawność, ale można uzyskać cały formalną treść projektu i, jeśli chcesz, odtwórz próbki z kopią ACL2. ACL2 można pobrać ze strony głównej. Wyniki przedstawione w każdym studium przypadku, jako skrypty wejściowe ACL2, a także rozwiązania ćwiczeń dla obu książek, są dostępne na tej stronie.