Beweren en bewijzen/de zuilen/Formalisering

We willen betrouwbaar redeneren over vraagstukken omtrent de fysieke realiteit. Absolute zekerheid dat een redenering klopt biedt de wiskunde, maar die gaat niet over de fysieke realiteit, hooguit over een wiskundig model van een aspect ervan. Hoe hangen de eigenschappen van →dingen samen met zulke wiskundige modellen?

Wiskundige objecten (bijvoorbeeld getallen als onderdeel van een model van de realiteit) als ook redeneringen erover moeten we opschrijven om ze te kunnen communiceren en controleren. Zowel de beschrijving van wiskundige objecten als de beschrijving van redeneringen kunnen, maar hoeven niet, in een formele taal gesteld zijn.

Sommige cursussen van de opleiding gaan óf over een stuk wiskunde óf over een stuk realiteit. Hier, in de hoofdstukken

wordt uitgelegd hoe deze verschillende werelden in elkaar zitten, wat ze met elkaar te maken hebben en hoe je ermee omgaat.

Inhoud

1 1. Vier werelden
- 1.1 Men moet kunnen praten
- 1.2 Het moet kloppen
2 2. Precisie
3 3. Domeinmodel
- 3.1 Ons speelveld
  - 3.1.1 Exemplarische onderwerpen
  - 3.1.2 Exemplarische talen
- 3.2 Voorbeelden
4 4. Correctheidsstelling
5 5. Systematisch vertalen
6 6. Tijd
7 7. Vereenvoudigingen
8 8. Parametrisatie
- 8.1 De algemene vorm van de correctheidsstelling voor systemen

1. Vier werelden

literatuur

Pencast^What? over het thema: rationaliteitscubus: Rationaliteitsvierkant en de vier werelden in een click here
Wat is de beste manier om iets te zeggen?

werelden

realiteit - wiskunde
objecten - beschrijvingen

De onderkant van het rationaliteitsvierkant gaat over dingen, d.w.z. objecten in de fysieke realiteit, de bovenkant over hun beschrijvingen. We willen over dingen en hun eigenschappen redeneren, en we willen dat zo doen dat wij en anderen, zelfs computers, onze redenering kunnen controleren, want iedereen maakt wel eens redeneerfouten.

De crux van de rationaliteit is dat dit redeneren en controleren aan de bovenkant van het rationaliteitsvierkant gebeurt: we redeneren niet over de dingen zelf, maar over hun beschrijvingen, en we schrijven een beschrijving van onze redenering op opdat iemand anders deze kan controleren.

Beschrijven kunnen we in natuurlijke taal of in een →formalisme. Formalismen hebben grote voordelen: ze zijn exact en ondubbelzinnig, je kunt ermee rekenen, en een computer kan er van alles mee. Helaas gaan formalismen nooit over dingen uit de fysieke realiteit, ze gaan altijd over wiskundige objecten. Als we bewijsbare conclusies over de fysieke realiteit willen trekken en het bewijs ook nog door een computer laten controleren, hebben we dus te maken met vier werelden. Hoe hangen deze samen?

Men moet kunnen praten

natuurlijke taal informele redeneringen	Syntaxis. De betekenis van een uitspraak in een formele taal kan exact worden afgeleid volgens haar constructieboom. Bij natuurlijke talen is dat niet het geval; zij zitten op een verwarrende manier anders in elkaar dan formele talen.	formele taal geldig gevolg
Semantiek. Natuurlijke taal heeft geen exacte, ondubbelzinnige betekenis. Dezelfde uitspraak over de realiteit kan door twee mensen verschillend geïnterpreteerd worden zonder dat ze dat door hebben.	Als de realiteit zich houdt aan de beweringen b₁, b₂, ... als bovendien B een logisch gevolg is van b₁, b₂, ..., dan houdt de realiteit zich ook aan B.	Semantiek. Elke syntactisch correcte bewering in een formele taal heeft een exacte betekenis, maar niet in de fysieke realiteit, alleen in de wereld van de wiskunde.
fysieke realiteit dingen en gebeurtenissen	Abstractie. Om helder en exact te kunnen redeneren over de realiteit moeten we belangrijke van irrelevante aspecten scheiden. We redeneren niet over de realiteit zelf maar over een abstractie.	wiskundig model beschrijfbare situaties

Wat weet jij over deze vier werelden?
natuurlijke taal Hebben de voegwoorden in natuurlijke taal een eenduidige betekenis? Zijn beweringen in natuurlijke taal altijd eenduidig te ontleden? Zijn de begrippen in natuurlijke taal scherp afgebakend? Is er een scherpe grens tussen natuurlijke en formele taal? Wat ís een formele taal? Wat is "Geformaliseerde natuurlijke taal"?	Syntaxis.	formele taal Wat betekent geldig gevolg? Wat betekenen de symbolen \|- en \|= ? Welke formele talen ken je?
Semantiek.	Als de realiteit zich houdt aan de beweringen b1, b2, ... als bovendien B een geldig gevolg is van b1, b2, ..., dan houdt de realiteit zich ook aan B.	Semantiek.
fysieke realiteit Bestaat er een objectieve realiteit? Is er een scherpe grens tussen verschillende dingen in de realiteit? Laten zich verschillende soorten dingen scherp onderscheiden? Kunnen we het eens worden over dingen en gebeurtenissen?	Abstractie.	wiskundig model Hoe zijn wiskundige objecten gedefinieerd? Wat zijn relaties? Wat is het verschil tussen wiskundige objecten en formules?

Hoe komen we van de linkerkant naar de rechterkant, opdat we met grootst mogelijke zekerheid gebruik kunnen maken van de rede? Zeker niet op deze manier:

Het moet kloppen

Formeel moet alles precies kloppen, hoe ingewikkeld het ook is. Maar het moet vooral ook passen bij de realiteit. Dit kunnen we beter controleren als het formalisme ook nog eens goed leesbaar is.

Wat er kan gebeuren als je niet oplet op de relatie tussen werkelijkheid en formalisme kun je hieronder lezen. Voltaire legt de woorden in de mond van de beroemde wiskundige Leonhard Euler:

Eulers bekentenis
De plus, ... notre lieutenant-général, Léonard Euler, déclare par notre bouche ce qui suit:	Bovendien ... verklaart onze generaalluitenant Leonhard Euler door onze mond het volgende:
...
IV. Qu’afin de radoucir un peu les philosophes allemands, il fera son possible pour ne plus captiver sa raison sous la foi d’une formule erronée. Il demande pardon à genoux à tous les logiciens d’avoir écrit à l’occasion d’un résultat contradictoire de son calcul: Hoc quidem veritati videtur minus consentaneum. Quidquid vero sit hic calculo potius quam nostro judicio est fidendum. (Voyez Euleri Mechanica, tome I^er, page 208.) « Cela ne paraît pas pouvoir être vrai. Mais, quoi qu’il en puisse être, il faut plutôt en croire le calcul que notre propre jugement. »	IV. dat hij, om de duitse filosofen enigzins gerust te stellen, het mogelijke zal doen om zijn verstand niet meer aan een foutieve formule uit te leveren. Hij bidt alle logici op zijn knieën om vergeving dat hij ter gelegenheid van een tegenstrijdige uitkomst van zijn berekening geschreven heeft: „Dit schijnt niet met de waarheid in overeenstemming te zijn. Hoe het zich ook in werkelijkheid verhouden moge, moet toch deze berekening meer vertrouwen geschonken worden dan ons verstand.”
V. ... qu’il n’emploiera plus soixante pages de calcul pour arriver à une conclusion qu’on peut établir par un raisonnement de dix lignes; item, que toutes les fois qu’il retroussera ses bras pour calculer trois jours et trois nuits de suite, il se donnera la patience de raisonner auparavant un quart d’heure sur le choix des principes qu’il conviendra d’employer.	V. ... dat hij niet meer zestig pagina’s vol berekeningen zal verspillen aan een conclusie die men met een redenering van tien regels kan bereiken; evenzo, dat elke keer als hij zijn mouwen opstroopt om drie dagen en nachten ononderbroken te rekenen, hij de tijd zal nemen om van te voren één kwartier na te denken over de keuze welke beginselen hij toepassen wil.

