Logica Hoare

Logica lui Hoare este un sistem formal care se încadrează în semantica axiomatică publicată pentru prima dată în 1969 de CAR Hoare care urmărește, prin definirea unui set inițial de axiome și reguli asupra acestora, să evalueze corectitudinea programelor folosind rigoarea matematicii. formalisme .

Logica a fost dezvoltată pentru a fi utilizată cu un limbaj de programare imperativ simplu și a suferit dezvoltări suplimentare datorită lui Hoare însuși și altor cercetători pentru gestionarea unor cazuri particulare, cum ar fi concurența , indicatorii și procedurile .

Triple of Hoare

Întregul sistem se bazează pe triplul concept al lui Hoare .

Acest triplu definește modul în care executarea unei comenzi schimbă adevărul despre program și este definit ca

\{P\}\;C\;\{Q\}

{\ displaystyle \ {P \} \; C \; \ {Q \}}

{\ displaystyle \ {P \} \; C \; \ {Q \}}

Unde P și Q se numesc afirmații și C este o comandă. În cazul specific, P este definit ca precondiție și Q postcondiție .

În lucrarea sa originală, Hoare definește semnificația triplului ca:

"Dacă declarația P este adevărată înainte de executarea unei comenzi sau a unei serii de comenzi C , atunci Q este adevărată după executare."

( CAR Hoare , o bază axiomatică pentru programarea computerizată )

În cazul în care nu există condiții prealabile care trebuie respectate, pur și simplu scriem

\{true\}\;C\;\{Q\}

{\ displaystyle \ {true \} \; C \; \ {Q \}}

{\ displaystyle \ {true \} \; C \; \ {Q \}}

Sistemul de verificare a triplelor folosește axiome , adică triple care sunt întotdeauna satisfăcute și reguli de inferență care fac posibilă simplificarea comenzii prin inducție structurală.

Axiome și reguli de inferență

Axioma educației goale

Acesta este cazul de bază foarte simplu, dar util pentru a înțelege raționamentul care trebuie făcut cu triplele Hoare:

\{P\}\ {\textbf {skip}}\ \{P\}

{\ displaystyle \ {P \} \ {\ textbf {skip}} \ \ {P \}}

{\ displaystyle \ {P \} \ {\ textbf {skip}} \ \ {P \}}

Corectitudinea este evidentă, deoarece pornim de la o stare inițială, precondiție P, comanda nu face nicio modificare și apoi ajungem în starea finală, post condiție, P.

Assiom al misiunii

Cel mai caracteristic caz de funcționare într-un limbaj de programare este în mod clar atribuirea, deci avem următoarea situație:

\{P\}\;\{x:=f\}\;\{Q\}

{\ displaystyle \ {P \} \; \ {x: = f \} \; \ {Q \}}

{\ displaystyle \ {P \} \; \ {x: = f \} \; \ {Q \}}

unde x este o variabilă și f este o expresie fără efecte secundare, dar poate conține x .

Executarea comenzii nu poate implica nimic în ceea ce privește condițiile prealabile, dar orice postcondiție a programului care se referă la x și este adevărată după executare, trebuie să fie adevărată pentru f înainte de execuție, deoarece comanda înlocuiește valoarea lui x cu cea evaluată din expresia f .

În mod formal avem:

\vdash P_{0}\;\{x:=f\}P

{\ displaystyle \ vdash P_ {0} \; \ {x: = f \} P}

{\ displaystyle \ vdash P_ {0} \; \ {x: = f \} P}

unde x este variabila, f este expresia e $P_{0}$ ${\ displaystyle P_ {0}}$ $P_0$ se obține din P prin substituirea fiecărei apariții a x cu expresia f .

Folosind reprezentarea cu reetichetarea putem exprima și axioma cu notația sa clasică:

{\frac {}{\{P[E/x]\}\ x:=E\ \{P\}}}

{\ displaystyle {\ frac {} {\ {P [E / x] \} \ x: = E \ \ {P \}}}}

{\ displaystyle {\ frac {} {\ {P [E / x] \} \ x: = E \ \ {P \}}}}

Rețineți că axioma este de fapt o clasă de axiome care aderă la un anumit model.

Regula consecinței

Regula consecinței permite deducerea unor adevăruri suplimentare pornind de la altele deja specificate. Să presupunem că un fragment al programului Q are ca postcondiție R : în mod natural, după executarea fragmentului, tot ceea ce este implicat de R va fi, de asemenea, adevărat. În schimb, să presupunem că un fragment Q are P ca condiție prealabilă : în acest caz putem spune cu certitudine că înainte de executarea lui Q tot ceea ce implică P va fi și adevărat.

În mod formal, putem scrie regula inferenței ca:

{\frac {P^{\prime }\rightarrow \ P\ ,\ \lbrace P\rbrace \ Q\ \lbrace R\rbrace \ ,\ R\rightarrow \ R^{\prime }}{\lbrace P^{\prime }\ \rbrace \ Q\ \lbrace R^{\prime }\rbrace }}

{\ displaystyle {\ frac {P ^ {\ prime} \ rightarrow \ P \, \ \ lbrace P \ rbrace \ Q \ \ lbrace R \ rbrace \, \ R \ rightarrow \ R ^ {\ prime}} {\ lbrace P ^ {\ prime} \ \ rbrace \ Q \ \ lbrace R ^ {\ prime} \ rbrace}}}

{\ displaystyle {\ frac {P ^ {\ prime} \ rightarrow \ P \, \ \ lbrace P \ rbrace \ Q \ \ lbrace R \ rbrace \, \ R \ rightarrow \ R ^ {\ prime}} {\ lbrace P ^ {\ prime} \ \ rbrace \ Q \ \ lbrace R ^ {\ prime} \ rbrace}}}

