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ť | 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
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]
Axiomatická schéma priradenia[upraviť | upraviť zdroj]
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]
Alternatívne pravidlo[upraviť | upraviť zdroj]
Iteratívne pravidlo[upraviť | upraviť zdroj]
Pravidlo následku[upraviť | upraviť zdroj]
Zdroj[upraviť | upraviť zdroj]
Tento článok je čiastočný alebo úplný preklad článku Hoare logic na anglickej Wikipédii.