ACL2

Logo de ACL2

ACL2 és, al mateix temps, un llenguage de programació, una llògica matemàtica per a especificar i demostrar formalment propietats dels programes escrits en dit llenguage, i un demostrador automàtic de teoremes que vares agarrar a l'usuari en dita tasca. ACL2 és la versió industrial del demostrador NQTHM de R. Boyer i J S. Moore. En l'actualitat està desenrollat per J S. Moore i M. Kaufmann en l'Universitat de Texas en Austin. El nom ACL2 és una abreviatura de A Computational Logic for an Applicative Common LISP.

El llenguage de programació ACL2 és un subconjunt aplicativa de Common LISP. ACL2 és un llenguage sense tipos degut a que totes les funcions de ACL2 són totals –és dir, tota funció associa a cada valor de l'univers de ACL2 un atre valor d'eixe univers. Els programes escrits en ACL2 poden ser eixecutats en Common Lisp directament. El propi ACL2 està desenrollat usant el seu mateix llenguage aplicatiu.

Una característica important de ACL2 és que s'usa el mateix llenguage tant per a l'implementació dels programes com per a l'especificació de les seues propietats. la llògica de ACL2 és un subconjunt de la llògica de primer orde. Les seues fòrmules no tenen quantificadors i les variables d'una fòrmula es consideren (implícitament) universalment quantificades. La teoria de base de ACL2 axiomatiza la semàntica del seu llenguage de programació i de les seues funcions predefinides, tal i com es descriuen en l'estàndart Common Lisp. Quan les definicions de l'usuari satisfan un cert principi de definició estenen la teoria en el corresponent axioma de definició. Grosso modo, el principi de definició garantisa que la funció definida termina per a totes les entrades possibles, mantenint aixina la consistència llògica de la teoria.

El demostrador de ACL2 pot considerar-se com un assistent per a la demostració de teoremes en la llògica de ACL2. El motor de demostració de ACL2 està basat principalment en la reescritura de térmens i en l'automatisació del principi d'inducció. Encara que en principi ACL2 pot ser considerat un demostrador automàtic (una volta introduïda una conjectura, procedix de manera automàtica en el seu intent de demostració), el sistema és interactiu en un sentit més profunt. El paper de l'usuari en una formalisació típica en ACL2 consistix en: a) definir les funcions que implementen el sistema que es vol verificar, b) escriure l'especificació del mateix, expressant les propietats formals que es desigen verificar i c) guiar al demostrador cap a una demostració automàtica de dita especificació. La manera principal per mig de la qual l'usuari guia al demostrador consistix en la demostració de lemes previs que s'inclouen en el sistema com a regles de reescritura i que són usats en la demostració de posteriors resultats. Els lemes específics necessaris per a cada demostració poden vindre sugerits d'una demostració (manual) preconcebuda o be, a més baix nivell, de l'inspecció de l'eixida generada per un intent de demostració automàtica fallanc.

L'objectiu dels creadors de ACL2 va ser realisar una versió del demostrador NQTHM de Boyer-Moore que poguera ser utilisat per a aplicacions d'escala industrial. Per eixe objectiu, ACL2 conté moltes característiques que permeten el desenroll net de teories matemàtiques i computacionals. Ademés, ACL2 obté eficiència gràcies a que està escrit en Common LISP. Aixina, la mateixa especificació que és la base per a una verificació formal pot ser compilada i eixecutada en còdic natiu.

La principal aplicació de ACL2 es troba en la verificació formal de sistemes hardware la seguritat del qual és crítica. Dits sistemes són modelats en el llenguage de programació i les propietats que asseguren la seua correcció són formalment verificades. El fet de que el model puga ser eixecutat de manera eficient permet ademés que puga ser usat com un simulador del sistema modelat.

En l'any 2005, l'ACM va concedir el premi de software al demostrador de teoremes de Boyer i Moore (lo que inclou tant a NQTHM com a ACL2). Lliteralment, el premi es concedix a R. Boyer, M. Kaufmann i J S. Moore per ser precursors i autors "del més efectiu demostrador de teoremes com una ferramenta de métodos formals per a la verificació d'hardware i software la seguritat del qual és crítica".

Sistemes d'reescritura de ACL2

La llògica ecuacional es formalisa en ACL2, un llenguage de programació i de llògica matemàtica utilisat per a la demostració formal de teoremes.

El seu concepte de conseqüència llògica es representa per mig d'un conjunt de axioma ecuacionales que pot ser descrit per mig d'una relació d'equivalència. Esta relació procedix del conjunt de térmens de primer orde, és dir, per mig d'axioma reemplaçant iguals per iguals (proposicions que s'assumixen com a verdaderes sense necessitat d'una demostració prèvia). Lo anteriorment dit és com es representa en ACL2 la teoria ecuacional.

Es diu sistema d'reescritura al conjunt d'equacions orientades de dreta a esquerra i per a conseguir la reducció associada a este tipo de sistemes s'ampra la noetherianidad i un algoritme de càlcul de formes normals. Un sistema d'reescritura conclou en estudiar un conjunt finit de parells cridats parells crítics.

Tipos de senyes en ACL2

Existixen diferents tipos d'objectes en ACL2:

Tipos d'objectes

Objecte	Valor associat
Números	7, -5, 2/5, c(2 1).
Caràcters	#�, Space.
Cadenes de caràcters	"Bones" "Vesprades"
Símbols	t, nil, x, NWM::a.
Parells punteados	(1 . 2), (i j k).

Sobre el maneig dels diferents tipos de números en ACL2:

• Els número racional s'escriuen com a fracció d'número entero.
• En ACL2, els símbols estan formats per dos cadenes de caràcters: el seu nom de paquet i el seu nom de símbol.
  • Per eixemple, el símbol el nom del qual de paquet és NWM i el nom del qual de símbol és a, s'escriu NWM::a

Teories ecuacionales en ACL2

Dau un sistema d'equacions I (axioma), la teoria ecuacional d'I és el conjunt d'equacions (teoremes) que són conseqüència llògica de E.

Una teoria ecuacional es pot vore com la relació d'equivalència descrita per una reducció: reemplazamiento o reescritura d'iguals per iguals, usant els axioma de la teoria. La teoria ecuacional ha segut exposta com l'equivalència d'una reducció concreta. En ACL2, tot sistema d'reescritura noetheriano, els parells crítics de la qual confluïxen, descriu una teoria ecuacional decidible.

Funcions i macros base en ACL2

La gran part de les funcions base de ACL2 provenen del software Common Lisp. Existixen moltes d'elles dedicades a aritmètiques, conversió, reconocedor de números/objectes, etc.

Algunes funciones eixemple són les següents:

(< x i)         Menor estricte
(<= x i)        Menor o igual
(> x i)         Major
(>= x i)        Major o igual
(+ x i ...)     Suma
(* x i ...)     Multiplicació
(- x i)         Resta
(- x)           Opost
(/ x i)         Divisió
(nfix x)        Conversió a número natural
(consp x)       Reconocedor de parells punteados
(atom x)        Reconocedor d'objectes atòmics
(true-listp l)  Reconocedor de llestes