Conceptul exprimat de această regulă se numește cea mai slabă precondiție sau cea mai puternică postcondiție datorită faptului că putem generaliza efectiv în cazul unui adevăr care precede fragmentul și să ne specializăm în cazul unui adevăr ulterior.

Regula pentru succesiunea comenzilor

În general, într-un limbaj de programare, avem un operator folosit pentru a exprima concatenarea între instrucțiuni multiple. Alegem punctul și virgula și presupunem două instrucțiuni în ordine $<C_{1};C_{2}>$ ${\ displaystyle <C_ {1}; C_ {2}>}$ ${\ displaystyle <C_ {1}; C_ {2}>}$ .

Regula prevede că:

{\frac {\{P\}\ C_{1}\ \{P'\}\ ,\ \{P'\}\ C_{2}\ \{P''\}}{\{P\}\ <C_{1};C_{2}>\ \{P''\}}}

{\ displaystyle {\ frac {\ {P \} \ C_ {1} \ \ {P '\} \, \ \ {P' \} \ C_ {2} \ \ {P '' \}} {\ { P \} \ <C_ {1}; C_ {2}> \ \ {P '' \}}}}

{\ displaystyle {\ frac {\ {P \} \ C_ {1} \ \ {P '\} \, \ \ {P' \} \ C_ {2} \ \ {P '' \}} {\ { P \} \ <C_ {1}; C_ {2}> \ \ {P '' \}}}}

Putem astfel evalua adevărul unei secvențe de instrucțiuni care caută predicate adevărate între una și cealaltă și apoi compunem treptat proprietățile pe care le căutăm pentru un fragment compus din mai multe operații care trebuie efectuate. Avem asta dacă este adevărat $P.$ ${\ displaystyle P}$ $P.$ inainte de $C_{1}$ ${\ displaystyle C_ {1}}$ $C_ {1}$ și contează ${P.}^{″}$ ${\ displaystyle P ''}$ ${\ displaystyle P ''}$ după $C_{2}$ ${\ displaystyle C_ {2}}$ $C_ {2}$ dacă găsim ${P.}^{'}$ ${\ displaystyle P '}$ $P '$ fi adevărat mai târziu $C_{1}$ ${\ displaystyle C_ {1}}$ $C_ {1}$ si inainte $C_{2}$ ${\ displaystyle C_ {2}}$ $C_ {2}$ putem deduce condițiile întregii secvențe.

Rețineți că, în acest caz, am folosit parantezele și virgulele pentru a defini succesiunea operațiilor multiple, dar raționamentul este evident aplicabil oricărui operator.

Regula de iterație

Comanda iterativă se execută dacă și numai dacă valoarea expresiei E este validă. Când se execută comanda C, nu se știe a priori câte cicluri vor fi necesare pentru ca valoarea expresiei să nu mai fie satisfăcută. Astfel, trebuie să existe o afirmație, invarianta , care este adevărată, indiferent de numărul de cicluri. Mai mult, înainte de a executa comanda iterativă, este necesar să se verifice dacă expresia E este bine definită (trebuie să dea naștere unei valori, număr sau boolean). Iterația se va termina atunci când valoarea expresiei E este falsă. Deci vom avea un triplu de acest tip

\{Inv\land E\}\ {\textbf {while}}\ E\ {\textbf {do}}\ C\ {\textbf {done}}\ \{Inv\land \sim E\}

{\ displaystyle \ {Inv \ land E \} \ {\ textbf {while}} \ E \ {\ textbf {do}} \ C \ {\ textbf {done}} \ \ {Inv \ land \ sim E \} }

{\ displaystyle \ {Inv \ land E \} \ {\ textbf {while}} \ E \ {\ textbf {do}} \ C \ {\ textbf {done}} \ \ {Inv \ land \ sim E \} }

În ceea ce privește comanda C, înainte de a fi executată, este necesar să se verifice dacă atât invariantul cât și expresia E. sunt valabile. Expresia E este bine definită (ipoteza invarianței):

\{Inv\land E\}\ C\ \{Inv\land def(E)\}

{\ displaystyle \ {Inv \ land E \} \ C \ \ {Inv \ land def (E) \}}

{\ displaystyle \ {Inv \ land E \} \ C \ \ {Inv \ land def (E) \}}

În plus față de ipoteza invarianței, comanda iterativă include alte două ipoteze care trebuie verificate înainte de a putea spune că un triplu iterativ este corect: ipoteza terminării și ipoteza progresului.

Ipoteza încetării servește pentru a garanta încetarea unui triplu:

Inv\Rightarrow t\geq 0

{\ displaystyle Inv \ Rightarrow t \ geq 0}

{\ displaystyle Inv \ Rightarrow t \ geq 0}

unde t este o funcție de terminare care servește pentru a garanta iterația până când expresia E este satisfăcută.

În ipoteza progresului înainte de executarea comenzii C se verifică că invarianța deține, expresia E că t = V, unde V se numește variabilă de specificație. După executarea comenzii, valoarea funcției de terminare este comparată cu cea a variabilei de specificație V.

\{Inv\land E\land t=V\}\ C\ \{t<V\}

{\ displaystyle \ {Inv \ land E \ land t = V \} \ C \ \ {t <V \}}

{\ displaystyle \ {Inv \ land E \ land t = V \} \ C \ \ {t <V \}}

Bibliografie

Mordechai Ben-Ari, Mathematical Logic for Computer Science , Londra, Springer, 1993, ISBN 978-1-4471-4128-0 .
Paolo Mancarella, Note despre semantica axiomatică ( PDF ), p. 78. Accesat la 6 februarie 2016 .

Controlul autorității	GND ( DE ) 4343105-7

Portal IT

Portalul de matematică