De noodzaak tot absolute correctheid

Onzorgvuldig ontwerpen van software kan rampzalig uitpakken. In zijn NWO-Huygenslezing pleit de Britse theoretisch informaticus Tony Hoare voor een gedisciplineerdere analyse van computerprogrammatuur. `Een helder, expliciet concept maken, dat levert rendement op.'

De NWO-Huygenslezing van prof.dr. Tony Hoare is, samen met die van co-referent prof.dr. Jan Bergstra, op aanvraag te verkrijgen bij NWO, afdeling Voorlichting & Communicatie, postbus 93138, 2509 AC Den Haag; fax 070-3850971; email: news@nwo.nl.

TONY HOARE (1934), hoofd van het Computing Laboratory van de Universiteit van Oxford — en voor de kenners: uitvinder van de quicksort-routine — is een opmerkelijk wetenschapper van het type waar Engeland het patent op lijkt te hebben. Een tengere gestalte, getooid met een academisch baardje en een onmodieus zwart brilmontuur, waarachter een paar vriendelijke, schrandere ogen. Een aimabele classicus uit Oxford bovendien, die via Plato in de logica, de wiskunde, en uiteindelijk in de wereld van de software verzeild raakte. Daar geniet hij een strenge reputatie als ijveraar voor gedisciplineerde en zorgvuldige analyse van software op logisch-mathematische grondslag, iets wat hem vooral in de wildere buitengewesten van de vooral praktisch ingestelde gemeenschap van programma-ontwikkelaars niet altijd even populair heeft gemaakt. Toch is Hoare allerminst een monomaan mathematicus, maar juist iemand die gedreven wordt door heel praktische motieven.

KLEINE AANPASSING

``Neem nu het millenniumprobleem', zegt hij. ``Daarvoor is de basis gelegd in een tijd dat een geheugenplaats nog echt geld kostte en toegangstijden voor geheugens gemeten werden in milliseconden, in plaats van, zoals nu, in micro- of zelfs nanoseconden. Natuurlijk ging men daar spaarzaam mee om. Maar men had kunnen voorkomen dat het ooit een serieus probleem zou worden als men in die tijd meer aandacht besteed had aan de manier waarop programmeertalen werden opgebouwd. Had er in COBOL zoiets als strikte type-checking bestaan, de dwang om van elke variabele expliciet aan te geven om wat voor soort gegeven het ging, bijvoorbeeld een geheel getal, een datum, een reëel getal, dan hadden we nu niet al die miljarden programmaregels stuk voor stuk hoeven doorvlooien. Een kleine aanpassing in de compiler, het programma dat zorgt dat de programmaregels in machinecode vertaald worden, was voldoende geweest, omdat die dan automatisch wist welke van die ontelbare nullen en enen waaruit een programma uiteindelijk bestaat een datum voorstelden.'

Voorkomen, dat is een sleutelwoord in Hoare's kijk op programmeren. Een gedegen analyse van wat je eigenlijk wilt voordat je ook maar een regel op papier zet, voorkomt niet alleen heel wat problemen later, maar kan naar zijn vaste overtuiging ook een bron van inspiratie zijn: ``Zo kun je elegante, welbegrepen ontwerpen van een programma maken, zelfs van programmeertalen, nog voordat je het product feitelijk gaat bouwen. Dat inspireert programmeurs om niet zomaar het eerste het beste idee dat in hun hoofd opkomt te accepteren. En vooraf de zaken netjes houden, een helder, expliciet concept maken, dat levert rendement op.

``Toch gaat het maar zelden zo. In de computerij is tijd nu eenmaal geld. Het is van het grootste belang om snel met een product op de markt te zijn, liefst als eerste. Dus wordt er ontworpen op basis van `net goed genoeg'. Dat heeft bovendien het voordeel dat je, mits je er tenminste geen compleet onontwarbare kluwen van maakt, alweer gauw een nieuwe, verbeterde versie van je programma op de markt kunt brengen. Sommige bedrijven gebruiken die strategie zelfs opzettelijk.'

Zorgvuldige analyse vooraf past daar slecht bij, want het kost tijd. En zo ontstond de gebruikelijke, van de traditionele industrie afgekeken ontwikkelmethode waarbij een product eerst gebouwd wordt, en daarna proefondervindelijk getest. Die methode is Hoare een doorn in het oog, omdat materiële producten, of het nu ijskasten zijn, wollen dekens of chocoladerepen, fundamenteel verschillen van computerprogramma's. Bij materiële producten dient het testen vooral om de grenzen te vinden waarbinnen het product veilig en naar tevredenheid functioneert, zoals de hoogste en laagste temperatuur waarbij een chocoladereep een bepaalde tijd bewaard kan worden, of de fluctuaties in de netspanning die de voeding van de ijskast kan verwerken. Het gaat dus uiteindelijk om eigenschappen van materialen. Ingenieurs doen steekproeven om die grenzen te vinden, en doorgaans geldt dat het gedrag van het product tussen die grenswaarden min of meer regelmatig en gelijkmatig verloopt: een reep die bij 10 graden Celsius en bij 23 graden Celsius goed blijft, zal dat ook bij 17,3 graden Celsius doen.

