CORRECTHEID

De NWO-Huygenslezing werd dit jaar gehouden door professor Tony Hoare van Oxford University. Het onderwerp was verificatietechnieken in informatica: hoe kunnen we zekerheid verkrijgen dat computerprogramma's in feite doen wat de bedoeling was dat ze deden.

In de W&O-bijlage van 31 oktober geeft Rik Smits een overzicht van de ideeen en het werk van professor Hoare over deze kwestie. Oppervlakkige lezing van Smits' artikel zou de indruk kunnen wekken dat die activiteiten geisoleerd staan. Het tegendeel is waar: het onderzoek aan het programmaverificatie vormt een hoofdrichting in de informatica.

Het belang van correctheidsbewijzen voor computerprogramma's werd reeds eind jaren veertig opgemerkt door A.M. Turing (1912-1954) naar wie de 'Nobelprijs' voor de informatica is genoemd: de Turing Award. In de context van de NWO-Huygenslezing en het artikel in NRC Handelsblad - waarin een en ander juist voor de lezers in dit land uiteengezet wordt - is het belangrijk dat de Nederlandse bijdrage niet ondergeschoffeld wordt.

In feite zijn de Nederlandse informatici hoofdspelers op dit gebied. In het bijzonder Edsger W. Dijkstra (Turing Award 1972; sinds 1984 werkzaam aan de Universiteit van Austin in Texas) geldt als de originator van het moderne fase van programmacorrectheid. Hij was een van de eerste voorstanders van het top-down-programmeren, introduceerde in het begin van jaren zeventig het begrip 'gestructureerd programmeren' en in zijn invloedrijk boek 'A Discipline of Programming' uit 1976 liet hij zien hoe de programma's samen met hun correctheidsbewijs systematisch ontwikkeld kunnen worden. Verder wees Dijkstra op 'go-to' als een foute programmeerconstructie die een correctheidsbewijs bemoeilijkt en het programmeerproces onnodig ingewikkeld maakt, en introduceerde hij programmeerconcepten (zoals 'semaphor') die gestructureerd parallel programmeren mogelijk maakten. Dijkstra is wereldwijd een van de bekendste informatici in dit genre.

Tony Hoare (Turing Award 1980) is vooral bekend door een uitvinden van de 'quicksort' sorteermethode (zoals vermeld door R. Smits), door het uitvinden van een belangrijke formele aanpak van correctheidsbewijzen, alsmede door een invloedrijke behandeling van synchronisatie en communicatie (met name door het introduceren van het begrip 'monitor') van parallelle en gedistribueerde programma's.

Het is nuttig op te merken dat de nu populaire internetprogrammeertaal Java geen 'go-to' statement bevat en dat zijn synchronisatie-methode gebaseerd is op de 'monitoren'.