Logica lui Hoare

Versiunea actuală a paginii nu a fost încă examinată de colaboratori experimentați și poate diferi semnificativ de versiunea revizuită pe 15 iunie 2021; verificările necesită 2 modificări .

Logica Hoare ( ing. logica Hoare , de asemenea logica Floyd-Hoare , sau regulile Hoare ) este un sistem formal cu un set de reguli logice concepute pentru a dovedi corectitudinea programe de calculator . A fost propus în 1969 de informaticianul și logicianul matematician englez Hoare , dezvoltat ulterior de Hoare însuși și alți cercetători. [1] Ideea originală a fost propusă de Floyd , care a publicat un sistem similar [2 ] aplicat diagramelor de flux .

Hoare tripleți

Principala caracteristică a logicii lui Hoare este triplul Hoare . Triplul descrie modul în care execuția unei bucăți de cod schimbă starea calculului. Triplul Hoare are următoarea formă:

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

unde P și Q sunt aserțiuni și C este o comandă . _ _ P se numește precondiție ( antecedent ) iar Q se numește postcondiție ( consecință ). Dacă precondiția este adevărată, comanda face ca postcondiția să fie adevărată. Enunţurile sunt formule ale logicii predicatelor .

Logica lui Hoare are axiome și reguli de inferență pentru toate constructele unui limbaj de programare imperativ simplu . În plus față de aceste constructe descrise în lucrarea originală a lui Hoare, Hoare și alții au dezvoltat reguli pentru alte constructe: execuție concomitentă , apel de procedură , salt și pointer .

Ideea principală a lui Hoare este de a da fiecărei construcții a unui limbaj imperativ o pre- și postcondiție , scrisă ca o formulă logică. Prin urmare, în nume apare un triplu - precondiție , construcție a limbii, postcondiție .

Este clar că pentru un operator gol, pre- și postcondițiile coincid.
Pentru un operator de atribuire într-o postcondiție , pe lângă precondiția , trebuie luat în considerare faptul că valoarea variabilei s-a modificat.
Pentru o instrucțiune compusă (în Python este indentare, în C este {} ) avem un lanț de condiții pre- și post- . Ca rezultat, prima precondiție și ultima postcondiție pot fi lăsate pentru instrucțiunea compusă .
Regula de inferență spune că putem întări precondiția și slăbi postcondiția dacă avem nevoie de ea. Nu are sens să păstrezi întregul program un fel de declarație care nu ajută la rezolvarea problemei.
Declarație de ramură sau doar dacă . Poate fi împărțit condiționat în două ramuri: apoi și else . Dacă adăugăm adevărul condiției logice la precondiția (ce este sub dacă ), atunci după executarea ramurii then , ar trebui să urmeze postcondiția . În mod similar, dacă adăugăm negația unei condiții logice la precondiția (ce este sub if ), atunci după execuția ramurii else , postcondiția ar trebui să urmeze
operator de buclă. Acesta este cel mai non-trivial și complex, deoarece bucla poate fi executată de mai multe ori și nici măcar nu se poate termina. Pentru a rezolva problema posibilei repetări repetate a corpului buclei, se introduce invariantul buclei . Un invariant de buclă este ceva care este adevărat înainte de a se executa, este adevărat după fiecare execuție a corpului buclei și, prin urmare, este adevărat după sfârșitul buclei. Condiția preliminară pentru o instrucțiune de buclă este pur și simplu invarianta sa buclă . Dacă condiția de continuare a buclei este adevărată (ce este sub while ), atunci după execuția corpului buclei, ar trebui să urmeze adevărul invariantului buclei . Ca urmare, după încheierea ciclului, avem ca postcondiție adevărul invariantului ciclului și negația condiției pentru continuarea ciclului.
Operator de buclă cu corectitudine deplină. Pentru a face acest lucru, la paragraful anterior se adaugă o funcție de limitare, cu ajutorul căreia este ușor de demonstrat că bucla va fi executată de un număr limitat de ori. Îi sunt impuse condiții ca acesta să fie întotdeauna >=0, să scadă strict după fiecare execuție a corpului buclei și exact = 0 când bucla se termină.

Un program care funcționează bine poate fi scris în multe feluri și în multe cazuri va fi eficient. Această ambiguitate complică programarea. Pentru a face acest lucru, introduceți un stil. Dar acest lucru nu este suficient. Pentru multe programe (de exemplu, cele legate indirect de viața umană), este, de asemenea, necesar să se dovedească corectitudinea lor. S-a dovedit că dovada corectitudinii face programul mai scump cu un ordin de mărime (de aproximativ 10 ori).

Corectitudine parțială și deplină

În logica standard a lui Hoare, numai corectitudinea parțială poate fi dovedită, deoarece terminarea programului trebuie dovedită separat. De asemenea, regula de a nu folosi părți redundante de program nu poate fi exprimată în logica lui Hoare. Înțelegerea „intuitivă” a triplei Hoare poate fi exprimată astfel: dacă P apare înainte ca C să fie finalizat, atunci fie Q apare , fie C nu se va termina niciodată. Într-adevăr, dacă C nu se termină, nu există după, așa că Q poate fi orice instrucțiune. Mai mult, putem alege ca Q să fie fals pentru a arăta că C nu se va termina niciodată.

Corectitudinea deplină poate fi dovedită și folosind o versiune extinsă a regulii pentru instrucțiunea While .

Reguli

Axioma operatorului gol

Regula pentru o instrucțiune goală afirmă că instrucțiunea skip ( instrucțiune goală ) nu schimbă starea programului, deci o declarație care era adevărată înainte de skip rămâne adevărată după ce este executată.