Maar bij computerpogramma's is dat niet zo. Die bestaan uit getallen, en die hebben geen materiaaleigenschappen. Je kunt dan ook testen wat je wilt, dat zegt helemaal niets over het optreden van fouten bij de eerste de beste toevallig optredende toestand die je niet getest hebt. En dat kan slecht uitkomen, zegt Hoare: ``Er zijn tot nu toe gelukkig nog maar weinig mensen omgekomen door dat soort ongelukken, maar er is wel al aanzienlijke economische schade aangericht. De eerste Ariane 5-raket, bijvoorbeeld, viel binnen een halve minuut uit de lucht door een miniem, onopgemerkt foutje in het programma dat de koers moest bepalen. Een paar jaar geleden viel het hele AT&T telefoonnet in Amerika negen uur lang uit door net zo'n foutje in de programmatuur van de schakelpunten in het net. Dat kost groot geld. Tragischer waren de ongelukken met de Therac 25, een medische röntgen-bestralingsmachine die door ongedetermineerdheid in de programmatuur patiënten soms een honderd maal grotere dosis straling toediende dan de bedoeling was, zonder dat iemand dat kon zien.'

COMPROMIS

Steekproeven met het kant en klare programma kunnen dat soort rampen nooit voorkomen, stelt Hoare. Maar het kan wel door het ontwerp van het programma netjes volgens de wetten van de logica en de wiskunde op te zetten, omdat je zo kunt bewijzen hoe het programma zich onder alle omstandigheden zal gedragen, zonder enige uitzondering. Dat is wat Hoare bedoelt als hij zegt dat programmeren wetenschappelijker moet worden.

``Onze taak, als onderzoekers, is daarbij uiteraard om te streven naar het maximum. Naar absolute correctheid. In de praktijk bestaat natuurlijk geen perfectie. Ingenieurs en programmeurs moeten altijd een compromis maken met de realiteit, en gelukkig kan dat ook. Maar wij, als onderzoekers, moeten dat maximum proberen te bereiken. Wij zijn er om praktijkmensen middelen te geven waar ze zonder meer op kunnen bouwen. Kijk, wiskundigen doen in zuivere getallen, en daarvan zijn er oneindig veel. We weten allemaal dat getallen nooit opraken, er is altijd weer een groter getal. Maar de oude Grieken waren daar helemaal niet zo zeker van. Voor zover zij wisten, konden ze best eens tegen het laatste getal aanlopen. Die vrees verdween pas toen Archimedes met zijn getallenstelsel bewéés dat er een oneindige voorraad was. En zo is het nog altijd. Pas als wij, de theoretici, aantonen dat er geen grenzen zijn, kunnen de praktijkmensen gerust zijn dat ze net zo ver kunnen gaan als nodig is.

``Er bestaat overigens nog helemaal niet zoiets als een geverifieerde bewijsprocedure voor complete programma's. Dat hoeft gelukkig ook niet meteen. Waar het om gaat is het ontwikkelen van proeven van correctheid van kleine onderdelen, die tezamen de juistheid van het geheel kunnen garanderen. Het is al heel wat als we zo expliciet mogelijk zijn over de eigenschappen van de belangrijkste op elkaar inwerkende programmaonderdelen. Met precieze, duidelijke beschrijvingen van het gedrag van die onderdelen kun je berekenen hoe het geheel zich zal gedragen. En als de onderdelen maar klein genoeg zijn, komen we een heel eind, want mensen zijn behoorlijk goed in het schrijven van betrouwbare kleine eenheden.'

