La lògica de Hoare (també coneguda com a lògica de Floyd – Hoare o regles de Hoare) és un sistema formal amb un conjunt de regles lògiques per raonar rigorosament sobre la correcció dels programes informàtics. Va ser proposada el 1969 per l'informàtic i lògic britànic Tony Hoare, i posteriorment refinada per Hoare i altres investigadors. Les idees originals van ser sembrades pel treball de Robert W. Floyd, que havia publicat un sistema similar per a diagrames de flux.

Triple Hoare La característica central de la lògica de Hoare és el triplet de Hoare. Un triplet descriu com l'execució d'un fragment de codi canvia l'estat del càlcul. Un triplet de Hoare és de la forma

on i són afirmacions i és una ordre. s'anomena la precondició i la postcondició: quan es compleix la precondició, l'execució de l'ordre estableix la postcondició. Les assercions són fórmules en lògica de predicats.

La lògica de Hoare proporciona axiomes i regles d'inferència per a totes les construccions d'un llenguatge de programació imperatiu simple. A més de les regles per al llenguatge simple de l'article original de Hoare, Hoare i molts altres investigadors han desenvolupat regles per a altres construccions de llenguatge des de llavors. Hi ha regles per a la concurrència, els procediments, els salts i els punters.

Correcció parcial i total Utilitzant la lògica estàndard de Hoare, només es pot demostrar una correcció parcial. La correcció total també requereix la terminació, que es pot demostrar per separat o amb una versió ampliada de la regla While. Així, la lectura intuïtiva d'un triplet de Hoare és: Sempre que possessió de l'estat abans de l'execució de , aleshores es mantindrà després, o no acaba. En aquest darrer cas, no hi ha un "després", per tant pot ser qualsevol afirmació. De fet, es pot triar ser fals per expressar això no finalitza.

"Terminació" aquí i a la resta d'aquest article s'entén en el sentit més ampli que el càlcul finalment s'acabarà, és a dir, implica l'absència de bucles infinits; no implica l'absència de violacions del límit d'implementació (per exemple, la divisió per zero) que aturin el programa prematurament. En el seu article de 1969, Hoare va utilitzar una noció més estreta de terminació que també implicava l'absència de violacions del límit d'implementació, i va expressar la seva preferència per la noció més àmplia de terminació, ja que manté les assercions independents de la implementació:

Una altra deficiència en els axiomes i regles citats anteriorment és que no donen cap base per demostrar que un programa finalitza correctament. L'error en finalitzar pot ser degut a un bucle infinit; o pot ser degut a la violació d'un límit definit per la implementació, per exemple, el rang d'operands numèrics, la mida de l'emmagatzematge o un límit de temps del sistema operatiu. Per tant, la notació "𝑃{𝑄}𝑅

" s'ha d'interpretar com a "sempre que el programa finalitzi correctament, les propietats dels seus resultats es descriuen mitjançant 𝑅". És bastant fàcil adaptar els axiomes de manera que no es puguin utilitzar per predir els "resultats" dels programes que no finalitzen; però l'ús real dels axiomes ara dependria del coneixement de moltes característiques dependents de la implementació, per exemple, la mida i la velocitat de l'ordinador, el rang de nombres i l'elecció de tècniques de desbordament. A part de les proves de com evitar bucles infinits, probablement és millor demostrar la correcció "condicional" d'un programa i confiar en una implementació per donar un avís si ha hagut d'abandonar l'execució del programa com a resultat de la violació d'un límit d'implementació.

— Hoare 1969, pàg. 578–579

Regles Esquema d'axiomes d'enunciats buits La regla de les sentències buides afirma que L'instrucció no canvia l'estat del programa, per tant, el que sigui cert abans també és vàlid després.

Esquema d'axiomes d'assignació L'axioma d'assignació estableix que, després de l'assignació, qualsevol predicat que abans era cert per al costat dret de l'assignació ara es compleix per a la variable. Formalment, sigui una asserció en què la variable és lliure. Aleshores:

on denota l'asserció en què cada aparició lliure de ha estat substituïda per l'expressió

L'esquema axiomàtic d'assignació significa que la veritat de és equivalent a la veritat posterior a l'assignació de Així doncs, cert abans de l'assignació, per l'axioma d'assignació, aleshores seria cert després de la qual cosa. A l'inrevés, si fals (és a dir, cert) abans de l'instrucció d'assignació, ha de ser fals després.

Exemples de triplets vàlids inclouen:

Totes les precondicions que no siguin modificades per l'expressió es poden transferir a la postcondició. En el primer exemple, assignant no canvia el fet que , de manera que ambdues afirmacions poden aparèixer a la postcondició. Formalment, aquest resultat s'obté aplicant l'esquema d'axiomes amb sent ( i ), que produeix ésser ( i ), que al seu torn es pot simplificar a la precondició donada .

L'esquema de l'axioma d'assignació és equivalent a dir que per trobar la precondició, primer cal agafar la postcondició i substituir totes les aparicions del costat esquerre de l'assignació pel costat dret de l'assignació. Aneu amb compte de no intentar fer-ho a l'inrevés seguint aquesta manera de pensar incorrecta : ; aquesta regla porta a exemples absurds com ara:

Una altra regla incorrecta que sembla temptadora a primera vista és ; això porta a exemples absurds com ara:

Mentre que una postcondició determinada determina únicament la precondició , el contrari no és cert. Per exemple:

, , , and

són instàncies vàlides de l'esquema axiomàtic d'assignació.

L'axioma d'assignació proposat per Hoare no s'aplica quan més d'un nom pot referir-se al mateix valor emmagatzemat. Per exemple,

és incorrecte si i es refereixen a la mateixa variable (aliasing), tot i que és una instància adequada de l'esquema d'axiomes d'assignació (amb tots dos i ésser ).

Verificació del codi d'intercanvi sense variables auxiliars

Les tres instruccions següents (línia 2, 4, 6) intercanvien els valors de les variables a i b, sense necessitat d'una variable auxiliar. A la prova de verificació, el valor inicial d'a i b es denota per les constants A i B, respectivament. La prova es llegeix millor cap enrere, començant per la línia 7; per exemple, la línia 5 s'obté de la línia 7 substituint a (expressió de destinació a la línia 6) per 𝑎−𝑏 (expressió d'origen a la línia 6). Algunes simplificacions aritmètiques s'utilitzen tàcitament, és a dir. 𝑎−(𝑎−𝑏=𝑏 (línia 5→3), etc. 𝑎+𝑏−𝑏=𝑎(línia 3→1). NrCodiAssercions1: 2:3:4:5:6:7: La regla de composició de Hoare s'aplica als programes i executats seqüencialment, on s'executa abans de i s'escriu ( s'anomena la condició mitjana):

Per exemple, considerem els dos exemples següents de l'axioma d'assignació:

i

Segons la regla de seqüenciació, es conclou:

Un altre exemple es mostra al requadre de la dreta.

Referències

Categoria:Lògica computacional