Source: https://www.cs.utexas.edu/~moore/publications/acl2-books/car/index.html

Beskrivelse

Denne boken er en lærebokintroduksjon til datastøttet resonnement. Det kan brukes i hovedfags- og øvre divisjonskurs på programvareteknikk eller formelle metoder. Det er også egnet i forbindelse med andre bøker i kurs om maskinvaredesign, diskret matematikk eller teori, spesielt kurs som legger vekt på formalisme, strenghet eller mekanisert støtte. Det passer også for kurs om kunstig intelligens eller automatisert resonnement.

Nåværende maskinvare- og programvaresystemer er ofte svært komplekse og trenden går mot økt kompleksitet. Ved å modellere systemer matematisk får vi modeller som vi kan bevise oppfører seg riktig. For ytterligere å øke tilliten til resonnementet vårt, som kan være komplisert, kan vi bruke et dataprogram til å sjekke bevisene våre og til og med automatisere noe av konstruksjonen deres.

I denne boken presenterer vi:

  • Et praktisk funksjonelt programmeringsspråk nært knyttet til Common Lisp som brukes til å definere funksjoner (som kan modellere datasystemer) og for å komme med påstander om definerte funksjoner.
  • En formell logikk der definerte funksjoner tilsvarer aksiomer; logikken er førsteordens, inkluderer induksjon, og lar oss bevise teoremer om funksjonene.
  • Det datastøttede resonnementsystemet ACL2, som inkluderer programmeringsspråket, logikken og mekanisk støtte for bevisprosessen.

Denne boken vil lære deg hvordan du formaliserer ting, hvordan du konstruerer bevis og hvordan du bruker et mekanisk verktøy for å sjekke disse bevisene.

Vi bruker en spesiell formalisme og en spesiell mekanisering av den, nemlig ACL2, som er fritt tilgjengelig under vilkårene for en lisens i BSD-stil fra ACL2-hjemmesiden . ACL2 ble skrevet av Kaufmann og Moore og er etterfølgeren til “Boyer-Moore teorem-beviseren,” Nqthm. (Bob Boyer ga også betydelige tidlige bidrag til ACL2.) ACL2-hjemmesiden inkluderer den elektroniske referansehåndboken, som er et stort hypertekstdokument primært ment for brukere av systemet. Denne boken er den definitive introduksjonen til ACL2 og hvordan du bruker den.

Mens vi underviser i bruken av mekanisert formalisme, fokuserer vi på beregningsproblemer av den typen som vanligvis møter noen som bruker formelle metoder for å analysere maskinvare eller programvare.

ACL2 brukes i industrien. Husker du Intel FDIV-feilen? Det første Pentium [varemerket, Intel, Inc] kunne ikke dele flyttallstallene riktig, og det kostet etter sigende Intel 500 millioner dollar å fikse. På det tidspunktet det skjedde brukte vi ACL2 for å verifisere at mikrokoden for flytende punktdeling på AMDs konkurrerende mikroprosessor, AMD-K5, var riktig. AMD brukte ACL2 for å verifisere de grunnleggende flytepunktoperasjonene for den nylig utgitte Athlon. [Merk: AMD, AMD-logoen og kombinasjoner derav, AMD-K5, AMD-K7 og AMD Athlon er varemerker for Advanced Micro Devices, Inc.] Følgevolumet presenterer en nært beslektet case-studie.

ACL2-systemet har blitt brukt på prosjekter av kommersiell interesse, inkludert mikroprosessormodellering, maskinvareverifisering, mikrokodeverifisering og programvareverifisering. Denne boken gir en metodikk for å modellere datasystemer formelt og for resonnement om disse modellene med mekanisert assistanse. Det praktiske ved datastøttet resonnement er ytterligere demonstrert i følgeboken, Computer-Aided Reasoning: ACL2 Case Studies.