Hoarelogica

Hoarelogica is een rekenmethode in de informatica die gebruikt wordt ter afleiding van programma's. Ze is vernoemd naar de bedenker van de basis van het mechanisme, Tony Hoare.

Inhoud 1 Hoarelogica en predicatencalculus 2 Hoaretriples en de informatica 3 De zwakste (vrije) preconditie 4 Bronnen

[bewerk] Hoarelogica en predicatencalculus

Hoarelogica is een toepassing van de predicatencalculus op de ontwikkeling van programma's.

In 1937 publiceerde Alan Turing een model van berekening, een Turingmachine genaamd. Dit theoretische mechanisme beschrijft op een zeer mechanische manier hoe een berekening uitgevoerd wordt, in termen van zeer kleine stappen die van een beginsituatie tot een eindsituatie leiden.

Rond 1968 bedacht Tony Hoare dat Turings idee betekende dat je ook op een andere manier naar een berekening kon kijken dan eerder altijd gedaan werd. Een berekening werd altijd beschouwd in termen van "Wat moet je doen?" of "Hoe moet je het doen?". Maar, zo bedacht Hoare, de verdeling in kleine stappen door Turing betekent dat er meer is aan een berekening dan alleen een begin, een eind en een aantal uit te voeren handelingen: er zijn (mogelijk heel veel) punten in de berekening die tussen opeenvolgende handelingen liggen. Bedenk maar zelf: als je eerst A moet uitvoeren en daarna B, dan is er een moment waarop je A uitgevoerd hebt maar nog niet aan B begonnen bent.

Hoare realiseerde zich echter niet alleen dat een berekening uit stappen met momenten-tussen-stappen bestaat, hij realiseerde zich ook dat het mogelijk was die momenten-tussen-stappen op een wiskundige manier te beschrijven. Het is bij iedere berekening mogelijk de momenten tussen stappen in de berekening een wiskundige beschrijving mee te geven. En niet zomaar een beschrijving, maar een beschrijving in termen van een logische uitspraak over de variabelen die in de berekening gebruikt worden – de waarden van die variabelen, maar ook de relaties tussen variabelen (zoals a < b, c + d = 0, etc.).

In 1969 publiceerde Hoare een artikel getiteld An axiomatic basis for computer programming. In dit artikel introduceerde hij een aantal ideeën die de informatica radicaal veranderden en in één klap een wetenschap met een zware, wiskundige basis maakten van wat eerder een vakgebied was dat half uit gokwerk bestond. Hoares visie kwam in het kort op het volgende neer:

1. Iedere berekening, ieder programma, bezit een toestandsruimte.
2. De toestandsruimte van een gegeven berekening is een echte vectorruimte, die opgespannen wordt door de variabelen van de berekening.
3. Iedere berekening bestaat - volgens het Turingmodel - uit een aantal stappen . Iedere stap wijzigt de waarde van tenminste één variabele van het programma en is dus op te vatten als een vector in de toestandsruimte van het programma.
4. Iedere vector, iedere stap in het programma, is een overgang van een punt in de toestandsruimte naar een ander punt (de bovengenoemde momenten-tussen-stappen); ieder punt kan beschreven worden met een logische uitspraak, een predicaat.
5. Ieder programma is dus feitelijk een serie vectoren, of ook wel een wandeling door de toestandsruimte; een dergelijke wandeling kan genoteerd worden als .
6. Iedere stap binnen een programma of berekening wordt volledig beschreven door het triple {T_k}S_k{T_{k + 1}} – de verificatie van de correctheid van een dergelijke stap is mogelijk als je alleen die drie zaken weet, zelfs zonder te weten hoe je in toestand T_k terechtgekomen bent. Het is genoeg te weten dat je in die situatie begint om te kunnen zien of het geheel correct is.

De volledige beschrijving van een stap van Hoare wordt tegenwoordig, ter ere van Tony Hoare, een Hoaretriple genoemd. Deze triples worden op generieke wijze genoteerd als

{P}S{Q}

met als semantiek:

Stel dat een stap S gestart wordt in een initiële toestand (een preconditie) P. Als S eindigt, dan is de resulterende toestand (de postconditie) toestand Q.

[bewerk] Hoaretriples en de informatica

De laatste stap uit het lijstje hierboven was als een soort bom die in de informatica afging, zo groot waren de gevolgen van het inzicht dat Hoare gehad had.