Bron: Traité de paix conclu entre Mr. le président de Maupertuis et Mr. le professeur Kœnig. Berlin, 1753. – beschrijving van de Koninklijke Bibliotheek – tekst bij Google Books. Vertaling: David N. Jansen. Het citaat van Euler vindt zich in § 272 op pagina 108 [sic!] van Mechanica: sive motus scientia analytice exposita / auctore Leonhardo Eulero. Tomus I. Petropoli: Typogr. Acad. Sc., 1736. – nieuwere editie beschikbaar in de faculteitsbibliotheek – tekst bij Google Books. Met dank aan Niklaus Wirth, die de duitse vertaling van het bovenstaande als motto in zijn boek opgenomen heeft: Algorithmen und Datenstrukturen: Pascal-Version / von Niklaus Wirth. – 3., überarb. Aufl. – Stuttgart: Teubner, 1983.

2. Precisie

literatuur

...

Willen we bij het redeneren geen fouten maken, moeten we ons heel precies uitdrukken. "Wat bedoelt U precies met 'precies'?" Dat leggen we uit aan de hand van voorbeelden uit de kranten en uit het werk van studenten van deze cursus. Het zal blijken dat men vooral dingen moet afleren.

Syntactisch correct

Het bewerings krijgen syntags een betekenissen geent of na naar verkeerdt. Mijdver!

Syntactisch eenduidig

De zin

Time flies like an arrow.

kan zo'n zeven verschillende betekenissen hebben [1][2] omdat hij op een aantal verschillende manieren ontleed kan worden. Wie zich precies wil uitdrukken moet vermijden dat zijn uitingen met een andere ontleding een andere betekenis krijgen.

Een voorbeeld voor wie de Duitse taal beheerst (en de geaardheid van zekere burgemeesters kent): →

Die jüngste Rechtschreibreform hat hier viel Schaden angerichtet, weil man nicht mehr unterscheiden kann was gesprochen ganz anders klingt:

Die Bürgermeister von Berlin und Hamburg sind gestern Abend zusammen gekommen.

Twee bijen praten met elkaar. De ene bij vraagt:

Wat was was eer was was was?

Eer was was was was was is.

Aanhalingstekens zijn noodzakelijk indien over taal gepraat wordt:

Wat was "was" eer "was" "was" was? 
Eer "was" "was" was was "was" "is".

Volledig

Laten we nu een deurbel specificeren. Dit is de →focus:

Het fragment van de realiteit is de knop aan de voordeur, de bel binnen op de bovenverdieping en de nodige bedrading.
Het perspectief is het gedrag, namelijk dat het op het juiste moment wel of niet rinkelt. De kunstzinnige vormgeving van de knop en de muziekhistorische waarde van de ringtone vallen buiten dit perspectief. Daarvan abstraheren we.

Is het volgende een goede eerste benadering van de specificatie van het gedrag van de deurbel?

Als buiten een signaal gegeven wordt, rinkelt het binnen.

Veel mensen zullen dit beamen, omdat ze mentaal invullen:

... en als geen signaal gegeven wordt, rinkelt het niet.

Maar een malafide verkoper met een goede advocaat zal de klant misschien een continu rinkelend belletje verkopen waarvan hij in een onduidelijk land een groot aantal had kunnen kopen. Dat rinkelt tenslotte ook als er buiten een signaal gegeven wordt.

Een betere formulering is:

Het rinkelt binnen op precies de momenten waarop buiten een signaal gegeven wordt.

We moeten alert zijn dat we veel dingen vanzelfprekend aannemen die eigenlijk expliciet genoemd moeten worden, wil men misverstanden voorkomen.

Kernachtig

Houd het bij onomwonden, kernachtige beweringen. Het is niet nodig of verstandig, in een specificatie woorden als "moet", "kan", "mag" te gebruiken, want die kunnen weer voor misverstanden zorgen. Een specificatie zegt wat het geval is, hoe korter, hoe beter. Elk woord te veel is gevaarlijk:

Als dit apparaat niet kapot is rinkelt het binnen dan en slechts dan als buiten de knop ingedrukt wordt.

Elk theekopje voldoet aan deze specificatie: het is een kapotte deurbel.

Hier een voorbeeld met bijzonder veel overbodige, verwarrende en misleidende woorden, uit het leven van deze cursus gegrepen:

De aanleiding om het doel van een deurbel te laten gelden is in de behoefte om een signaal te verplaatsen, in dit geval van binnen naar buiten. Het doel van een deurbel is om op verzoek te rinkelen, dit is het hoogst waarneembare doel. Als dit doel iets verder gespecificeerd wordt, dan wordt het: Het inschakelen van een elektrische bel op een zodanige wijze, dat de bel precies op die moment van stroom wordt voorzien, waarop een knop ingedrukt wordt. Hierbij is van belang, dat de kwaliteit zodanig is, dat het ook doet wat het moet doen.

Wie niet goed piano kan spelen gebruikt graag het rechter pedaal, waarmee je elke onzuiverheid in aangenaam halfduister kunt hullen. Zo kent ook natuurlijke taal een aantal middelen om een rookgordijn op te trekken: "als het ware", "eigenlijk", "in principe", "iets van", "in verband met", "o.i.d." e.d. In professionele specificaties zijn deze onacceptabel.

Ook modale woordjes als "moet", "kan", "mag" hebben in kernachtige beweringen niets te zoeken: ze laten iets open, maar zeggen niet wat. In de wet staat: "wie [dat en dat] doet wordt [zo en zo] gestraft." Punt. Niet: "Degene, waarvan vastgesteld is dat hij... zou eigenlijk door de rechter die en die straf opgelegd zou moeten worden."

Semantisch eenduidig

Als het regent of stormt is het terras gesloten.

En als het regent én stormt tegelijk? Uiteraard ook, dat is toch duidelijk.

Ober: Wat wenst U te drinken?
Gast: Wijn of champagne.

Zou zo'n gast het accepteren dat hij een fles wijn én een fles champagner voor zijn neus krijgt en beide op de rekening verschijnen?

Drinkt u koffie of thee?
Neemt u suiker of melk?

Over het algemeen verstaat men de alternatieven in de eerste vraag als exclusief – van de gast wordt verwacht dat hij precies één drank kiest – en de tweede zin als inclusief – de gast mag ook suiker én melk in zijn koffie bestellen. (Terzijde: Formeel zijn dit gesloten vragen, waar de aangesprokene met „Ja” of „Nee” op kan antwoorden. In de praktijk gebeurt dat echter zelden. Natuurlijke taal heeft ook een pragmatisch niveau, waarop het gaat over de effecten die de spreker wenst te bewerkstelligen. In dit voorbeeld: De ober/gastheer wil graag een bestelling opnemen; zijn woorden maken in de eerste plaats zijn bereidheid daartoe duidelijk.)

Het voegwoord of heeft in natuurlijke taal geen eenduidige betekenis. Professionals zijn zich hiervan bewust en schrijven óf "óf ... óf ..." óf "... en/of ...". Of ze vinden een elegante én eenduidige formulering die het woordje "of" helemaal vermijdt.

Consistent

De betekenis van naamwoorden en werkwoorden ligt in natuurlijke taal niet helemaal vast. De betekenis kan schommelen (hoe groot is groot precies?), maar een woord kan ook een aantal totaal verschillende betekenissen hebben (homoniemen). Dit kan makkelijk worden opgelost, bijvoorbeeld door de context aan te geven en duidelijk te maken welke afspraken hier gelden:

In dit jachttijdschrift betekent "das" altijd de beschermde diersoort en niet een stuk dat men om zijn hals knoopt.

Essentieel is wel dat hetzelfde woord ook overal dezelfde betekenis heeft. Op een tekst waarin hetzelfde woord voor verschillende betekenissen gebruikt wordt (→knel) kun je geen deugende redenering bouwen.

Formele talen

Deze valkuilen kan men vermijden door binnen de context van het professionele werk een kunstmatige, formele taal af te spreken. Zo'n taal, ook formalisme genoemd, moet zo in elkaar zitten dat alle syntactisch correcte teksten precies één betekenis hebben, die langs de syntaxboom van de tekst bepaald kan worden.

Binnen de wereld van zo'n formalisme kan men absoluut eenduidige, betrouwbare redeneringen opzetten en controleren, al dan niet met behulp van een computerprogramma:

Zonder valkuilen van de natuurlijke taal
Men moet wel absoluut zeker weten hoe het formalisme werkt en het perfect toepassen
Zonder het vangnet van de natuurlijke taal

Formele talen hebben het nadeel dat men een tekst pas begrijpen kan als men syntax en semantiek van de taal precies kent. Het is alles of niets. Voor je het weet heb je bij één symbool een totaal verkeerd idee en begrijp je de hele tekst verkeerd.

Geformaliseerde natuurlijke taal

