Hoareova logika

z Wikipédie, slobodnej encyklopédie
Prejsť na: navigácia, hľadanie

Hoareova logika alebo Floydova-Hoareova logika je formálny systém logických pravidiel používaný pri verifikácii počítačových programov. Po prvýkrát s ním prišiel britský informatik a logik Charles Antony Richard Hoare v roku 1969, neskôr prešiel niekoľkými úpravami. Pôvodná myšlienka však siaha do prác Roberta Floyda, ktorý vyvinul podobný formálny systém pre vývojové diagramy.

Hoareova trojica[upraviť | upraviť zdroj]

Základným konceptom Hoareovej logiky sú tzv. Hoarove trojice, ktoré popisujú zmenu výpočtového stavu po vykonaní daného príkazu, prípadne programu. Hoarova trojica má tvar

\{P\}\;S\;\{Q\},

kde S je príkaz, P je tzv. vstupná podmienka a Q je výstupná podmienka. Uvedená Hoareova trojica znamená, že ak pred vykonaním príkazu S platila vstupná podmienka (istá logická formula) P, tak po vykonaní príkazu S bude platiť výstupná podmienka Q.

Axiómy[upraviť | upraviť zdroj]

Formálny systém Hoareovej logiky pozostáva z dvoch axióm:

Axióma prázdneho príkazu[upraviť | upraviť zdroj]

 \frac{}{\{P\}\ \textbf{skip}\ \{P\}} \!

Axiomatická schéma priradenia[upraviť | upraviť zdroj]

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

Inferenčné pravidlá[upraviť | upraviť zdroj]

Formálny systém Hoareovej logiky pozostáva z nasledujúcich inferenčných pravidiel:

Kompozičné pravidlo[upraviť | upraviť zdroj]

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

Alternatívne pravidlo[upraviť | upraviť zdroj]

\frac { \{B \wedge P\}\ S\ \{Q\}\ ,\ \{\neg B \wedge P \}\ T\ \{Q\} } { \{P\}\ \textbf{if}\ B\ \textbf{then}\ S\ \textbf{else}\ T\ \textbf{endif}\ \{Q\} } \!

Iteratívne pravidlo[upraviť | upraviť zdroj]

\frac { \{P \wedge B \}\ S\ \{P\} } { \{P \}\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ \{\neg B \wedge P\} }\!

Pravidlo následku[upraviť | upraviť zdroj]

 \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 }\!

Zdroj[upraviť | upraviť zdroj]

Tento článok je čiastočný alebo úplný preklad článku Hoare logic na anglickej Wikipédii.