[oo] Correctheidsbewijzen

[Verwijderd]

Ik heb laatst een artikel gelezen van een programmeergoeroe op leeftijd (de naam is mij even ontschoten) die een fanatiek voorstander was van de functionele programmeertechniek, oo was volgens hem zwaar overschat. Als argument hiervoor gaf hij dat het toepassen van correctheidsbewijzen bij een object georienteerde programmeertechniek niet mogelijk is.

Er werd daarbij niet aangegeven waarom dit niet kan. Bij mijn opleiding ben ik in aanraking gekomen met correctheidsbewijzen bij een functionele benadering. Ik begrijp echter niet waarom dit (misschien een beetje aangepast) toegepast kan worden op een OO benadering.

Kan iemand hierover z'n licht schijnen?

[whoami]

Even een stomme vraag, maar wat houdt een 'correctheidsbewijs' precies in?

Is dat een bewijs die garandeerd dat de software geen bugs bevat ofzo?

* whoami heeft er nog nooit van gehoord.

[Verwijderd]

Correctheidsbewijzen zijn een methodiek om aan te tonen dat een method/functie doet wat hij moet doen bij een zekere input. je ziet ze in allerlei soorten en maten, veelal in de vorm van 'pre-/post condities'. Voor functionele talen is dit makkelijker, want de functie zelf omschrijf je in de taal met de taalconstructies. Maw: de functie's code is de omschrijving, en je kunt je correctheidsbewijs dan opsplitsen in het bewijzen van de correctheid van de functies die gebruikt worden in de functie in kwestie.

In imperatieve talen werk je niet met functies als elementen maar met statements. Op zich zou dat in theorie voldoende kunnen zijn, maar sommige talen, bv de talen die low level programming toelaten, laten toe dat men bv geheugen modificeert waar andere delen van een functie/method weer op werken. Het aantonen dat een method correct is, dwz doet wat hij moet doen bij een zekere input, is daardoor een lastig karwei, echter niet onmogelijk. De wat meer abstractere OO talen, zoals C# en Java, waarbij type safety voorop staat, kun je aantonen op statement niveau dat een zeker statement doet wat hij moet doen, en daardoor bewijzen dat een method correct is. Echter, het is wel tijdrovender dan bij functionele talen.

[RickN]

Die goeroe zou heel goed Dijkstra kunnen zijn.

whoami: Yep, dat is het idee ja. Je hebt een algoritme en daarvan bewijs je dat als aan de precondities van het algoritme wordt voldaan dan dan ook aan de postconditie van het algoritme wordt voldaan. Nog leuker is het om uitgaande van de postconditie een preconditie en algoritme af te leiden dat eraan voldoet waardoor de correctheid van je algoritme per constructie gegarandeerd is.

Ik geloof dat ik ook wel eens heb gehoord wat de topic starter zegt. Ik geloof dat het argument was dat de communicatie tussen componenten in oo qua complexiteit vergelijkbaar is met een parallel programma waardoor het bewijzen van de correctheid van een (sequentieel) programma net zo ingewikkeld wordt als van een parallel programma.

[Verwijderd]

[quote]RickN schreef op 07 augustus 2002 @ 11:12:
Die goeroe zou heel goed Dijkstra kunnen zijn.
quote]

Inderdaad!

[whoami]

Dat het moeilijker is om correctheidsbewijzen toe te passen bij OO programmering, daar kan ik in komen, maar dat is imho geen argument om te zeggen dat OO zwaar overschat is.

[Soultaker]

Een correctheidsbewijs is eigenlijk niet meer dan een bewijs dat een stuk code aan de door de programmeur opgestelde randvoorwaarden voldoet. Denk daarbij aan uitspraken als: de uitvoerwaarde is altijd kleiner dan 0, of: dit sorteeralgoritme doorloopt N^2 iteraties. Het meeest specifiek zijn uitspraken als: sin(x) levert de sinus van x op met een fout van maximaal 0.1%; maar dit is alleen formeel te bewijzen als je ook formeel kan vaststellen wat de 'sinus van x' nu eigenlijk is.

Het is niet zo dat het onmogelijk is om de correctheid van een methode in een OO taal te bewijzen; integendeel, dit is vaak zeer goed te doen. Het wordt alleen erg complex om dit ook in een volledig programma te doen. Dat is geen eigenschap van een OO taal; in een functionele taal wordt het bewijs (logischerwijs) ook moeilijker naar gelang de taal ingewikkelder wordt.