Tot op het moment van Hoares publicatie had de informatica meer en meer geworsteld met de complexiteit van het aantonen van correctheid van programma's. Programmacorrectheid met een wiskundig bewijs was vaak een lastige klus waar complexe argumenten in gingen zitten. En steeds complexer wordende computerprogramma's maakten de zaak er niet beter op – een computerprogramma kan vertakkingen (selectiestatements) in zijn berekening bevatten, of herhalingen, wat betekent dat een bewijs van correctheid iets moet zeggen over mogelijk oneindig veel verschillende berekeningen die een programma zou kunnen uitvoeren.

Maar nee, zei Hoare, niets van dat alles: je kunt de correctheid van een programma bewijzen door statement voor statement, handeling voor handeling, stap voor stap, te kijken naar de correctheid van iedere stap op zich. Iedere stap begint in een toestand. Iedere stap die eindigt, eindigt in een toestand. Als dat bewijsbaar de toestand is waarin je dacht dat de stap zou eindigen, dan is die stap correct. Als een programma bestaat uit stappen die allemaal correct zijn, dan kan het programma correct zijn. Als iedere correcte stap eindigt in een toestand die ook nog eens de verwachte begintoestand van de volgende, correcte stap is, dan is het programma correct. Zo simpel is het en je hoeft niet alle, mogelijk oneindig veel, mogelijke berekeningen na te lopen die een programma kan doen om de correctheid van dat programma aan te tonen.

De volgende stap was zo mogelijk nog groter dan de vorige en kwam met behulp van Edsger Dijkstra en zijn studenten tot stand. Zij vroegen zich namelijk het volgende af:

Het is mooi dat je de correctheid van een programma kunt verifiëren door het programma te beschouwen als een wandeling door de toestandsruimte. Maar stel nou dat je er andersom naar kijkt. Je hebt een toestandsruimte, je hebt een punt in die ruimte die je de begintoestand noemt, en een punt die je de eindtoestand noemt. Zou je nu een wandeling van de begintoestand naar de eindtoestand kunnen uitrekenen, zodat het resultaat een werkend programma is?

En het antwoord was ja. Met behulp van een aantal rekenregels, de predicatencalculus en je eigen creativiteit om de zaak een bepaalde richting op te sturen, kun je een programma uitrekenen dat een gegeven probleem oplost en zeker correct moet zijn (of aantonen dat een dergelijk programma niet kan bestaan).

[bewerk] De zwakste (vrije) preconditie

Tussen 1969 en 1975 werkten mensen als Hoare en Dijkstra aan de ontwikkeling van een calculus om programma's mee uit te rekenen. Als onderdeel van dat werk ontwikkelden zij allerlei wiskundige hulpmiddelen, waaronder verfijningen van de betekenis van Hoares triples om de complexiteit het hoofd te bieden.

Een belangrijke stap was het inzicht dat het Hoaretriple eigenlijk vaak te streng is om bewijzen mee te kunnen leveren. Als je een brug wilt slaan tussen de toestanden P en Q, dan is het vaak te moeilijk om een stap te bedenken die een dergelijke brug vormt. Soms kan dat opgelost worden door meerdere stappen te nemen (bijvoorbeeld door te splitsen, waardoor je iets krijgt als {P}S₀{P'}S₁{Q}. Maar soms is het gewoon echt te moeilijk, omdat P te strenge eisen stelt (we zeggen dan: P is te sterk).

Gelukkig hoef je niet altijd direct een brug te slaan. Hoare wilde graag dat de betekenis van zijn triple was dat als je vanuit P aan S begint en S eindigt, dan eindigt S in een toestand Q. Dijkstra bedacht dat je dan natuurlijk ook voor iedere, mogelijke, stap vanuit een of andere Q kon bedenken wat de minste (of zwakste) preconditie was die je nodig had om dat te bereiken. Dit werd de zwakste vrije preconditie (weakest liberal precondition) genoemd. De notatie hiervoor werd

wlp.S.Q

en de betekenis was

wlp.S.Q "absoluut de zwakste toestand zodanig dat {wlp.S.Q}S{Q}"

En daarmee was een groot probleem opgelost, want als je kon bewijzen dat

dan volgde daar ook direct {P}S{Q} uit. En omgekeerd ook, als je moeite had met de aansluiting op het volgende statement:

.

Met deze kennis in de hand werd het mogelijk een calculus op te stellen gebaseerd op de zwakste vrije precondities van alle soorten stappen die gezet konden worden:

Het lege statement of de skip

De toekenning

(R met daarin alle voorkomens van x vervangen door E)

De sequentiële compositie

Het selectiestatement

Het repetitiestatement

Bron(nen):

On a method of multiprogramming W.H.J. Feijen en A.J.M. van Gasteren Springer Verlag New York, 1999 ISBN 0-387-98870-X Predicate calculus and program semantics E.W. Dijkstra en C.S. Scholten Springer Verlag, 1990 ISBN 0-387-96957-8