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 correctheidBewerken

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:

 ,

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

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

Een hoaretripel   is volledig correct als hij partieel correct is en   altijd termineert.

Bewijsregels van de hoarelogicaBewerken

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):

ToekenningsaxiomaBewerken

Met het toekenningsaxioma kan geredeneerd worden over variabeletoekenningen.

 

Hier staat   voor de formule   waarin alle voorkomens van de variabele   worden vervangen door  . Met dit axioma kan bijvoorbeeld worden bewezen dat het hoaretripel   correct is.

GevolgtrekkingsregelBewerken

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

 

CompositieregelBewerken

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

 

IteratieregelBewerken

Met de iteratieregel kan worden geredeneerd over lussen.

 

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

KeuzeregelBewerken

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

 

Zwakste preconditiesBewerken

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

De zwakste preconditie kan als volgt worden uitgerekend:

  • Toekenning:
 
  • Sequentiële compositie:
 
  • Keuze:
 
  • Iteratie:
 
waarbij
  •  
  •  
Hierbij is   inductief gedefinieerd.

LiteratuurBewerken

  • 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.