Een belangrijk verschil tussen functionele talen en gebruikelijke OO/imperatieve talen is echter, dat in het laatste geval van variabelen gebruik gemaakt wordt, die gewijzigd kunnen worden (destructive updating). In een functionele programmeertaal is dit onmogelijk en heeft elke functie dus uitsluitend met z'n eigen invoer en uitvoer te maken. Het is dan dus redelijk goed te doen, om van elke functie afzonderlijk de correctheid te bewijzen (aannemend dat de andere functies correct zijn) en daaruit te concluderen dat het gehele programma
correct werkt.

In een taal als C++ zal je er echter rekening mee moeten houden, dat bijvoorbeeld een object dat in de ene methode gebruikt wordt, in een andere (al dan niet tegelijkertijd) gewijzigd kan worden. Doordat de verschillende methoden (delen van) hun staat delen met andere methoden (van dezelfde klasse of uit andere klassen), moet bij het bewijzen van de correctheid van een enkele methode rekening gehouden worden met de rest van de applicatie. Het is nu dus heel erg moeilijk om het correctheidsbewijs op te delen in behapbare stukken en in de praktijk dus erg moeilijk zonder verdere aannames te doen.

Zeker geautomatiseerde bewijsvoeringen (waarbij de eigenschappen van procedures formeel worden gespecificeerd en met een speciaal voor dat doel ontwikkelde tool kunnen worden bewezen) zijn in (bijvoorbeeld) een object-georienteerde taal zeer moeilijk te realiseren.

Het is dus niet een kwestie van mogelijkheid/onmogelijkheid, maar meer een verschil in makkelijkheid (dat voorkomt uit een verschil in opzet). Ik denk dat software geschreven in functionele programmeertalen (zeker wanneer er een bewijs van de correctheid bij gegeven is) doorgaans aanzienlijk minder bugs bevat, maar dit kan ook komen doordat een applicatie ontwikkelen in een functionele programmeertaal dusdanig moeilijk is, dat je al een aardig goede ontwerper moet zijn om het voor elkaar te krijgen of tenminste gedwongen wordt om een goed ontwerp op te zetten.

_{Ik zie al weer dat iedereen me voor is geweest.}

[Verwijderd]

Hoe zie je OO dan in embedded systemen die tijdkritisch zijn (bv. beveiligingssystemen) waarbij bepaalde specificaties gegarandeert dienen te zijn (bv. responstijd)

[Soultaker]

RickN schreef op 07 augustus 2002 @ 11:12:
Die goeroe zou heel goed Dijkstra kunnen zijn.
Ik geloof dat ik ook wel eens heb gehoord wat de topic starter zegt. Ik geloof dat het argument was dat de communicatie tussen componenten in oo qua complexiteit vergelijkbaar is met een parallel programma waardoor het bewijzen van de correctheid van een (sequentieel) programma net zo ingewikkeld wordt als van een parallel programma.

Daarmee suggereer je dat het 'moeilijkheidsverschil' 'm in het verschil tussen seriele of parallelle executie zou zitten. Het klopt dat parallelle executie de zaken alleen maar ingewikkelder maakt, maar dat is niet het hele verhaal.

Het mooie van een functionele programmeertaal is juist, dat het compleet irrelevant is in hoeverre de executie parallel plaatsvind. Wat dat betreft zou elk functioneel programma in principe parallel uitgevoerd kunnen worden, zonder dat dat ook maar iets aan de 'ingewikkeldheid' verandert (de code blijft hetzelfde en het resultaat ook).

Als de stelling die de topicstarter naar voren brengt klopt, vermoed ik dat die ook opgaat voor een parallel uitgevoerd functioneel programma ten opzichte van een serieel uitgevoerd imperatief programma.

[Verwijderd]

Verwijderd schreef op 07 augustus 2002 @ 11:23:
Hoe zie je OO dan in embedded systemen die tijdkritisch zijn (bv. beveiligingssystemen) waarbij bepaalde specificaties gegarandeert dienen te zijn (bv. responstijd)

