Computer-Aided Reasoning - 9781441949813

Kompiuterinis samprotavimas: ACL2 atvejų tyrimai iliustruoja, kaip kompiuterinė samprotavimo sistema ACL2 gali būti naudojama produktyviais ir novatoriškais būdais projektuojant, kuriant ir prižiūrint techninės ir programinės įrangos sistemas. Čia yra dvidešimt vieno bendraautorio parašyti techniniai dokumentai, kuriuose pateikiami savarankiški atvejų tyrimai, kai kurie iš jų yra švarūs pramoniniai projektai. Straipsniuose nagrinėjamos įvairios idėjos, įskaitant slankiojo kablelio aritmetiką, mikroprocesoriaus modeliavimą, modelio tikrinimą, simbolinės trajektorijos įvertinimą, kompiliavimą, įrodymų tikrinimą, realią analizę ir keletą kitų. Kompiuterinis samprotavimas: „ACL2 Case Studies“ yra skirtas dviem auditorijoms: ieškantiems naujoviškų būdų greičiau ir patikimiau kurti, kurti ir prižiūrėti techninę ir programinę įrangą, ir tiems, kurie nori išmokti tai padaryti. Buvusi auditorija – projektų vadovai ir į apklausą orientuotų kursų studentai. Pastaroji auditorija apima studentus ir specialistus, kurie griežtai laikosi techninės ir programinės įrangos inžinerijos ar formalių metodų. Kompiuterinis samprotavimas: ACL2 atvejų studijos gali būti naudojamos absolventų ir aukštesniųjų skyrių bakalauro kursuose apie programinės įrangos inžineriją, formalius metodus, aparatinės įrangos projektavimą, skaičiavimo teoriją, dirbtinį intelektą ir automatizuotą samprotavimą. Knyga padalinta į dvi dalis. I dalis prasideda diskusijomis apie pastangas naudojant ACL2. Jame taip pat yra trumpas įvadas į ACL2 logiką ir jos mechanizavimą, kuris turi suteikti skaitytojui pakankamai žinių, kad galėtų perskaityti atvejų tyrimus. Išsamesnį vadovėlio įvadą į ACL2 galima rasti papildomoje knygoje „Computer-Aided Reasoning: An Approach“. Knygos esmė yra II dalis, kurioje pateikiami atvejų tyrimai. Atvejo analizėse yra pratimų, kurių sprendimai yra internete. Be to, visi ACL2 scenarijai, reikalingi modeliams formalizuoti ir visoms aptartoms savybėms įrodyti, yra internete. Pavyzdžiui, kai sakome, kad viena iš atvejo tyrimų formalizuoja slankiojo kablelio daugiklį ir įrodo, kad jis teisingas, tai reiškia, kad galite ne tik perskaityti modelio aprašymą angliškai ir kaip jis buvo įrodytas teisingu, bet ir gauti visą oficialų projekto turinį ir, jei norite, pakartokite įrodymus su savo ACL2 kopija. ACL2 galima gauti iš jo pagrindinio puslapio. Šiame puslapyje rasite kiekvieno atvejo tyrimo rezultatus, kaip ACL2 įvesties scenarijus, taip pat abiejų knygų pratimų sprendimus.