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

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.