Omdat elk formalisme weer geleerd moet worden, hebben veel mensen een hekel aan formele talen die zo ver gaan dat je niet eens met haakjes mag aankomen: ze klappen meteen dicht. Daarom probeert men soms de natuurlijke taal zo zorgvuldig toe te passen als ware het een formele taal. Men wil het exact en leesbaar tegelijk houden. Dat lukt aardig, als men afleert wat men op school geleerd heeft:

We leren op school dat men herhalingen moet vermijden en niet steeds weer dezelfde woorden moet gebruiken. "De jongen liep op straat. De vrachtwagenbestuurder zag het kind niet. Het kereltje was bijna dood." Om hoeveel mensen gaat het hier?

Om de exactheid van formele talen te benaderen moet men zich aan een aantal regels houden. Het resultaat noemen we geformaliseerde natuurlijke taal.

Kwaliteitscriteria geformaliseerde natuurlijke taal

Gebruik voor dezelfde dingen steeds precies dezelfde woorden. Gebruik verschillende woorden als signaal dat er een verschil in betekenis is.
Gebruik bij het maken van zinnen geen voegwoorden waarvan de betekenis vaag is. In de formele logica hebben alle voegtekens een precieze betekenis: ∧, ∨, → etc. In de natuurlijke taal gaat het met "of" al mis. Hoe beter je formele talen beheerst hoe preciezer je natuurlijke taal kunt toepassen, omdat de formele talen je de problemen duidelijk hebben gemaakt.
Maak absoluut duidelijk waar je een eigen begrip definieert en houd je dan precies aan deze definitie en gebruik de term daarna in de tekst nooit meer in de "gewone" betekenis.
Zeg geen woord te veel.
Vermijd modale woordjes als "kan", "moet", "mag".
Gebruik aanhalingstekens als je in de taal over de taal schrijft. "In het Nederlands" heeft zeker 15 letters. In het Nederlands heeft "zeker" 5 letters.
Gebruik verschillende lettertypes waar dat helpt verschillende taalniveaus te onderscheiden.

Leesbaar

In het afschrikkende voorbeeld hieronder ontbreekt 1 haakje. Waar?

