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 trojicaUpraviť

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

 

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ómyUpraviť

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

Axióma prázdneho príkazuUpraviť

 

Axiomatická schéma priradeniaUpraviť

 

Inferenčné pravidláUpraviť

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

Kompozičné pravidloUpraviť

 

Alternatívne pravidloUpraviť

 

Iteratívne pravidloUpraviť

 

Pravidlo následkuUpraviť

 

ZdrojUpraviť

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