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 upraviť
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ómy upraviť
Formálny systém Hoareovej logiky pozostáva z dvoch axióm:
Axióma prázdneho príkazu upraviť
Axiomatická schéma priradenia upraviť
Inferenčné pravidlá upraviť
Formálny systém Hoareovej logiky pozostáva z nasledujúcich inferenčných pravidiel:
Kompozičné pravidlo upraviť
Alternatívne pravidlo upraviť
Iteratívne pravidlo upraviť
Pravidlo následku upraviť
Zdroj upraviť
Tento článok je čiastočný alebo úplný preklad článku Hoare logic na anglickej Wikipédii.