Hoareova logika

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

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

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

Axióma prázdneho príkazu

$\frac{}{\{P\}\mathbf{\text{skip}}\{P\}}$

Axiomatická schéma priradenia

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

Inferenčné pravidlá

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

Kompozičné pravidlo

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

Alternatívne pravidlo

$\frac{\{B\wedge P\}S\{Q\},\{\mathrm{\neg }B\wedge P\}T\{Q\}}{\{P\}\mathbf{\text{if}}B\mathbf{\text{then}}S\mathbf{\text{else}}T\mathbf{\text{endif}}\{Q\}}$

Iteratívne pravidlo

$\frac{\{P\wedge B\}S\{P\}}{\{P\}\mathbf{\text{while}}B\mathbf{\text{do}}S\mathbf{\text{done}}\{\mathrm{\neg }B\wedge P\}}$

Pravidlo následku

$\frac{P^{\prime }\to P,\{P\}S\{Q\},Q\to Q^{\prime }}{\{P^{\prime }\}S\{Q^{\prime }\}}$