Definition Kachel := ((forall t1 : T, (forall t2 : T, (t2 in (t1-5, t1] -> KIK t2 /\ LIK t2 /\ VER t2)
-> TEMP (t1) warmtewisselaar kookpunt /\ (forall t3 : T, t3 in (t1-5, t1] /\ RUS t3)) /\ (forall t1 : T, (forall t2 : T, (t2 in (t1-5, t1] ->
~KIK t2 \/ ~LIK t2 \/ ~VER t2)) -> ~TEMP (t1) warmtewisselaar kookpunt /\ (forall t3 : T, t3 in (t1-5, t1] /\ ~RUS t3))).

Wie ingewikkelde specificaties in een formalisme opschrijft, moet zijn formules zo opmaken dat de lezer als het ware de constructieboom voor zich ziet. Dit kan op allerlei manieren en is deels een kwestie van smaak. Hier een voorbeeld:

Definition Kachel := 
(   (forall t1: T,   (forall t2: T, (t2 in (t1-5, t1] ->  KIK t2 /\ LIK t2 /\ VER t2))
                   ->
                     TEMP (t1) warmtewisselaar kookpunt /\ (forall t3: T, t3 in (t1-5, t1] /\ RUS t3)
    )
  /\
    (forall t1: T,   (forall t2: T, (t2 in (t1-5, t1] -> ~KIK t2 \/ ~LIK t2 \/ ~VER t2))
                   ->
                     ~TEMP (t1) warmtewisselaar kookpunt /\ (forall t3: T, t3 in (t1-5, t1] /\ ~RUS t3)
    )
).

Je ziet meteen wat de bereiken van de quantoren zijn. Bij elk openend haakje kun je het erbij horende sluitende haakje makkelijk vinden.

Te veel witruimte is echter ook niet goed. Bij goede indentatie en de juiste plaatsing van haakjes is het niet nodig om ook nog witregels in formules te hebben of de regel achter een openend haakje wit te laten. Leesbaarheid hangt er namelijk ook van af dat je alles wat bij elkaar hoort in samenhang kunt zien, dus niet over te veel pagina's verspreid:

Dat is nergens goed voor en maakt formules onnodig groot.

Kwaliteitscriteria opmaak van formules

Formules mogen nooit zo breed gezet worden dat ze van de pagina aflopen.
Een sluitend haakje staat
- óf op dezelfde regel als het bijbehorende openend haakje
- óf precies eronder.
Hetzelfde geldt voor voegtekens en operatoren op hetzelfde niveau.
Wees zuinig met onnodige haakjes en witruimte.

Wie zich niet houdt aan zulke discipline doet zichzelf geen plezier: ook de eigen formules zijn na een tijd niet meer te doorgronden. Tegen andere lezers, waaronder medestudenten en docenten, is een onoverzichtelijk opgemaakte formule een uiting van onbeleefdheid. Je moet het zo schrijven dat het voor de ander aantrekkelijk is je werk te doorgronden en geen kwelling.

Het probleem van het doorgronden van constructiebomen doet zich ook in natuurlijke taal voor:

Zo schrijft de Nederlandse rechter J. Willems, voorzitter van de Raad van Tucht, over Peper vs. KPMG:

Omdat het te verrichten onderzoek zich aldus mede zou gaan uitstrekken tot de gedragingen van individuele personen, die bovendien zoals ten aanzien van klager het geval was nog immer, hetzij binnen de gemeente Rotterdam hetzij daarbuiten, publieke functies bekleedden en omdat naar betrokkenen wellicht hebben onderkend en in ieder geval behoren te hebben onderkend eventuele, deze personen belastende, bevindingen diverse gevolgen zouden kunnen hebben, niet alleen van bijvoorbeeld civielrechtelijke of bestuursrechtelijke aard, rustte op betrokkenen meer nog dan in het algemeen reeds met betrekking tot het geraken en presenteren van bevindingen door accountants het geval is in het bijzonder de verplichting naar de mate van het redelijkerwijs mogelijke te voorkomen dat met name eventuele indidividuele personen belastende bevindingen een onevenredige nadruk zouden kunnen gaan krijgen, bijvoorbeeld doordien aan die bevindingen vanwege de wijze van presenteren ervan of het onvoldoende plaatsen daarvan in de context van bevindingen met betrekking tot de regelgeving of bestuurlijke of andere opvattingen waarbinnen of op de grondslag waarvan de onderzochte activiteiten werden verricht een andere betekenis zou worden toegekend dan zij genuanceerd en in haar context begrepen naar objectieve maatstaven dienen te hebben.

Bovenstaande bewering is juridische taal. Juristen zijn gewend zich zorgvuldig en ondubbelzinnig uit te drukken, maar wat opmaak betreft, kunnen ze misschien van wiskundigen en informatici nog wat leren. De lezer moet namelijk de volgende opmaak mentaal reconstrueren alvorens ook maar iets te begrijpen; dan is het glashelder:

Omdat
- het te verrichten onderzoek zich aldus mede zou gaan uitstrekken tot
  - de gedragingen van
    - individuele personen, die
      - bovendien
        zoals ten aanzien van klager het geval was
      - nog immer,
        hetzij binnen de gemeente Rotterdam
        
        hetzij daarbuiten,
      - publieke functies bekleedden
en omdat
- - naar betrokkenen wellicht hebben onderkend
  - en in ieder geval behoren te hebben onderkend
- eventuele, deze personen belastende, bevindingen diverse gevolgen zouden kunnen hebben,
  - niet alleen van bijvoorbeeld
    - civielrechtelijke
    - of bestuursrechtelijke aard,
rustte op betrokkenen
- meer nog dan in het algemeen
  - reeds met betrekking tot
    - het geraken en presenteren van bevindingen door accountants
- het geval is
- in het bijzonder
de verplichting
naar de mate van het redelijkerwijs mogelijke
te voorkomen
dat
- met name eventuele indidividuele personen belastende
bevindingen
een onevenredige nadruk zouden kunnen gaan krijgen,
- bijvoorbeeld
  - doordien aan die bevindingen
    - vanwege de wijze van presenteren ervan
    - of het onvoldoende plaatsen daarvan
      - in de context van bevindingen met betrekking tot de regelgeving of bestuurlijke of andere opvattingen waarbinnen of op de grondslag waarvan de onderzochte activiteiten werden verricht
  - een andere betekenis zou worden toegekend
    - dan zij
      - genuanceerd
      - en in haar context begrepen
    - naar objectieve maatstaven
    - dienen te hebben.

Hoe dan ook, pas als we precieze, ondubbelzinnige beweringen kunnen opschrijven, kunnen we proberen ons gelijk te bewijzen.

3. Domeinmodel

literatuur

Boek Logica voor alfa's en informatici

Redeneren betekent scheiden, passen en sluiten van gedachtenfragmentjes, en om te beginnen moeten we fragmentjes hebben die zo klein en goed gedefinieerd zijn dat we betrouwbaar na kunnen gaan of ze eigenlijk wel waar zijn t.a.v. de realiteit, of niet. Om zeker te zijn dat onze redenering klopt willen we daartoe een formalisme gebruiken en misschien de redenering ook nog door een computer laten controleren. Daartoe moeten we een formele taal maken.

Omdat dit nogal veel werk is, doen we er goed aan van begin af alles rigoreus weg te laten, wat er niet toe doet. Daarom is het ook belangrijk dat we een focus kiezen en daarmee een gezichtspunt. We hoeven dan niet te praten over fenomenen die onder dat gezichtspunt irrelevant zijn.

Als we bijvoorbeeld na willen gaan of de stroomdraden in een gebouw juist aangesloten zijn, moeten we ook over de kleur van de isolering praten. Er zijn namelijk voorschriften voor het gebruik van zwarte, blauwe, bruine en geel-groene kabels. Als we alleen willen beredeneren dat geen brand of kortsluiting kan ontstaan, doet de kleur van de kabels er niet toe, maar wel hun dikte en daarmee hun weerstand.

Hoe meer je vanaf het begin weloverwogen buiten beschouwing laat hoe makkelijker het later wordt; minder is meer. Maar in welke formele termen praten we het beste over wat we niet buiten beschouwing kunnen laten?

Ons speelveld

Exemplarische onderwerpen

Hoe men door formalisering precisie bereikt en tegen welke prijs leggen we hier exemplarisch uit aan de hand van correctheidsvraagstukken uit de ontwikkeling en verificatie van artefacten. Wat we hier zeggen geldt echter ook voor andere gebieden, al is de koppeling van het formalisme aan de realiteit niet overal zo makkelijk. We zullen namelijk hier alleen redeneren in termen van waarneembare fenomenen.

In Beweren en bewijzen/de zuilen/Artefacten/3. Specificaties gaven we de specificatie van een artefact en haar onderdelen in natuurlijke taal. Formaliseren wil zeggen op een precieze wiskundige manier de specificatie van in dit geval een artefact of onderdeel vastleggen. Door een formele taal te gebruiken wordt een aantal criteria wel gemakkelijker te toetsen. Bijvoorbeeld bij criterium S3: "Een specificatie praat alleen over fenomenen die het te specificeren ding deelt met zijn omgeving". Dit is eenvoudig te toetsen door te kijken of de namen die in de specificatie van een ding voorkomen, overeenkomen met van te voren gedeclareerde namen van fenomenen.

We sluiten dus aan bij de criteria voor specificaties uit Beweren en bewijzen/de zuilen/Artefacten/3. Specificaties en de criteria voor precisie uit Beweren_en_bewijzen/de_zuilen/Formalisering/2._Precisie.

Elke formele specificatie, in welke taal dan ook, praat over wiskundige objecten in de hoop dat deze overeenkomen met de realiteit. Bij ons zijn dat waarneembare fenomenen: verschijnselen waarvan we met een meting kunnen vaststellen of ze in de realiteit waar zijn en in de formele taal namen hebben die met wiskundige objecten corresponderen.

De correspondentie tussen reële fenomenen en namen voor wiskundige objecten geven we hier altijd aan in een tabel: het zogenaamde domeinmodel, ook wel "woordenboek" genoemd.

Gereedschappen zoals Coq kunnen worden gebruikt om een aantal zaken te controleren. Deze controle speelt zich uiteraard alleen af binnen het wiskundige domein.

Exemplarische talen

In deze cursus gebruiken we formele logica zoals uitgelegd in Beweren en bewijzen/de zuilen/Taal/2. Logica. Er zijn talloze andere specificatietalen op de markt, waarvan sommige voor de beroepspraktijk beter geschikt zijn. Maar in geen andere taal dan de logica leer je het beste wat de essentie van formeel specificeren en bewijzen is. Als je deze cursus voltooid hebt kun je andere talen zelf leren en aan elkaar relateren.

In de propositielogica zijn beweringen samengesteld uit eindig veel proposities. Om het verband tussen formele beweringen en de fysieke realiteit te leggen moet je bij elke propositie aangeven wat in de realiteit moet gelden wil de propositie waar zijn.

In de predikaatlogica kun je veel meer uitdrukken dan in de propositielogica. In plaats van eindig veel proposities heb je eindig veel predikaten, waarvan elk een aantal parameters kan hebben, waardoor men over oneindig veel situaties kan praten. Vaak zal één van deze parameters de tijd zijn, waarop het predikaat waar is. De precieze taal en notatie komt in het hoofdstuk Beweren en bewijzen/de zuilen/Taal uitgebreid aan te orde.

Voorbeelden

We zullen nu formele specificaties en domeinmodellen illustreren aan de hand van een aantal voorbeelden. De formules en domeinmodellen in predicaatlogica staan hier voor een eerste indruk waar we naar toe gaan, maar we zullen in het begin vooral oefenen met de - eenvoudigere maar zwakkere - propositielogica.

Oven

Onze focus is het functioneren van een oven. Veiligheid e.d. vallen buiten de focus en over de precieze spanningen, stromen, temperaturen en vermogens willen we het ook niet hebben. Het gaat alleen om het samenspel van stekker, knop en bakplaat:

Als er spanning op de steker staat en de Aan-knop is ingedrukt, dan is de bakplaat warm.

In propositielogica wordt dit:

Spanning ∧ Aan → Warm

In het domeinmodel geven we aan wat de gebruikte proposities met de realiteit te maken hebben:

domeinmodel
propositie	type	betekenis	meting	formele notatie t.b.v. Coq
Spanning	B	er staat spanning op de stekker	voltmeter	`Variable Spanning: B.`
Aan	B	de Aan-knop is ingedrukt	bekijken	`Variable Aan: B.`
Warm	B	de bakplaat is warm	thermometer	`Variable Warm: B.`

Als we nu een uitgebreidere specificatie maken waarin de oven een opwarmtijd van 8 minuten heeft, dan kunnen we niet langer abstraheren van de tijd en hebben we predikaatlogica nodig. We kunnen dan ook in één moeite door de nodige spanning en de gewenste temperatuur specificeren: "Als de oven 8 minuten lang ingeschakeld is en op 230V is aangesloten, is hij aan het eind van die periode opgewarmd op 180 C." Hier een eerste poging:

(∀t: (0,8], Spanning t 230 ∧ Aan t) → Warm 8 180

(Gemakshalve gebruiken we hier een half-open tijdsinterval als type. Hoe je daarmee in de taal van de logica en bij gebruik van een bewijsassistent precies moet omgaan, staat uitgelegd in de hoofdstukken Typering, Tijd en Tijdslogica.)

We kunnen bij een echte oven op ieder moment beginnen, niet alleen op het moment 0. De specificatie wordt dus:

∀m: T, (∀t: (0,8], Spanning(m+t) 230 ∧ Aan(m+t)) → Warm (m+8) 180

In het domeinmodel moeten we nu predicaten met tijds-, temperatuur- en spanningsparameters gebruiken:

domeinmodel
type		betekenis (verzameling)		formele notatie t.b.v. Coq
T		de tijd in minuten in reële getallen		`Definition T := R.`
U		de spanning in Volt in reële getallen		`Definition U := R.`
Tmp		de temperatuur in graden C in reële getallen		`Definition Tmp := R.`
(t₁, t₂]		{t: T \| t₁< t ∧ t ≤ t₂}		Zie nadere toelichting.
predikaat	type	betekenis	meting	formele notatie
Spanning	T→U→B	Spanning t v: op moment t staat er v Volt op de steker	voltmeter	`Variable Spanning: T->U->B.`
Aan	T→B	Aan t: op moment t is de Aan-knop ingedrukt	bekijken	`Variable Aan: T->B.`
Warm	T→Tmp→B	Warm t x: op moment t is de bakplaat op temperatuur x C	thermometer	`Variable Warm: T->Tmp->B.`

Dit domeinmodel is ingewikkelder, maar we kunnen er ook veel meer me uitdrukken, bijvoorbeeld de afhankelijkheid van de temperatuur van de verwarmingsduur.

CD-speler

We willen een bepaald muziekstuk s horen:

∀t: (0, duratie s], hoor t (klank (s t))

Hierbij is s een functie van type T→C; dus voor een tijdstip is een klank digitaal beschreven.

Het stuk kiezen we door een cd aan te bieden waarop het staat. Die cd moet de hele tijd beschikbaar zijn, want we denken aan een speler zonder geheugen. Let op de nuance: de hele tijd bieden we een cd aan waarop het hele stuk s staat, maar op elk moment horen we precies dat moment van het stuk.

 (∀t: (0, duratie s], cd t s) → (∀t: (0, duratie s], hoor t (klank (s t)))

Het verhaal moet gelden voor elk willekeurig muziekstuk:

 ∀s: T→C, 
   (∀t: (0, duratie s], cd t s) → (∀t: (0, duratie s], hoor t (klank (s t)))

Bovendien moeten we de mogelijkheid hebben om op elk gewenst moment een stuk te horen:

 ∀m: T, 
   ∀s: T→C,
     (∀t: (0, duratie s], cd (m+t) s) → (∀t: (0, duratie s], hoor (m+t) (klank (s t)))

domeinmodel
type		betekenis (verzameling)		formele notatie t.b.v. Coq
T		de tijd in seconden in reële getallen		`Definition T := R.`
K		de hoorbare klanken		`Variable K: Set.`
C		digitale beschrijving van klanken		`Variable C: Set.`
(t₁, t₂]		{t: T \| t₁< t ∧ t ≤ t₂}		Zie nadere toelichting.
functie	type	betekenis		formele notatie t.b.v. Coq
duratie	(T→C)→T	duratie s: de duratie van een digitaal beschreven stuk s		`Variable duratie: (T->C)->T.`
klank	C→K	klank c: de hoorbare klank bij de beschrijving c van een klank		`Variable klank: C->K.`
predikaat	type	betekenis	meting	formele notatie t.b.v. Coq
cd	T→(T→C)→B	cd t s: op moment t draait in de cd-speler een schijfje waarop stuk s staat	schijfje bekijken	`Variable cd: T->(T->C)->B.`
hoor	T→K→B	hoor t k: op moment t hoort men klank k	luisteren	`Variable hoor: T->K->B.`

Politielasergun

Voor een bepaalde auto a, willen we gedurende een tijd van 3000 ms de snelheid die a vlak daarvoor had op een display tonen:

∀s: S, snelheid 0 a s → (∀t: (0, 3000], toon t s)

We moeten in staat zijn dit op ieder gewenst moment te doen:

∀m: T, ∀s: S, snelheid m a s → (∀t: (0, 3000], toon (m+t) s)

We verzwakken de specificatie door te eisen dat voorafgaand aan m, 500 ms op de auto wordt gericht met de loop van de lasergun. Let op de nuance: de hele tijd in (-500, 0] wordt op de auto gericht.

 ∀m: T, (∀t: (-500, 0], richtOp a (m+t))
        →
        (∀s: S, snelheid m a s → (∀t: (0, 3000], toon (m+t) s))

De lasergun moet voor alle auto's werken:

 ∀a:A, 
   ∀m: T, (∀t: (-500, 0], richtOp a (m+t)) 
          →
          (∀s: S, snelheid m a s → (∀t: (0, 3000], toon (m+t) s))

domeinmodel
type		betekenis (verzameling)		formele notatie zonder tabel
T		de tijd in milliseconden in reële getallen		`Definition T := R.`
A		auto's		`Variable A: Set.`
S		snelheid in km/u		`Variable S: Set.`
(t₁, t₂]		{t: T \| t₁< t ∧ t ≤ t₂}		Zie nadere toelichting.
predikaat	type	betekenis	meting	formele notatie zonder tabel
snelheid	T→A→S→B	snelheid t a s: op moment t heeft auto a snelheid s	met andere apparatuur nameten	`Variable snelheid T->A->S->B.`
toon	T→S→B	toon t s: op moment t wordt snelheid s op het display getoond	display bekijken	`Variable toon: T->S->B.`
richtOp	A→T→B	richtOp a t: op moment t wordt de loop op auto a gericht	hoeken opmeten	`Variable richtOp: A->T->B.`

Kwaliteitscriteria domeinmodel

D1. Belangrijk is dat voor elk predikaat in het domeinmodel een meting aangegeven is, waarmee je in de realiteit kunt nagaan of een predikaat waar is. In Beweren en Bewijzen houden we ons alleen bezig met beweringen, opgebouwd uit predikaten die met zo'n meting corresponderen.
D2. Een goed domeinmodel is minimaal, d.w.z. het bevat geen elementen die zich door definities laten samenstellen uit andere elementen van dit domeinmodel. (Als een domeinmodel bv. de predikaten 'is kind van' en 'is vrouwelijk' bevat, zijn de predikaten 'is zoon van' en 'is mannelijk' niet nodig, omdat ze zich laten definiëren.)
D3. Zorgvuldig en systematisch gekozen namen in het domeinmodel en bij eigen definities kunnen helpen verwarring te voorkomen.

4. Correctheidsstelling

literatuur

Pencast^What? college: Functioneel netwerk en correctheidsstelling click here

Stel we hebben

een specificatie S die zegt wat een artefact moet doen,
decompositie van het artefact in een n-tal onderdelen,
voor elk onderdeel i een specificatie s_i,
waarbij in alle s_i dezelfde fenomenen ook hetzelfde genoemd worden (waardoor dus de samenhang van de onderdelen vastgelegd is),
een sluitende argumentatie (een bewijs dus) dat S een geldig gevolg is van alle s_i samen,

dan weten we dat het artefact doet wat het moet doen.

Dat S een geldig gevolg is van alle s_i samen, wordt in de logica genoteerd als:

s₁, s₂, s₃, ... , s_n |= S

Dit noemen we een correctheidsstelling van artefact A als S een specificatie van artefact A is, de s_i specificaties van onderdelen van A en S daadwerkelijk een geldig gevolg is van de s_i samen.

Als we een artefact willen ontwerpen dat aan een gegeven specificatie S moet voldoen, moeten we dus s_i bedenken die een bewijsbare correctheidsstelling opleveren.

Een correct systeem ontwikkelen betekent: een wiskundige stelling bedenken. (Zie Beweren en bewijzen/de zuilen/Artefacten/5. Decompositie en [3].)

Als de specificaties s₁ en S in de taal van de logica opgeschreven zijn, kun je de correctheidsstelling ook in één enkele, logisch gelijkwaardige formule opschrijven, zie Stelling en bewijs:

s₁∧s₂∧s₃∧ ... ∧s_n →  S

Ambitieniveaus

Informeel

In Beweren en bewijzen/de zuilen/Artefacten/4. Structuur zagen we een correctheidsstelling voor een deurbel, geschreven in natuurlijke taal. Omdat de specificaties lang zijn, schrijven we ze onder elkaar en gebruiken een horizontale streep in plaats van de ⊨.

Batterij: Er staat een spanning op contact A.
Knop: Als er een spanning op contact A staat geldt: op contact B staat een spanning dan en slechts dan als de knop ingedrukt is.
Bel: Rinkelt dan en slechts dan als er een spanning op contact C staat.
Kabel: Dan en slechts dan als er een spanning op contact B staat, staat er een spanning op contact C.
--------------------------------------------------------------------------------------------------------------------------------
Dan en slechts dan als de knop ingedrukt is rinkelt het.

Bij correctheidsstellingen kunnen we aan aantal ambitieniveaus onderscheiden. Wij illustreren deze aan de hand van een moderne, simpelere deurbel uit twee onderdelen die één intern fenomeen met elkaar delen. We abstraheren van de energievoorziening en praten niet over wat er gebeuren moet als de knop niet ingedrukt is, dit om het voorbeeld minimaal te houden.

Knop: Als de knop ingedrukt is, is er een radiosignaal.
Bel: Rinkelt als er een radiosignaal is.
--------------------------------------------------------------------------------------------------------------------------------
Als de knop ingedrukt is rinkelt het.

Kwalitatief

(P→Q),  (Q→R) |= (P→R)

Of in in één formule:

(P→Q) ∧ (Q→R) → (P→R)

Dit is een kwalitatieve correctheidsstelling, met abstractie van kwantiteiten. In ons voorbeeld betekent dit abstractie van de tijd en de sterkte van het radiosignaal en van het geluid. Zulke stellingen kunnen nuttig zijn om aan te tonen dat een systeem op de juiste manier in elkaar geplugd is. Hier is propositielogica voldoende.

Kwantitatief

Stel nu, dat de twee onderdelen van onze deurbel computerchips ontvangen die drie tikken van de klok nodig hebben om hun werk te doen en dat de installatie in een omgeving gebruikt wordt, waar tijd een rol speelt. Dan wil men over deze duraties kunnen redeneren.

Predicaatlogica is de adequate taal:

(∀t:T, P t → Q (t+3)) ∧ (∀t:T, Q t → R (t+3)) → (∀t:T, P t → R (t+6))

(Theoretisch kost ook de transmissie van het radiosignaal tijd, maar gezien de lichtsnelheid mogen we dit verwaarlozen.)

Namen i.p.v. waarden

De vorige stelling bevat tweemaal de constante 3. Is het wezenlijk of is het toeval dat de twee duraties gelijk zijn? Net als bij gestructureerd programmeren kun je beter met namen dan met getallen werken:

Definition d1 := 3.
Definition d2 := 3.
(∀t:T, P t → Q (t+d1)) ∧ (∀t:T, Q t → R (t+d2)) → (∀t:T, P t → R (t+d1+d2))

(Het moge vanzelf spreken dat je bij een echte correctheidsstelling betekenisvolle namen i.p.v. P, Q, R, d1 en d2 kiest en in het domeinmodel aangeeft wat deze constanten in het echt betekenen.)

Generieke correctheidsstelling

Nu is het maar een kleine stap om een generieke stelling te bewijzen:

∀d1:T, ∀d2:T, ∀d3:T,
d3=d1+d2 
→
(∀t:T, P t → Q (t+d1)) ∧ (∀t:T, Q t → R (t+d2)) → (∀t:T, P t → R (t+d3))

Als dit eenmaal bewezen is, kun je er alle artefacten van een hele klasse mee verifiëren. Je hoeft alleen nog maar te controleren of de duraties samen aan de formule

d3=d1+d2

voldoen.

Meer hierover in Beweren en bewijzen/de zuilen/Formalisering/8. Parametrisatie.

Bewijsassistenten

Als we onze correctheidsstellingen opschrijven in een notatie die een bewijsassistent begrijpt, kunnen we ons door de computer laten helpen met het vinden en secuur controleren van het bewijs. Hier een volledig, door de computer goedgekeurd bewijs van de generieke correctheidsstelling:

   ┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
1  │      a: 	T 	 	 	 	 	 	 	 	 	 	 	 	 	 	assumption
   │┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
2  ││     b: 	T 	 	 	 	 	 	 	 	 	 	 	 	 	 	assumption
   ││┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
3  │││    c: 	T 	 	 	 	 	 	 	 	 	 	 	 	 	 	assumption 
   │││┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
4  ││││   h1: 	c = a+b 	 	 	 	 	 	 	 	 	 	 	 	 	assumption
   ││││┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
5  │││││  h2: 	(∀t:T, P t → Q (t+a)) ∧ (∀t:T, Q t → R (t+b)) 	 	 	 	 	 	 	 	 	assumption
   │││││┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
6  ││││││ y: 	T 	 	 	 	 	 	 	 	 	 	 	 	 	 	assumption
   ││││││┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
7  │││││││h3: 	P y 	 	 	 	 	 	 	 	 	 	 	 	 	 	assumption
8  │││││││ 	(∀t:T, P t → Q (t+a)) ∧ (∀t:T, Q t → R (t+b)) 	 	 	 	 	 	 	 	 	assumption
9  │││││││ 	∀t:T, Q t → R (t+b) 	 	 	 	 	 	 	 	 	 	 	 	∧e₂ 8
10 │││││││ 	Q (y+a) → R (y+a+b) 	 	 	 	 	 	 	 	 	 	 	 	∀e 9
11 │││││││ 	y+a+b = y+(a+b) 	 	 	 	 	 	 	 	 	 	 	 	lin_solve
12 │││││││ 	y+a+b = y+c 	 	 	 	 	 	 	 	 	 	 	 	 	[replace,c,with,(a,+,b)] 11
13 │││││││ 	Q (y+a) → R (y+c) 	 	 	 	 	 	 	 	 	 	  		[replace,(y,+,c),with,(y,+,a,+,b)] 10,12
14 │││││││ 	(∀t:T, P t → Q (t+a)) ∧ (∀t:T, Q t → R (t+b)) 	 	 	 	 	 	 	 	 	assumption
15 │││││││ 	∀t:T, P t → Q (t+a) 	 	 	 	 	 	 	 	 	 	 	 	∧e₁ 14
16 │││││││ 	P y → Q (y+a) 	 	 	 	 	 	 	 	 	 	 	 	 	∀e 15
17 │││││││ 	P y 	 	 	 	 	 	 	 	 	 	 	 	  		assumption
18 │││││││ 	Q (y+a) 	 	 	 	 	 	 	 	 	 	 	 	 	→e 16,17
19 │││││││ 	R (y+c) 	 	 	 	 	 	 	 	 	 	 	 	 	→e 13,18
   ││││││└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
20 ││││││ 	P y → R (y+c) 	 	 	 	 	 	 	 	 	 	 	 	 	→i 7-19
   │││││└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
21 │││││ 	∀t:T, P t → R (t+c) 	 	 	 	 	 	 	 	 	 	 	 	∀i 6-20
   ││││└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
22 ││││ 	(∀t:T, P t → Q (t+a)) ∧ (∀t:T, Q t → R (t+b)) → ∀t:T, P t → R (t+c) 	 	 	  	 		→i 5-21
   │││└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
23 │││ 	 	c = a+b → (∀t:T, P t → Q (t+a)) ∧ (∀t:T, Q t → R (t+b)) → ∀t:T, P t → R (t+c) 	 	  	 		→i 4-22
   ││└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
24 ││ 	 	∀d3:T, d3 = a+b → (∀t:T, P t → Q (t+a)) ∧ (∀t:T, Q t → R (t+b)) → ∀t:T, P t → R (t+d3) 	  		 	∀i 3-23
   │└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
25 │ 	 	∀d2:T, ∀d3:T, d3 = a+d2 → (∀t:T, P t → Q (t+a)) ∧ (∀t:T, Q t → R (t+d2)) → ∀t:T, P t → R (t+d3) 	 	∀i 2-24
   └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
26  	 	∀d1:T, ∀d2:T, ∀d3:T, d3 = d1+d2 → (∀t:T, P t → Q (t+d1)) ∧ (∀t:T, Q t → R (t+d2)) → ∀t:T, P t → R (t+d3) 	∀i 1-25

Rollen

rollen

opdrachtgever

De opdrachtgever vraagt om een artefact dat één van zijn problemen oplost. Hij geeft (evtl. met hulp van anderen) een specificatie van het gehele artefact en vraagt de architect om een passend artefact te laten maken.

ontwerper

De ontwerper zoekt passende onderdelen en combineert die zó dat zij samen voldoen aan de specificatie van het geheel.

leverancier

Elke leverancier die een relevant onderdeel produceert, levert ook een specificatie die aangeeft wat zijn onderdeel doet.

Scheiding van belangen

Opdrachtgever

s₁/\s₂/\..../\s_n→S

Ontwerper

s₁∧s₂∧ ... ∧s_n→S

Leverancier

s₁/\s₂/\..../\s_n→S

Wat als iets mis gaat?

Als het systeem in het echt niet doet wat het moet doen, betekent dit logisch dat het zijn S niet waar maakt. Dan zijn er slechts deze mogelijkheden:
- Het bewijs - en daarmee het ontwerp - deugt niet.
- Ten minste één onderdeel maakt zijn specificatie niet waar.
De correctheidsstelling geeft ons dan houvast bij het maken van een beter ontwerp.

5. Systematisch vertalen

literatuur

...

Wie slaapt, snurkt

We verkennen de samenhang tussen een stukje natuurlijke taal - in dit geval het woord je "wie" - en onze formele taal, predikaatlogica, aan de hand van een zeer eenvoudig voorbeeld.

Verkenning

Wie slaapt, snurkt.
Hoe pakken we zoiets aan? Stel we hebben predicaten `slaapt` en `snurkt` in ons domeinmodel, dan zal het toch iets moeten zijn van:
	slaapt ...		snurkt ...
Om wie gaat het? In elk geval in beide gevallen om dezelfde persoon, laten we ze `x` noemen:
	slaapt x		snurkt x
Hoe moeten we de twee delen verbinden? Er zijn niet zo veel mogelijkheden: `∧ ∨ →` x slaapt en snurkt? x slaapt of snurkt? Nee: Als x slaapt, dan snurkt x.
	slaapt x	→	snurkt x
Maar x is nog niet gedefinieerd? Er zijn niet zo veel mogelijkheden om een naam te definieren. Is het een parameter? Nee. Ook geen constante. Het gaat om een universele uitspraak:
∀ x:M,	slaapt x	→	snurkt x

Dit kunnen we beter systematisch aanpakken:

Systematisch

We kijken aan de hand van hetzelfde zeer eenvoudige voorbeeld hoe we zoiets systematisch kunnen vertalen.

Wie slaapt, snurkt.

Wordt hier gepraat over één bepaald persoon? Of over een zeker (maar niet bekend) persoon?

Nee, er wordt over iedereen gepraat. Het is een universele bewering.

(kwantor)formule

∀ x:M,

Als x slaapt, snurkt x.

implicatie

x slaapt.
term
slaapt x

→

x snurkt.
term
snurkt x

Dus de uiteindelijke formule wordt:

∀ x:M, ( ( slaapt x ) → ( snurkt x ) )

Door bij elk nieuw blok haakjes te zetten, weten we zeker dat alles goed afgebakend is. Helaas levert dat vaak meer haakjes op dan noodzakelijk volgens de grammatica. In dit geval kunnen we deze formule reduceren naar de equivalente formule:

∀ x:M, slaapt x  → snurkt x

Algoritme

Organisatiestap: Teken een rechthoek, waarbinnen je alles uitvoert.

Verduidelijken.
- Verander de zin op zo'n manier dat het duidelijker wordt wat de (logische) structuur van de zin eigenlijk is, maar natuurlijk zonder de betekenis van de zin te veranderen. Voorbeelden:
  - Als je denkt dat de zin een negatie is, maak er dan van: „Het is niet het geval dat ...”
  - Als je denkt dat de zin een kwantorformule is, maak er dan van: „Voor alle ... geldt: ...” of „Er bestaat een ... waarvan geldt: ...”
  - Een disjunctie kun je ook opschrijven als: „Minstens één van de volgende eigenschappen is waar: 1. ...; 2. ...”
Kies één operator en vertaal die naar een formule.
- Schrijf ook op welke operator je nu aan het vertalen bent in de terminologie van de grammatica, dus (kwantor)formule, conjunctie, negatie, negatief, term etc.
Teken tussen de haakjes een nieuwe rechthoek, schrijf daar bovenin nieuwe hoofzinnen en pas op die hoofdzinnen nog eens dit algoritme toe.
Na afloop schrijf je de hele formule nog eens op, maar nu zonder overbodige haakjes.

Wiens vader iedereens vader is, die heeft elke man tot broer.

We oefenen dit algoritme op een complex voorbeeld.

Versie op 1 regel, verlangt een breed scherm

Wiens vader iedereens vader is, die heeft elke man tot broer.

(kwantor)formule

∀ x:M,

Als de vader van x iedereens vader is, dan is elke man een broer van x.

implicatie

De vader van x is iedereens vader.

(kwantor)formule

∀ v:M,

Als v de vader van x is, dan is v iedereens vader

implicatie

v is de vader van x.
term
isVaderVan v x

→

v is iedereens vader

(kwantor)formule

∀ i:M,

v is de vader van i.
term
isVaderVan v i

→

Elke man is een broer van x.

(kwantor)formule

∀ m:M,

Als m een man is, dan is m een broer van x.

implicatie

m is een man.
term
isMan m

→

m is een broer van x.
term
isBroerVan m x

Versie voor kleinere schermen

Wiens vader iedereens vader is, die heeft elke man tot broer.

(kwantor)formule

∀ x:M,

Als de vader van x iedereens vader is, dan is elke man een broer van x.

implicatie

De vader van x is iedereens vader.

(kwantor)formule

∀ v:M,

Als v de vader van x is, dan is v iedereens vader

implicatie

v is de vader van x.
term
isVaderVan v x

→

v is iedereens vader

(kwantor)formule

∀ i:M,

v is de vader van i.
term
isVaderVan v i

→

Elke man is een broer van x.

(kwantor)formule

∀ m:M,

Als m een man is, dan is m een broer van x.

implicatie

m is een man.
term
isMan m

→

m is een broer van x.
term
isBroerVan m x

6. Tijd

literatuur

...

Real-timesystemen zijn systemen die precies op tijd moeten reageren. Ze zijn vaak ingebouwd in machines, liften, verkeersregelingsinstallaties e.d. In Nijmegen doet de Informatica voor Technische Toepassingen hieromtrent veel onderzoek. Eigenlijk zijn, als je het goed bekijkt, alle systemen real-timesystemen, ook een salarisadministratie: als je salaris immers niet elke maand komt, is het fout. Maar niet bij elk systeem vindt men timing zo belangrijk en critisch dat men er in de correctheidsstelling aandacht aan besteedt. De Postbank zette bijvoorbeeld jaren lang elke avond om 23:00 het programma aan dat alle overschrijvingen van die dag verwerkt, en dat was gewoon een paar uur later klaar omdat tegenwoordig computers snel genoeg zijn. Men denkt na over correctheid van het beheer van alle rekeningen, er mag bij het overschrijven geen geld ontstaan of verloren gaan, er mag niets twee keer overgeschreven worden, maar "tijd speelt geen rol" omdat de nacht tussen twee werkdagen altijd lang genoeg was.

Bij systemen als een spoorwegovergang met lichten en slagbomen speelt tijd een cruciale rol. We pakken dat systematisch aan.

Keuze van een tijdsmodel

Als we gedrag willen specificeren waarbij tijd een rol speelt, moeten we als onderdeel van ons domeinmodel een geschikte wiskundige structuur voor de tijd kiezen. Hier een paar voorbeelden:

De belastingdienst werkt met kalenderjaren. Voor specificaties van delen van het belastingstelsel zijn jaargetallen als tijdsmodel voldoende.
Rente van spaarrekeningen wordt per dag berekend. Een tijdsmodel waarbij men over uren en minuten moet praten kan de zaak nodeloos ingewikkeld maken.
Een ouderwetse wijzerklok zonder datumtelling doet elk etmaal tweemaal precies hetzelfde. Een klok met een slinger van 1 m heeft seconden als kleinste eenheid. Om te beredeneren of een bepaald raderwerk een correcte klok oplevert, zijn hele getallen modulo 12*60*60 het meest geschikt: de seconden van een halve dag.
Binnen een vak als computerarchitectuur kan het adequaat zijn, alles te specificeren in termen van de klok van de processor.
Natuurkundigen modelleren tijd als reële getallen, met als eenheid de seconde. Als het in je werkstuk niet gaat om kalenderdagen en processorklokcycli maar om snelheden van voertuigen en duraties van processen als het openen van deuren, is dit misschien het meest voor de hand liggende tijdsmodel.

Je maakt een keuze en neemt in je domeinmodel een type T op met de nodige uitleg, bijvoorbeeld: "Natuurlijke getallen, eenheid sec".

type		betekenis (verzameling)		formele notatie t.b.v. Coq
T		de tijd in sec. in reële getallen		`Definition T := R.`

Observaties

De predikaten van het domeinmodel komen overeen met observeerbare gebeurtenissen in de reële wereld. Het predikaat is_mannelijk x is bijvoorbeeld waar als persoon x in de werkelijkheid inderdaad mannelijk is. We maken een observatie (natuurkundig: een meting) en weten of het predikaat waar of onwaar is.

Als tijd een rol speelt, verdient het aanbeveling, de predikaten van het domeinmodel te voorzien van een tijdparameter:

type		betekenis (verzameling)		formele notatie t.b.v. Coq
T		de tijd in sec. in reële getallen		`Definition T := R.`
S		de toestanden van sensoren: {actief, passief}		`Variable S:Set. Variable actief:S. Variable passief:S.`
D		de toestanden van slagbomen: {open, bewegend, dicht}		`Variable D:Set. Variable open:D. Variable bewegend:D. Variable dicht:D.`
predicaat	type	betekenis	meting	formele notatie
treinsensor	T→S→B	treinsensor t actief: op moment t zendt de treinsensor een puls treinsensor t passief: op moment t zendt de treinsensor geen puls	5 Volt op de sensorkabels 0 Volt op de sensorkabels	`Variable treinsensor:T->S->B.`
boom	T→D→B	boom t open: op moment t staan de bomen recht omhoog (5 graden omprecies te zijn) boom t bewegend: op moment t bewegen de bomen boom t dicht : op moment t staan de bomen horizontaal	kijken	`Variable boom:T->D->B.`

Loop je lijst van gegeven predikaten af en kijk welke op één moment waar, op een ander moment onwaar kunnen zijn; zij komen in aanmerking voor een tijdparemeter. Overigens: gezien dat steeds meer mensen tijdens hun leven van geslacht veranderen is het een kwestie van tijd dat de burgerlijke stand ook overgaat tot predicaten met een tijdsparameter: is_mannelijk datum x

Eigenlijk kom je bij het specificeren van real-timesystemen uit met één predikaat met drie parameters: wanneer, waar, wat. Je moet dan wel voor elke mogelijke waarde aangeven hoe deze gemeten kan worden.

type		betekenis (verzameling)
T		de tijd: Natuurlijke getallen, eenheid sec
L		de observatiepunten: zie lijst van observatiepunten
V		alle mogelijke waarden en toestanden: zie tabel van metingen
predicaat	type	betekenis	meting
obs	T→L→V→B	obs t l v: op observatiepunt l is op moment t de waarde v observeerbaar	zie tabel van metingen

Of je alles in termen van zo'n algemene obs specificeert of diverse predikaten als treinsensor als gegeven aanneemt, is grotendeels een kwestie van smaak. Je kunt ook het ene in je domeinmodel opnemen en het andere definiëren:

Definition treinsensor (t:T) (s:V) := obs t sensor s.

Echte tijd en representaties

Leer te onderscheiden tussen de fysieke tijd, d.w.z. de momenten waarop in de realiteit iets gebeurt en geobserveerd kan worden, en de representatie van momenten en duraties in het geheugen van een systeem.

Een kookwekker rinkelt op bepaalde momenten. Dat is de fysieke tijd. Op dat moment kun je iets observeren. Je kunt "een tijd instellen", maar dat is niet de fysieke tijd, dat is een wijzerpositie, of een cijfer op een schermpje. Op een bepaald moment kun je observeren dat het wijzertje op een bepaalde stand staat. Het is een instelling die een poos dezelfde blijft en die de gewenste kooktijd representeert. Als je een kookwekker op moment t instelt op kooktijd d, schrijf je zet t (repr d) om het verschil duidelijk te maken. t is onze tijdsparameter en geeft het daadwerkelijke moment aan waarop de handeling van het instellen plaats vindt. repr d is de representatie van een kooktijd, bijvoorbeeld in de vorm van de positie van een instelschroef. De functie repr moet je uiteraard wel definiëren.

7. Vereenvoudigingen

literatuur

Taxonomy/1. Quality/02. Models

We hebben eerder geleerd dat men beweringen, met name specificaties en blauwdrukken, beter kernachtig en goed opgemaakt kan opschrijven en dat men definities kan gebruiken om alles op precies één plek te schrijven.

Ook hebben we geleerd dat men een probleem vanuit verschillende gezichtspunten kan behandelen en onder elk gezichtspunt van veel dingen abstraheren.

Maar dan nog kunnen formules erg complex en onoverzichtelijk worden en hun controle en verwerking te moeilijk - zelfs voor computers.

Manieren om een specificatie overzichtelijk te houden

kernachtig en leesbaar: niet meer schrijven dan nodig is, en dit gesructureerd opmaken
definities: dingen maar op één plek zeggen
abstractie: niet over (voor het gekozen gezichtspunt) irrelevante dingen praten
idealisatie: verwaarloosbare hoeveelheden als 0 behandelen

Bij de besturing van de wissels en seinen van een spoorweg moet alles op het juiste moment gebeuren. Van de tijd kunnen we onmogelijk abstraheren. Bij het redeneren erover of alles correct gebeurt, moeten we voortdurend over momenten en duraties praten. Alles kost tijd: het rijden van de treinen, het bewegen van slagbomen, wissels, seinen, de berekeningen in het besturingskastje en de geleiding van stroom in de kabels. Moeten we al deze duraties ook in de formule meenemen?

Gelukkig niet. Hier kunnen we leren van de natuurkunde.

Terug naar de correctheidsstelling van onze deurbel. Streng genomen kan zo 'n deurbel als gespecificeerd niet bestaan, want de snelheid van de stroom in kabels is beperkt. Het rinkelt altijd ietsjes later dan de knop ingedrukt was. Een eerlijke specificatie zou die vertraging noemen, al dan niet gecontroleerd vaag. Natuurkundigen weten heel goed wanneer ze oneerlijk mogen doen alsof iets geen tijd kost, geen ruimte inneemt of geen wrijving heeft. Ze →verwaarlozen bepaalde kleine hoeveelheden. In deze traditie mogen we bij een huis- tuin- en keukendeurbel doen alsof de snelheid van stroom oneindig is. Maar we moeten wel goed weten wanneer zoiets mag, zie Beweren en bewijzen/de zuilen/Artefacten/6. Domeintheorie.

Zo ook bij de spoorwegovergang: de tijden die de computer nodig heeft voor zijn berekeningen (enkele microseconden) en de tijden die nodig zijn om seinen om te schakelen (minder dan één seconde) vallen in het niets t.o.v. de tijden die bij de verkeersleiding en beveiliging een rol spelen (tientallen seconden, soms vele minuten). Hier is verwaarlozing van de reken- en schakeltijden verantwoord. Zo hoeven in de formules niet voor te komen omdat we net doen alsof ze nul zijn.

Wisseltijden daarentegen worden niet verwaarloosd. Dat zijn relevante momenten omdat voor het vrijgeven en omschakelen de vorige trein de hele wissel verlaten moet hebben en hij pas weer gereserveerd kan worden voor een opvolgende trein als de wissel correct is vergrendeld. Het duurt ca. (n + 1) ∙ 6 sec om n wissels om te zetten. Men zet wissels niet precies tegelijk om om te vermijden dat er een grote piek in de stroombelasting komt. Deze tijden zijn relevant omdat die orde-grootte al relatief dicht bij die van de afstand tussen treinen ligt (typisch 2–3 minuten). Dan is 12 sec al 7–10%, en het omschakelen van wissels verkleint de capaciteit behoorlijk.

Ook niet verwaarloosd wordt de zichttijd, de tijd die een machinist nodig heeft om een sein te zien. Het sein moet dus al enkele seconden voordat de trein in de buurt komt op de juiste stand gezet worden.

Overlijdensakten en soortgelijke documenten verwaarlozen soms het precieze moment van het overlijden en noemen alleen de datum [4]. Dat is voldoende informatief voor een (weduwen- of wezen)pensioenfonds, maar bij bepaalde erfkwesties kan dat te weinig exact zijn.

8. Parametrisatie

literatuur

...

De algemene vorm van de correctheidsstelling voor systemen

∀ φ, ∀ ψ, ∀ Φ, ∀ Ψ,
        Π(φ, ψ, Φ, Ψ)
    →
            N ∧ (∀ i ∈ {1, 2, ..., n}, a_i(φ_i) → c_i(ψ_i))
        →
            A(Φ) → C(Ψ)

Hierbij betekent:

a_i(φ_i) → c_i(ψ_i) is de specificatie van onderdeel i.
A(Φ) → C(Ψ) is de specificatie van het geheel.
φ en ψ zijn de parameters van de onderdelen en Φ en Ψ de parameters van het geheel. Met deze parameters kun je een specificatie algemener maken, zodat ze b.v. geldt voor snelle en langzame onderdelen.
Π(φ, ψ, Φ, Ψ) geven algemene voorwaarden aan zodat de parameters bij elkaar passen.
N geeft relevante natuurwetten en domeinkennis aan.

Beweren en bewijzen/de zuilen/Formalisering

Inhoud

Men moet kunnen praten

Het moet kloppen

Syntactisch correct

Syntactisch eenduidig

Volledig

Kernachtig

Semantisch eenduidig

Consistent

Formele talen

Geformaliseerde natuurlijke taal

Leesbaar

Ons speelveld

Exemplarische onderwerpen

Exemplarische talen

Voorbeelden

Oven

CD-speler

Politielasergun

Ambitieniveaus

Informeel

Kwalitatief

Kwantitatief

Namen i.p.v. waarden

Generieke correctheidsstelling

Bewijsassistenten

Rollen

Wat als iets mis gaat?

Wie slaapt, snurkt

Verkenning

Systematisch

Algoritme

Wiens vader iedereens vader is, die heeft elke man tot broer.

Versie op 1 regel, verlangt een breed scherm

Versie voor kleinere schermen

Keuze van een tijdsmodel

Observaties

Echte tijd en representaties

De algemene vorm van de correctheidsstelling voor systemen

Navigatiemenu

zoek