{\frac {}{\{P\}\ {\textbf {săriți}}\ \{P\))}

Axioma operatorului de atribuire

Axioma operatorului de atribuire afirmă că după o atribuire, valoarea oricărui predicat în raport cu partea dreaptă a atribuirii nu se modifică odată cu înlocuirea părții drepte cu partea stângă:

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

Aici înseamnă expresia P în care toate aparițiile variabilei libere x sunt înlocuite cu expresia E . $P[E/x]$

Sensul axiomei de atribuire este că adevărul este echivalent după ce atribuirea a fost efectuată. Astfel, dacă a fost adevărat înainte de atribuire, conform axiomei de atribuire va fi adevărat după atribuire. În schimb, dacă a fost egal cu „fals” înainte de declarația de atribuire, ar trebui să fie egal cu „fals” după. $\{P[E/x]\}$ $\{P\}$ $\{P[E/x]\}$ $\{P\}$ $\{P[E/x]\}$ $\{P\}$

Exemple de triple valide:

$\{x+1=43\}\ y:=x+1\\{y=43\)$
$\{x+1\leq N\}\ x:=x+1\\{x\leq N\)$

Axioma de atribuire din formularea lui Hoare nu se aplică atunci când mai mult de un identificator se referă la aceeași valoare. De exemplu,

\{ y = 3\} \ x := 2\ \{y = 3 \}

este falsă dacă x și y se referă la aceeași variabilă, deoarece nicio precondiție nu poate asigura că y este 3 după ce x a fost atribuit 2.

Regula de compunere

Regula de compunere a lui Hoare se aplică executării secvențiale a programelor S și T , unde S este executat înainte de T , care este scris ca S;T .

{\frac {\{P\}\ S\ \{Q\}\ ,\ \{Q\}\ T\ \{R\}}{\{P\}\ S;T\ \{ R\}}}

De exemplu, luați în considerare două exemple ale axiomei de atribuire:

\{ x + 1 = 43\} \ y := x + 1\ \{y =43 \}

și

\{ y = 43\} \ z := y\ \{z = 43 \}

Conform regulii de compunere, obținem:

\{ x + 1 = 43\} \ y:=x + 1; z:= y\ \{z =43 \}

Regula operatorului condiționat

{\frac {\{B\wedge P\}\S\\{Q\}\ ,\\{\neg B\wedge P\}\T\\{Q\}}{\{P\ }\ {\textbf {dacă}}\ B\ {\textbf {atunci}}\ S\ {\textbf {altfel}}\ T\ {\textbf {endif}}\ \{Q\}}}

Regula de inferență

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

Regula instrucțiunii buclei

{\frac {\{P\wedge B\}\ S\ \{P\}}{\{P\}\ {\textbf {în timp ce}}\ B\ {\textbf {do}}\ S \ {\textbf {terminat}}\ \{\neg B\wedge P\}}}

Aici P este un invariant de ciclu .

Ciclul de regulă de declarație cu corectitudine deplină

{\frac {<\;{\text{este bine întemeiat,}}\;[P\wedge B\wedge t=z]\ S\ [P\wedge t<z]}{[P] \ {\textbf {în timp ce}}\ B\ {\textbf {do}}\ S\ {\textbf {terminat}}\ [\neg B\wedge P]}}

În această regulă, pe lângă păstrarea invariantului buclei, terminarea buclei este dovedită printr-un termen numit variabilă buclă (aici t ), a cărei valoare este strict redusă conform relației bine întemeiate " < " cu fiecare iterație. În acest caz, condiția B trebuie să implice că t nu este elementul minim al domeniului său, altfel premisa acestei reguli va fi falsă. Deoarece relația „ < ” este pe deplin întemeiată, fiecare pas de buclă este definit de membrii descrescători ai unei mulțimi finite ordonate liniar .

Notarea acestei reguli folosește paranteze pătrate, nu acolade, pentru a indica corectitudinea completă a regulii. (Acesta este o modalitate de a indica corectitudinea completă.)

Exemple

Exemplul 1

\{x+1=43\}\ y:=x+1\\{y=43\)

— pe baza axiomei atribuirii.

Deoarece , pe baza regulii de inferență, obținem:

( x + 1 = 43 \Leftrightarrow x = 42 )

\{x=42\}\ y:=x+1\ \{y=43\land x=42\}

Exemplul 2

\{x+1\leq N\}\ x:=x+1\\{x\leq N\)

— pe baza axiomei atribuirii.

Dacă x și N sunt numere întregi, atunci și pe baza regulii de inferență, obținem:

(x < N) \implica (x+1 \leq N)

\{x<N\}\ x:=x+1\ \{x\leq N\}

Vezi și

Link -uri

↑ CAR Hoare . „ O bază axiomatică pentru programarea computerelor Arhivat 17 iulie 2011 la Wayback Machine ”. Communications of the ACM , 12(10):576-580,583 octombrie 1969. doi : 10.1145/363235.363259
↑ RW Floyd . « Atribuirea cuvintelor programelor. Arhivat din original pe 9 decembrie 2008. (link în jos din 13-05-2013 [3444 zile] - istorie ) » (link descărcat) Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19-31. 1967.

Literatură

Guts AK Logica matematică și teoria algoritmilor. - M . : Casa de carte „LIBROKOM”, 2009. - 117 p. — ISBN 9785397000567 .
https://web.archive.org/web/20110123200456/http://djvu-student.narod.ru/02-matematicheskaya-logika/metodichka/metoda_matlogika_i_teor_algoritm_g6.html

În cataloagele bibliografice	GND : 4343105-7