Hoare pleit daarom voor top-down ontwerpen. Niet zomaar ergens een stukje beginnen te programmeren, en de rest er zo goed en zo kwaad als het gaat aanbreien, maar eerst terdege boven water krijgen wat precies de bedoeling is, en dan van groot naar klein uitwerken, tot aan die kleine, betrouwbare onderdelen. Dat zorgt voor betrouwbaarheid, en meteen voor de nodige flexibiliteit. ``Zo krijg je programma's die je kunt aanpassen aan veranderde omstandigheden. Als je precies weet hoe ze in elkaar steken, weet je ook hoe hun gedrag bij wijziging zal veranderen. En omstandigheden veranderen nu eenmaal. Kijk maar naar de telefoon. Ooit was één lijn gelijk aan één nummer, één abonnee en één toestel. Dat is allemaal veranderd: er zijn abonnees met tientallen lijnen, en lijnen waar tientallen abonnees op zitten, en zo voort. En steeds is de software van het telefoonsysteem aangepast zonder ooit uit bedrijf genomen te worden. Dat is een knappe prestatie, maar het is wel een wankel kaartenhuis geworden. Echt erg wordt het pas als het zover komt dat je de programmatuur wel moet, maar eigenlijk niet meer kúnt aanpassen, omdat niemand meer weet hoe het werkt. Dat is de kern van het millenniumprobleem waar we het al over hadden. Ook dan brengt trouwens de analytische, logisch-mathematische manier van werken uitkomst. Als je structuur moet gaan zoeken in een berg nullen en enen, kun je maar beter zo veel mogelijk bruikbare ideeën hebben over wat die nullen en enen zouden kunnen betekenen. En die ideeën levert de logica. Het is alleen wel een stuk arbeidsintensiever en duurder dan wanneer je dat denkwerk van te voren gedaan had.'

Ook al is Hoare's aanpak lang geen gemeengoed, hij wordt wel degelijk toegepast. Hoare: ``Dat gebeurt vooral daar waar veiligheid boven alles gaat. Als er bij uitval of foutieve werking grote bedragen of zelfs mensenlevens op het spel staan. Dat zijn vaak betrekkelijk kleine programma's, een paar duizend tot een paar honderdduizend regels, zoals bij de besturing van een kerncentrale.'

``In zo'n omgeving gaat correcte werking boven alles. Want ga maar na. Ik weet niet helemaal zeker of het ook echt is ingevoerd, maar in Amerika is naar aanleiding van de bijna-ramp met de centrale op Three Mile Island tenminste voorgesteld om te zorgen dat na een ongeluk de computer een half uur lang niet kan worden afgezet. Dat was omdat men uit onderzoek concludeerde, en waarschijnlijk terecht, dat het meeste gevaar veroorzaakt was door onjuiste reacties van het personeel. Door paniek. Hetzelfde gold toen de kruiser USS Vincennes in juli 1988 boven de Golf een Iraans lijnvliegtuig met 296 mensen aan boord uit de lucht schoot. Dat kwam hoofdzakelijk door de nerveuze stemming in de commandocentrale. De computer wist donders goed dat het niet om een F-14 ging, zoals de officieren dachten.

``Er zijn experimenten die hebben laten zien dat de productie van een rationele beslissing van een team mensen ligt rond 1 bit per half uur. Dat betekent: één doordachte ja/nee-beslissing in het eerste half uur nadat er een crisis uitbreekt. Dan begin je te begrijpen dat men liever de computer aan het roer zet, mits je absoluut aankan op de correctheid van de software.'

JUISTE INSTELLING

Wat geldt voor programma's, geldt evengoed voor programmeurs, meent Hoare: ``Het valt niet mee om voor dit soort pijnlijk nauwkeurig werk de juiste mensen te vinden. Dat is een van de redenen dat we in Oxford het afstudeerprogramma computerkunde hebben opgezet. Om mensen te kweken met de juiste instelling en het professionalisme om in zo'n omgeving te kunnen floreren. En dat vraagt wel wat. Westinghouse in Bath zocht bijvoorbeeld eens twee nieuwe programmeurs voor werk aan een beveiligingssysteem voor treinmachinisten. Die vonden ze na eindeloos selecteren en testen, maar binnen zes maanden waren ze allebei vertrokken: ze konden het tempo niet aan. Te langzaam. Tja, ze produceerden op die afdeling maar een paar honderd programmaregels per jaar. Maar die moesten uiteraard absoluut kloppen, dus nam men de tijd.

``Onze opleiding is dan ook ietwat onconventioneel, veel wiskundiger gericht dan gewoonlijk. Wij doen geen schitterende plaatjes en geen indrukwekkende multimedia-toestanden. Wij doen het werk dat niemand ziet, maar dat toch degelijk in elkaar moet zitten. Wij maken de gereedschappen waar de multimediamannen zonder kopzorg mee kunnen bouwen.

``Aan de andere kant', zegt hij serieus, ``heb je dat andere soort programmeurs, die wilde jongens, zeker ook nodig. In de spelletjesindustrie bijvoorbeeld. Niet alleen vanwege de enorme tijdsdruk, maar ook omdat daar achteraf proefondervindelijk testen noodzaak is. Visuele effecten, emotionele kracht, dat zijn dingen die je met geen enkele logica kunt bepalen. Dat moet je gewoon zien.'

Als we naar buiten lopen zegt hij, half tegen zichzelf en met een tikje verbazing in zijn stem: ``Tja, ik ben eigenlijk best wat milder geworden.'