Waarom zou dat niet kunnen dan?
Een klasse heeft dan gewoon de verantwoordelijkheid om binnen de gegarandeerde tijd zijn zaken af te handelen. Ik zie niet in waarom dat bij OO dan opeens anders is.

_{ps. Eindelijk weer 's een interessant topic!}

[Verwijderd]

Ik weet wel dat de klasse de verantwoordelijk heeft. Hoe bewijs je dan dat die klasse dat worst -case ook haalt?

[Verwijderd]

Verwijderd schreef op 07 augustus 2002 @ 11:31:
Ik weet wel dat de klasse de verantwoordelijk heeft. Hoe bewijs je dan dat die klasse dat worst -case ook haalt?

Tja, ik denk op ongeveer dezelfde manier...

[mbravenboer]

Ik schreef eergisteren dit op de front-page, wat hier wel relevant is (Dit is precies waar Otis het al eerder over had):

Definieer 'declaratief' dan maar eens. Er is namelijk maar 1 heersende opinie of de term declarativiteit en dat is dat het de meeste slecht gedefinieerde notie van de hele informatica is .

Juist daarom ben ik heel voorzichtig met de term declaratief. Prolog noemde ik een logische programmeertaal (knappe vent die dat gaat tegenspreken ) en XSLT omschreef ik bewust als een meer declaratieve taal in mijn post hierboven.

Ik heb even opgezocht hoe declarative gedefinieerd is in mijn Engelse woordenboek:
[...]
Ik vind deze definitie echter uitermate slap en naief als je niet goed beseft waarover het eigenlijk gaat. De definitie die hier (en veel mensen zouden zich kunnen vinden in deze definitie) wordt namelijk nogal eens misbruikt om te beweren dat declaratieve talen (wat dat ook mogen zijn) geen programma verificatie nodig hebben. Een programma in zo'n taal beschrijf immers niet hoe iets moet gebeuren maar wat er moet gebeuren. Hoe kan een programma nu fout zijn als het alleen beschrijft wat er moet gebeuren?

De fout zit hem in het niet maken van een onderscheid tussen de taal waarin een probleem gespecificeerd is en de taal waarin een probleem geimplementeerd wordt.

Als je een probleem specificeert in een functionele taal en daarna implementeert in een imperatieve taal, zal je een stap moeten maken van het functionele model naar het imperatieve model. Bij deze stap kan je fouten maken en daardoor zal het imperatieve programma geverifieerd moeten worden ten op zichte van zijn specificatie.

Als je een probleem specificeert in een functionele taal en daarna implementeert in een functionele taal, is de specificatie gelijk ook de implementatie. Het is dus niet nodig om de implementatie te vergelijken met de specificatie, omdat ze simpelweg hetzelfde zijn.

Als je een probleem specificeert in een imperatieve taal en daarna implementeert in een imperatieve taal, is de specificatie weer gelijk aan de implementatie. Hierdoor hoeft de implementatie dus ook nu niet geverifieerd te worden.

Nu terug naar het misbruik van de definitie van declarativiteit: ik kan zo het quicksort algoritme implementeren in een functionele taal. Waarom zou ik hierin geen fout kunnen maken?

Het punt zit hem in de aanname dat de specificatie van een probleem in dezelfde taal is geschreven als de implementatie: de implementatie is de specificatie en andersom. Op zich prima, als dit ook daadwerkelijk zo zou zijn. In het algemeen is het echter zo dat algorithmen of problemen niet gespecificeerd zijn in een functionele taal. Ze zijn gespecificeerd in een ander model: niet het functionele, niet het imperatieve (het model van de computer).

Er is verificatie nodig zodra een implementatie in een ander model valt de specificatie. Daarom is het onzinnig om te beweren dat een programma geschreven in declaratieve taal nooit geverifieerd zou moeten worden, wat helaas wel vaak gebeurd.

De term declaratief is tegenwoordig in feite een verzamelnaam voor alle talen die niet gebaseerd zijn op het model van de moderne computer: het imperatieve model. Als je declarativiteit zo bekijkt is dat prima, maar helaas worden er vaak meer consequenties verbonden aan het declaratief zijn van een taal.

Minder relevant, maar misschien toch nog leuk:

Beireke :Structureel gezien is iedere porogrammeertaal gelijk

Gelukkig niet. Programmeertalen zijn onder te verdelen in paradigma's. Het paradigma van een programmeertaal is simpel gezegd de filosofie van een taal.

Programmeertalen zijn ontworpen om een programmeer zich prettig te laten uitdrukken. Maar wat is prettig uitdrukken? Misschien dat je verschillende problemen ook wel juist op een andere manier wilt uitdrukken? Vergelijk het eens met eten: yoghurt eet je met een lepel, niet met een vork. Brood eet je bij voorkeur weer wel met een vork.

Omdat programmeer problemen heel divers zijn, zijn er ook veel verschillende paradigma's. Het vrijwel totaal dominerende paradigma in deze tijd is het imperatieve paradigma, wat je terug ziet in een procedurele en een object georienteerde variant. Vrijwel alle veel gebruikte programmeertalen van dit moment zijn imperatief en daarom lijkt het misschien alsof alle programmeertalen dezelfde structuur hebben.

Er zijn echter ook andere talen, met andere paradigma's: XSLT (een transformatie taal voor XML) is bijvoorbeeld niet imperatief. XSLT is 1 van de eerste talen in een ander paradigma die gebruikt wordt door een breed publiek. Het is een wat meer declaratieve taal, met een functioneel luchtje.

SQL is bijvoorbeeld ook niet imperatief, maar is vanwege zijn aard lastig te vergelijken met andere programmeertalen: een XSLT implementatie kan je eventueel in Java uitdrukken, bij een SQL query ligt dat wat anders. Bij SQL beschrijf je in relationele algebra een query op een database. Het beschrijvende is een belangrijk aspect: je geeft niet precies aan hoe een query uitgevoerd moet worden, maar je geeft aan wat de query moet doen.

Daarnaast zijn er nog vele andere programmeertalen in volstrekt andere paradigma's die echter maar lastig hun weg kunnen vinden naar de gewone programmeur. De bekendste voorbeelden zijn wellicht de hogere orde functionele talen, met als voorbeelden Haskell en Clean. Ook is er bijvoorbeeld nog Prolog, een logische programmeertaal, Stratego een krachtige transformatie-taal met een functioneel luchtje en verder zijn er nog karrevrachten programmeertalen met een heel specifiek domein. Deze zogenaamde DSLs (domain specific languages) lijken een steeds grotere rol te gaan spelen omdat ze zich richten op een bepaald probleem: yoghurt eet je bij voorkeur met een lepel, een tool wat speciaal is gemaakt voor vloeibare etensmiddelen.

Verder is het nog zo dat functioneel programmeren nog wel eens gezien wordt als een speeltje van wannebe wiskundigen. Functioneel programmeren is min of meer gebaseerd op het argument dat in de wiskunde vrijwel alle problemen in termen van functies worden gedefinieerd. Het argument is dan vaak dat functies kennelijk een goed formalisme zijn om je uit te drukken. Boze tongen beweren echter dat wiskundigen dit alleen maar als formalisme gebruiken om zich goed en formeel uit te kunnen drukking, maar absoluut niet denken en redeneren in termen van functies.

Functioneel programmeren heeft sowieso het voordeel dat je niet direct kunt goochelen met geheugen, maar dit voordeel hebben vrijwel alle meer declaratieve talen en in mindere mate ook al de moderne object georienteerde talen. Bij deze laatste kunnen echter nog steeds aliassen bestaan, wat de zaak nogal compliceert bij bewijsvoering.

[Orphix]

Maar als ik het goed begrijp gaat het niet zozeer om OO vs non-OO, maar meer om imperatief vs functioneel programmeren?
Oftewel een C programma zou even moeilijk correct te bewijzen zijn als een C++ programma?

[Dash2in1]

Hmm, ik las eigenlijk dat er alleen een vergelijking getrokken wordt tussen aan de ene kant functionele talen en aan de andere kant object georienteerde talen. Over niet-oo (die wel imperatief zouden zijn) talen wordt zoals ik het lees geen uitspraak gedaan.

[MSalters]

Ik heb het ernstige gevoel dat dit allemaal irrelevant is.
Voor systemen waarvan de correctheid bewezen moet worden hoeft vaak alleen de logica bewezen te worden, ik hoef bv. niet te bewijzen dat alle 100M transistoren in m'n CPU het doen en zo.
Kortom, ik schrijf in zo'n geval m'n programma logica niet in C of C++ (OO of niet OO) maar in Z oid. Dat bewijs ik dan, en vervolgens map ik alle Z constructies op corresponderende C++ constructies. Deze mapping zul je met de hand moeten verifieren, maar die is veel makkelijker (want beperkt).

En dat zoiets werkt, dat blijkt uit bv. de stormvloedkering in de nieuwe waterweg - die is met Z en C++ gemaakt. Naar schatting 1 bug in 10000 jaar.

[Alarmnummer]

Tegenwoordig zijn er ook al test programma`s uit, zoals JUnit (voor java) en NUnit (voor .NET) waarmee je je objecten kan testen aan de hand van gevonden uitvoer, en verwachte uitvoer. Dit is superhandig omdat je die testen (in aparte objecten) altijd in je sourcecode houd en je ze eventueel na iedere compile kan uitvoeren om te controleren op correctheid.
Het is dan wel niet hetzelfde als een correctheid bewijs, maar ik hou wel een veel veiliger gevoel over mijn objecten.

[Soultaker]

Orphix schreef op 07 augustus 2002 @ 12:16:
Maar als ik het goed begrijp gaat het niet zozeer om OO vs non-OO, maar meer om imperatief vs functioneel programmeren?
Oftewel een C programma zou even moeilijk correct te bewijzen zijn als een C++ programma?

Dat klopt. Het gaat er natuurlijk een beetje om, hoe de code geschreven is. Je kunt in C al je staat in globale variabelen bewaren; daar de correctheid van bewijzen is een hel. Je kunt in C echter ook redelijk goed functioneel programmeren (al mis je wat handige features) in welk geval het weer wat makkelijker gaat.

En dat zoiets werkt, dat blijkt uit bv. de stormvloedkering in de nieuwe waterweg - die is met Z en C++ gemaakt.

Voor zover ik ervaring heb met Z (heb in 't kader van m'n studie een boek van Jacky (?) erover gelezen) was ik niet erg enthousiast. De specificaties die je in Z schrijft, wijken vaak af van de implementatie. Wanneer de specificatie niet 1-op-1 af te spiegelen is op implementatie, is het niet zo nuttig om formeel te kunnen bewijzen dat de specificatie correct is. Dat zegt dan immers weinig over de correctheid van de implementatie, waar het uiteindelijk om gaat.

Ik zie dus meer toekomst in programmeertalen waarvan de code zelf dusdanige vorm heeft, dat er op een zinnige wijze over valt te redeneren.

Naar schatting 1 bug in 10000 jaar.

Dat lijkt me wel een heel erg globale schatting. Waar baseren ze dit op? Sowieso is 'aantal bugs per jaar' natuurlijk een wat vreemde maat. Bugs zitten wel of niet in de software. Of ze zich ook manifesteren is maar de vraag en als dat gebeurt, zit er een groot verschil tussen de ernstigheid ervan. Dit soort uitspraken lijken mij dus een poging indruk te maken; dat komt weinig professioneel over.

[Verwijderd]

MSalters schreef op 07 augustus 2002 @ 12:36:
Ik heb het ernstige gevoel dat dit allemaal irrelevant is.
Voor systemen waarvan de correctheid bewezen moet worden hoeft vaak alleen de logica bewezen te worden, ik hoef bv. niet te bewijzen dat alle 100M transistoren in m'n CPU het doen en zo.
Kortom, ik schrijf in zo'n geval m'n programma logica niet in C of C++ (OO of niet OO) maar in Z oid. Dat bewijs ik dan, en vervolgens map ik alle Z constructies op corresponderende C++ constructies. Deze mapping zul je met de hand moeten verifieren, maar die is veel makkelijker (want beperkt).

Je algo bewijzen is idd de 1e stap. Echter, dat zegt nog niets over de implementatie. Je zult toch echt moeten aantonen dat de implementatie gelijk is aan het algoritme (en niet minder en niet meer) zodat je met je algobewijs de code bewijst.

En dat zoiets werkt, dat blijkt uit bv. de stormvloedkering in de nieuwe waterweg - die is met Z en C++ gemaakt. Naar schatting 1 bug in 10000 jaar.

[/quote]
De programmeurs van deze software werkten toevallig op dezelfde afdeling als waar ik toen werkte bij CMG en believe me, een aantal van die programmeurs hoopt echt dat het nooit hoog water wordt.