Beweren en bewijzen/de zuilen/Formalisering/4. Correctheidsstelling
| literatuur
PencastWhat? 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 si,
- waarbij in alle si 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 si samen,
dan weten we dat het artefact doet wat het moet doen.
Dat S een geldig gevolg is van alle si samen, wordt in de logica genoteerd als:
s1, s2, s3, ... , sn |= S
Dit noemen we een correctheidsstelling van artefact A als S een specificatie van artefact A is, de si specificaties van onderdelen van A en S daadwerkelijk een geldig gevolg is van de si samen.
Als we een artefact willen ontwerpen dat aan een gegeven specificatie S moet voldoen, moeten we dus si 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 [1].)
Als de specificaties s1 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:
s1∧s2∧s3∧ ... ∧sn → S
Inhoud
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
Scheiding van belangen
- Opdrachtgever
s1/\s2/\..../\sn→S
- Ontwerper
s1∧s2∧ ... ∧sn→S
- Leverancier
s1/\s2/\..../\sn→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.
