title: Hoarelogica
text: 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:
  ,
  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 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.
  
   
  
  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.
  
  Gevolgtrekkingsregel 
  Met de gevolgtrekkingsregel kan de preconditie van een hoaretripel worden versterkt of de postconditie verzwakt:
  
  Compositieregel 
  Met de compositieregel kan worden geredeneerd over programma's die uit meer dan een opdracht bestaan.
  
  Iteratieregel 
  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.
  
  Keuzeregel 
  Met de keuzeregel wordt geredeneerd over if-then-else-opdrachten.
  
  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  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.
  
  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.
  
  Logica in de informatica