23 sep 2025·7 min
Tony Hoare's ideeën over correctheid: van logica naar veilige code
Lees hoe Tony Hoare’s werk aan Hoare-logica, Quicksort en veiligheidsdenken praktische technieken vormde om correcte software te schrijven en te beoordelen.
Lees hoe Tony Hoare’s werk aan Hoare-logica, Quicksort en veiligheidsdenken praktische technieken vormde om correcte software te schrijven en te beoordelen.
Als mensen zeggen dat een programma “correct” is, bedoelen ze vaak: “Ik heb het een paar keer uitgevoerd en de uitvoer zag er goed uit.” Dat is een nuttig signaal—maar het is geen correctheid. In eenvoudige bewoordingen betekent correctheid dat het programma voldoet aan zijn specificatie: voor elke toegestane invoer produceert het het vereiste resultaat en houdt het zich aan regels over toestand, timing en fouten.
Het lastige is dat “voldoet aan de specificatie” moeilijker is dan het klinkt.
Ten eerste zijn specificaties vaak vaag. Een producteis kan zeggen “sorteer de lijst”, maar betekent dat stabiel sorteren? Wat met dubbele waarden, lege lijsten of niet-numerieke items? Als de specificatie het niet zegt, vullen verschillende mensen verschillende dingen in.
Ten tweede zijn randgevallen niet zeldzaam—ze worden alleen minder vaak getest. Null-waarden, overflow, off-by-one grenzen, ongebruikelijke gebruikerssequensen en onverwachte externe fouten kunnen van “het lijkt te werken” naar “het faalde in productie” leiden.
Ten derde veranderen eisen. Een programma kan correct zijn ten opzichte van de specificatie van gisteren en onjuist ten opzichte van die van vandaag.
Tony Hoare's belangrijkste bijdrage was niet de stelling dat we altijd alles formeel moeten bewijzen. Het was het idee dat we preciezer kunnen zijn over wat code moet doen—en er op een gedisciplineerde manier over kunnen redeneren.
In dit artikel volgen we drie verbonden draden:
De meeste teams zullen geen volledige formele bewijzen schrijven. Maar zelfs gedeeltelijk, “proof-stijl” denken maakt bugs makkelijker te vinden, reviews scherper en gedrag duidelijker voordat code wordt uitgebracht.
Tony Hoare is een van die zeldzame informatici wiens werk niet in papers of collegezalen bleef. Hij bewoog zich tussen academie en industrie en gaf om een praktische vraag die elk team nog steeds heeft: hoe weten we dat een programma doet wat we denken dat het doet—vooral als de inzet hoog is?
Dit artikel richt zich op een paar Hoare-ideeën die blijven terugkomen in echte codebases:
{P} C {Q}.Je zult hier geen diepe wiskundige formaliteiten vinden, en we zullen geen complete machine-controleerbare bewijsvoering van Quicksort proberen. Het doel is de concepten toegankelijk te houden: genoeg structuur om je redenering helderder te maken, zonder je code review in een graduate seminar te veranderen.
Hoare's ideeën vertalen naar gewone beslissingen: op welke aannames een functie vertrouwt, wat het garandeert aan callers, wat tijdens een lus waar moet blijven en hoe je “bijna correcte” wijzigingen tijdens reviews opmerkt. Zelfs als je nooit expliciet {P} C {Q} schrijft, verbetert denken in die vorm API's, tests en de kwaliteit van discussies over lastige code.
Hoare's kijk is strenger dan “het doorstond een paar voorbeelden”: correctheid gaat over het nakomen van een afgesproken belofte, niet over er goed uitzien op een kleine steekproef.
Bugs ontstaan vaak wanneer teams de middelste stap overslaan: ze springen van vereisten rechtstreeks naar code en laten de “belofte” vaag.
Twee verschillende claims worden vaak door elkaar gehaald:
Voor echte systemen kan “nooit eindigen” net zo schadelijk zijn als “eindigen met het verkeerde antwoord”.
Correctheidsverklaringen zijn nooit universeel; ze rusten op aannames over:
Expliciet zijn over aannames verandert “werkt op mijn machine” in iets waar anderen over kunnen redeneren.
Beschouw een functie sortedCopy(xs).
Een nuttig spec kan zijn: “Geeft een nieuwe lijst ys terug zodanig dat (1) ys oplopend gesorteerd is, en (2) ys bevat precies dezelfde elementen als xs (zelfde aantallen), en (3) xs blijft ongewijzigd.”
Nu betekent “correct” dat de code die drie punten onder de genoemde aannames naleeft—niet dat de uitvoer bij een snelle test er maar uit ziet als gesorteerd.
Hoare-logica is een manier om over code te spreken met dezelfde helderheid als een contract: als je begint in een toestand die aan bepaalde aannames voldoet, en je voert dit codefragment uit, dan eindig je in een toestand die aan bepaalde garanties voldoet.
De kernnotatie is de Hoare-triple:
{precondition} program {postcondition}
Een preconditie geeft aan wat waar moet zijn voordat het programmablokje draait. Dit gaat niet over wat je hoopt dat waar is; het gaat over wat de code nodig heeft.
Voorbeeld: stel een functie geeft het gemiddelde van twee getallen zonder overflow-checks terug.
a + b past in het integer-typeavg = (a + b) / 2avg is het wiskundige gemiddelde van a en bAls de preconditie niet geldt (overflow mogelijk), geldt de postconditie niet meer. De triple dwingt je dat hardop te zeggen.
Een postconditie stelt wat waar zal zijn nadat de code draait—ervan uitgaande dat de preconditie voldaan was. Goede postcondities zijn concreet en controleerbaar. Zeg in plaats van “resultaat is geldig” wat “geldig” betekent: gesorteerd, niet-negatief, binnen grenzen, ongewijzigd behalve voor specifieke velden, enz.
Hoare-logica schaalt van kleine statements naar meerstapscode:
x = x + 1, welke feiten over x zijn dan waar?Het punt is niet om overal accolades te zetten. Het is om intentie leesbaar te maken: duidelijke aannames, duidelijke uitkomsten en minder “het lijkt te werken”-gesprekken in reviews.
Een lusinvariant is een bewering die waar is voordat de lus begint, waar blijft na elke iteratie, en nog steeds waar is als de lus eindigt. Het is een simpel idee met veel winst: het vervangt “het lijkt te werken” door een claim die je daadwerkelijk bij elke stap kunt controleren.
Zonder invariant klinkt een review vaak als: “We itereren over de lijst en lossen geleidelijk dingen op.” Een invariant dwingt precisie af: wat is er nu al precies correct, ook al is de lus nog niet klaar? Zodra je dat duidelijk kunt zeggen, worden off-by-one fouten en missende gevallen makkelijker te zien, omdat ze zich voordoen op momenten waarop de invariant gebroken zou worden.
De meeste dagelijkse code kan een paar betrouwbare sjablonen gebruiken.
1) Grenzen / indexveiligheid
Houd indices in een veilige range.
0 <= i <= nlow <= left <= right <= highDit type invariant is uitstekend om out-of-range toegang te voorkomen en array-redenering concreet te maken.
2) Verwerkte vs. onverwerkte items
Splits je data in een “klaar” gebied en een “nog niet” gebied.
a[0..i) zijn onderzocht.”result is verplaatst voldoet aan de filter-predicaat.”Dit verandert vaardige voortgang in een duidelijke contractuele bewering over wat “verwerkt” betekent.
3) Gesorteerde prefix (of gepartitioneerde prefix)
Veelvoorkomend bij sorteren, mergen en partitioneren.
a[0..i) is gesorteerd.”a[0..i) zijn <= pivot, en alle items in a[j..n) zijn >= pivot.”Zelfs als de hele array nog niet gesorteerd is, heb je vastgelegd wat wél klopt.
Correctheid gaat niet alleen over gelijk hebben; de lus moet ook klaar komen. Een eenvoudige manier om dat te beargumenteren is een maat (variant) te benoemen die bij elke iteratie afneemt en niet oneindig kan blijven dalen.
Voorbeelden:
n - i neemt bij elke stap met 1 af.”Als je geen krimpende maat kunt vinden, heb je mogelijk een echt risico: een oneindige lus op sommige inputs.
Quicksort heeft een eenvoudige belofte: gegeven een fragment van een array herordent het elementen zodat ze in niet-afnemende volgorde eindigen, zonder waarden te verliezen of te verzinnen. De hoge-niveau vorm van het algoritme is makkelijk samen te vatten:
Het is een uitstekend voorbeeld voor correctheid omdat het klein genoeg is om te overzien, maar rijk genoeg om te laten zien waar informeel redeneren faalt. Een Quicksort die “er goed uitziet” op een paar willekeurige tests, kan nog steeds fouten bevatten die alleen in specifieke inputs of grensgevallen naar voren komen.
Een paar problemen veroorzaken de meeste bugs:
Om correctheid in Hoare-stijl te beargumenteren, splitst men het bewijs typisch in twee delen:
Deze scheiding houdt de redenering beheersbaar: maak partition goed, bouw de correctheid van sorteren daarop.
De snelheid van Quicksort hangt af van één schijnbaar klein onderdeel: partition. Als partition zelfs maar een beetje fout is, kan Quicksort verkeerd sorteren, eeuwig blijven lopen of crashen op randgevallen.
We gebruiken het klassieke Hoare partition-schema (twee pointers die naar binnen bewegen).
Input: een array-slice A[lo..hi] en een gekozen pivot-waarde (vaak A[lo]).
Output: een index p zodanig dat:
A[lo..p] is <= pivotA[p+1..hi] is >= pivotMerk op wat niet beloofd wordt: de pivot eindigt niet per se op positie p, en gelijke elementen mogen aan beide kanten voorkomen. Dat is oké—Quicksort heeft alleen een correcte splitsing nodig.
Terwijl het algoritme twee indices vooruitzet—i van links, j van rechts—richt goede redenering zich op wat al “vast staat”. Een praktische set invarianten is:
A[lo..i-1] zijn <= pivot (de linkerzijde is schoon)A[j+1..hi] zijn >= pivot (de rechterzijde is schoon)A[i..j] is ongeclassificeerd (nog te controleren)Als we A[i] > pivot en A[j] < pivot vinden, blijft het wisselen die invarianten behouden en krimpt het ongeclassificeerde midden.
i schuift naar rechts; partition moet toch termineren en een zinnige p teruggeven.j schuift naar links;zelfde terminatiezorg.< vs <=), kunnen pointers vastlopen. Hoare’s schema vertrouwt op een consistente regel zodat voortgang blijft plaatsvinden.Er bestaan verschillende partition-schemas (Lomuto, Hoare, three-way). Het belangrijkste is er één te kiezen, het contract te stellen en de code daar consequent tegen te reviewen.
Recursie is het makkelijkst te vertrouwen wanneer je twee vragen helder kunt beantwoorden: wanneer stopt het? en waarom is elke stap geldig? Hoare-stijl denken helpt omdat het je dwingt te zeggen wat waar moet zijn vóór een aanroep en wat waar zal zijn nadat deze terugkeert.
Een recursieve functie heeft minstens één basisgeval waarin ze geen verdere recursieve aanroepen doet en toch het beloofde resultaat levert.
Bij sorteren is een typisch basisgeval “arrays van lengte 0 of 1 zijn al gesorteerd.” Definieer “gesorteerd” expliciet: voor een orde-relatie ≤ is de output gesorteerd als voor elke index i < j geldt dat a[i] ≤ a[j]. (Of gelijke elementen hun oorspronkelijke volgorde behouden is een aparte eigenschap: stabiliteit; Quicksort is meestal niet stabiel tenzij je het speciaal ontwerpt.)
Elke recursieve stap moet zichzelf aanroepen op een strikt kleinere invoer. Deze “krimp” is je terminatieargument: als de grootte daalt en niet onder 0 kan komen, kun je niet eeuwig recursief blijven gaan.
Krimp is ook belangrijk voor stack-veiligheid. Zelfs correcte code kan crashen als de recursiediepte te groot wordt. Bij Quicksort kunnen onevenwichtige partitions diepe recursie veroorzaken. Dat is zowel een terminatiebewijs als een praktische herinnering om aan de slechtste-casus diepte te denken.
Quicksort’s worst-case tijd kan degraderen naar O(n²) bij zeer onevenwichtige partitions, maar dat is een prestatieprobleem — geen correctheidsfout. Het redeneringsdoel hier is: aangenomen dat de partitionstap elementen behoudt en splitst volgens de pivot, impliceert recursief sorteren van de kleinere delen dat het geheel gesorteerd is.
Testen en proof-stijl redeneren hebben hetzelfde doel—vertrouwen—maar bereiken dat op verschillende manieren.
Tests zijn uitstekend in het vangen van concrete fouten: een off-by-one, een gemist randgeval, een regressie. Maar een testsuite kan slechts een deel van de invoerruimte bemonsteren. Zelfs “100% coverage” betekent niet “alle gedrag gecontroleerd”; het betekent meestal “alle regels zijn uitgevoerd”.
Proof-stijl redeneren (met name Hoare-stijl) start vanuit een specificatie en vraagt: als deze precondities gelden, stelt de code dan altijd de postcondities veilig? Goed doen betekent niet alleen een bug vinden—je kunt vaak een hele categorie bugs uitsluiten (zoals “arraytoegang blijft binnen grenzen” of “de lus verlaat nooit de partition-eigenschap”).
Een heldere specificatie is een testgenerator.
Als je postconditie zegt “output is gesorteerd en is een permutatie van de invoer”, krijg je automatisch testideeën:
<= pivot aan de linkerkant).Het spec zegt wat “correct” betekent en tests controleren of de realiteit daarmee overeenkomt.
Property-based testing zit tussen bewijzen en voorbeelden in. In plaats van een paar gevallen handmatig te kiezen, formuleer je eigenschappen en laat je een tool veel inputs genereren.
Voor sorteren volstaan twee eenvoudige properties vaak:
Deze eigenschappen zijn in wezen postcondities geschreven als uitvoerbare checks.
Een lichtgewicht routine die schaalt:
Als je dit wilt institutionaliseren, maak dan “spec + redeneernotities + tests” onderdeel van je PR-template of reviewchecklist (zie ook /blog/code-review-checklist).
Als je een vibe-coding workflow gebruikt (code genereren vanuit een chatinterface), geldt dezelfde discipline—misschien wel meer. In Koder.ai kun je bijvoorbeeld in Planning Mode precondities/postcondities vastleggen voordat je code genereert, en vervolgens itereren met snapshots en rollback terwijl je property-based tests toevoegt. De tool versnelt implementatie, maar het spec houdt "snel" daartoe geen "fragiel".
Correctheid betekent dat een programma voldoet aan een afgesproken specificatie: voor elke toegestane invoer en relevante systeemtoestand levert het de vereiste uitvoer en bijwerkingen en behandelt het fouten zoals afgesproken. “Het lijkt te werken” betekent meestal dat je maar een paar voorbeelden hebt getest, niet de hele invoerruimte of de lastige grensgevallen.
Vereisten zijn het zakelijke doel in gewone taal (bijv. “sorteer de lijst voor weergave”).
Een specificatie is de precieze, controleerbare belofte (bijv. “geeft een nieuwe lijst terug, oplopend gesorteerd, met dezelfde multiset aan elementen, invoer ongewijzigd”).
De implementatie is de code. Bugs ontstaan vaak wanneer teams rechtstreeks van vereisten naar implementatie springen en de controleerbare belofte niet opschrijven.
Partial correctness: als de code terugkeert, is het resultaat correct. Total correctness: de code keert terug en het resultaat is correct — terminatie hoort dus bij de claim.
In de praktijk is total correctness belangrijk wanneer “altijd vastlopen” een zichtbare fout, resource-lek of veiligheidsrisico is.
Een Hoare-triple {P} C {Q} leest als een contract:
P (preconditie): wat waar moet zijn voordat C draaitPrecondities zijn wat de code nodig heeft (bijv. “indices binnen bereik”, “elementen vergelijkbaar”, “lock is gehouden”). Als een preconditie door callers geschonden kan worden, moet je óf:
Anders worden je postcondities wishful thinking.
Een lusinvariant is een bewering die waar is voordat de lus begint, die na elke iteratie waar blijft en die nog steeds waar is als de lus eindigt. Handige sjablonen:
0 <= i <= n)Als je geen invariant kunt formuleren, is dat een teken dat de lus te veel dingen tegelijk doet of dat de grenzen onduidelijk zijn.
Je noemt meestal een maat (variant) die bij elke iteratie afneemt en niet oneindig kan dalen, zoals:
n - i neemt met 1 afAls je geen dalende maat vindt, heb je mogelijk een echt risico op niet-terminatie (vooral bij duplicaten of vastlopende pointers).
In Quicksort is partition de kleine routine waar alles vanaf hangt. Als partition ook maar een beetje fout is, kun je krijgen:
Daarom helpt het om het contract van partition expliciet te maken: wat links waar moet zijn, wat rechts, en dat elementen alleen herschikt worden (een permutatie).
Duplicaten en de manier waarop je “gelijk aan pivot” behandelt zijn veelvoorkomende foutbronnen. Praktische regels:
i/j)Als duplicaten frequent zijn, overweeg three-way partitioning om zowel bugs als recursiediepte te verminderen.
Tests vangen concrete fouten op; redeneren kan hele categorieën bugs uitsluiten (bounds-veiligheid, behoud van invarianten, terminatie). Een praktische hybride werkwijze:
Voor sorteren zijn twee waardevolle properties:
CQ (postconditie): wat waar zal zijn nadat C klaar is, aangenomen dat P goldJe hoeft deze notatie niet letterlijk in code te schrijven — het gebruik van de structuur in reviews (“aannames in, garanties uit”) is het praktische voordeel.