Hoarelogica

Hoarelogica is een formele logica die in de informatica wordt gebruikt om over programma's te redeneren. Ze is vernoemd naar de bedenker van de basis van het mechanisme, Tony Hoare.

Hoaretripels en correctheid

Hoarelogica is een toepassing van de predicatencalculus op de ontwikkeling van programma's. De logica werd in 1969 door Tony Hoare in het artikel An axiomatic basis for computer programming geïntroduceerd. Aan de basis van de hoarelogica staat het hoaretripel:

$\{P\}\ S\ \{Q\}$,

waarin $P$ en $Q$ predicatenlogische formules zijn die een verzameling toestanden beschrijven en $S$ één of meer instructies is. Het hoaretripel $\{P\}\ S\ \{Q\}$ betekent, dat als een programma zich in een toestand bevindt waarin de conditie $P$ (de preconditie) geldt, en $S$ wordt uitgevoerd, het programma zich daarna in een toestand zal bevinden waarin de conditie $Q$ (de postconditie) geldt.

Een hoaretripel $\{P\}\ S\ \{Q\}$ is partieel correct wanneer het volgende geldt: als $P$ waar is in de huidige toestand, en $S$ wordt uitgevoerd, dan geldt in de toestand die optreedt nadat $S$ uitgevoerd is, $Q$. Het kan zijn dat $S$ nooit termineert, omdat $S$ in een oneindige lus terechtkomt ($S$ termineert dan niet). In dat geval bestaat er geen toestand na het uitvoeren van $S$, en kan $Q$ dus een willekeurige formule zijn.

Een hoaretripel $\{P\}\ S\ \{Q\}$ is volledig correct als hij partieel correct is en $S$ altijd termineert.

Bewijsregels van de hoarelogica

De hoarelogica bevat bewijsregels waarmee het mogelijk is partiële of volledige correctheid van een hoaretripel te bewijzen. In de oorspronkelijke bewijsregels werd een eenvoudige, sequentiële programmeertaal gebruikt, maar inmiddels zijn door anderen al vele uitbreidingen op de logica bedacht. Voor een eenvoudige programmeertaal die bestaat uit variabelen, toekenningen, voorwaardelijke sprongen (if then else) en lussen (while B do) bestaat de hoarelogica waarmee partiële correctheid kan worden bewezen uit de volgende bewijsregels (voor volledige correctheid is daarnaast een bewijs nodig, dat het programma altijd termineert):

Toekenningsaxioma

Met het toekenningsaxioma kan geredeneerd worden over variabeletoekenningen.

$\{P[x\backslash f]\}\ x{\mathrel {:=}}f\ \{P\}$

Hier staat $P[x\backslash f]$ voor de formule $P$ waarin alle voorkomens van de variabele $x$ worden vervangen door $f$. Met dit axioma kan bijvoorbeeld worden bewezen dat het hoaretripel $\{y>5\}\ x:=y\ \{x>5\}$ correct is.

Gevolgtrekkingsregel

Met de gevolgtrekkingsregel kan de preconditie van een hoaretripel worden versterkt of de postconditie verzwakt:

${\frac {P'\to P\quad \{P\}\ S\ \{Q\}\quad Q\to Q'}{\{P'\}\ S\ \{Q'\}}}$

Compositieregel

Met de compositieregel kan worden geredeneerd over programma's die uit meer dan een opdracht bestaan.

${\frac {\{P\}\ S\ \{Q\}\quad \{Q\}\ T\ \{R\}}{\{P\}\ S\mathop {;} T\ \{R\}}}$

Iteratieregel

Met de iteratieregel kan worden geredeneerd over lussen.

${\frac {\{P\land B\}\ S\ \{P\}}{\{P\}\ {\mbox{while }}B{\mbox{ do }}S\ \{P\land \lnot B\}}}$

In de bovenstaande regel is $B$ de lusvoorwaarde: als de lus termineert, dan is $B$ niet meer waar. De formule $P$ is een lusinvariant, een formule die altijd waar is net voordat en net nadat $S$ uitgevoerd wordt.

Keuzeregel

Met de keuzeregel wordt geredeneerd over if-then-else-opdrachten.

${\frac {\{P\land B\}\ S\ \{Q\}\quad \{P\land \neg B\}\ T\ \{Q\}}{\{P\}\ {\mbox{if }}B{\mbox{ then }}S{\mbox{ else }}T\ \{Q\}}}$

Zwakste precondities

Een bijdrage uit 1975 aan de hoarelogica, van Edsger W. Dijkstra, was het geven van zwakste precondities. De zwakste preconditie van een formule $Q$ met betrekking tot een programma $S$, geschreven ${\mathit {wp}}(S,Q)$, is de zwakste conditie $P$ (de conditie waar de grootste verzameling programmatoestanden aan voldoet) zodat $\{P\}S\{Q\}$ een volledig correcte hoaretripel is (dat wil onder andere zeggen, das $S$ termineert).

De zwakste preconditie kan als volgt worden uitgerekend:

• Toekenning:

${\mathit {wp}}(x:=f,Q)=Q[x\backslash f]$

• Sequentiële compositie:

${\mathit {wp}}(S\mathop {;} T,Q)={\mathit {wp}}(S,{\mathit {wp}}(T,Q))$

• Keuze:

${\begin{array}{lcr}{\mathit {wp}}({\text{if }}B{\text{ then }}S{\text{ else }}T,Q)&=&(B\to {\mathit {wp}}(S,Q))&\land &(\neg B\to {\mathit {wp}}(T,Q))\\&=&(B\land {\mathit {wp}}(S,Q))&\lor &(\neg B\land {\mathit {wp}}(T,Q))\end{array}}$

• Iteratie:

${\mathit {wp}}({\text{while }}B{\text{ do }}S,Q)=\exists k\,H_{k}$

waarbij

• $H_{0}=\neg E\land Q$
• $H_{k+1}=H_{0}\lor {\mathit {wp}}(S,H_{k})$

Hierbij is $H_{k}$ inductief gedefinieerd.

Literatuur

• C.A.R. Hoare. An axiomatic basis for computer programming (pdf). In: Communications of the ACM. 12(10): 576–585, 1969.
• W.H.J. Feijen en A.J.M. van Gasteren. On a method of multiprogramming. Springer Verlag, 1999.
• E.W. Dijkstra en C.S. Scholten. Predicate calculus and program semantics. Springer Verlag, 1990.