Leertaak 5
Correctheidsregels, soundness en completeness
Achtergrond
Voor een uitbreiding van een programmeertaal specificeren
we de syntax en operationele semantiek. Eventueel breiden we de correctheidscalculus
uit met regels voor de betreffende nieuwe statements.
Omdat het formele systeem af en toe wordt uitgebreid, is
het belangrijk om de 'meta-eigenschappen' consistentie (soundness)
en volledigheid (completeness) te kunnen verifiëren.
Leerdoel
Na het voltooien van deze taak kunt u
- onderstaande kernbegrippen (zie 'Werkwijze') verklaren;
- correctheidsregels voor uitbreidingen van de taal While construeren;
- de soundness van nieuwe correctheidsregels nagaan;
- bij een gegeven statement en postconditie de bijbehorende zwakste preconditie bepalen.
Instructie
- Lees p. 183-190. Kernbegrippen:
- invariant
- bewijsbaar equivalent
- soundness, completeness
- valid ('geldig', 'waar')
- wlp
- We breiden de taal While uit met nondeterministische
keuze (or): zie p. 46 voor syntax en natuurlijke semantiek. Geef een bewijsregel (axiomatische semantiek) voor or.
- Toon aan dat uw bewijsregel sound is ten opzichte van de standaard semantiek.
- Laat zien dat de (misschien voor de hand liggende) alternatieve regel voor
de toewijzing
[asspalt] { true } x := a { x = a }
niet sound is.
- Ontwerpers en gebruikers van bewijsregels en -tools hechten doorgaans meer
waarde aan soundness dan aan completeness
van hun systemen. Kunt u dit verklaren? Licht in uw betoog de betekenis en
de wenselijkheid van beide eigenschappen kort toe.
- Bepaal de zwakste preconditie P in de volgende gevallen.
Schrijf P zo simpel mogelijk op.
- { P } x := x+10 { x>0 }
- { P } x := x+x { x>0 }
- { P } x := x+y { x=2y }
- { P } x := x+y { x=-1 en y=1 }
- { P } x := 2*y; w := -x { x>y en y>0 en wx>=0 } (*)
- { P } x := x+1 { true }
- { P } x := (m+n) div 2 { m<=x<=n }
- { P } x := x div y { x = 7 }
- { P } z := 0 { er bestaat w zodat x^2 + y^2 = w^2 en z=0 }
- { P } if x = 2*y then x := 3 else y := x div 3 { x=3y }
- { P } if x = y then x := 0 else y := 0 { x = y }
- { P } if x < 0 then x := x+2 else skip { x>0 } (*)
Opmerking: de regels met (*) zijn na het responsiecollege op triviale wijze
aangepast.
Product
- Een afleidingsregel voor or.
- Een bewijs van soundness.
- Redenering over niet-soundness van de alternatieve
regel.
- Vergelijking tussen soundness en completeness.
- Een lijstje van zwakste precondities bij de gegeven statements.
Reflectie
- Is de afleidingsregel eenduidig geformuleerd? Kunt u hem motiveren?
- Is de redenering in het soundness-bewijs helder? Benoemt en bewijst u de
tussenresultaten systematisch? Is het duidelijk met betrekking tot welke semantiek
de regel sound is? Op welke manier volgt nu de soundness van het gehele systeem?
- Is uw bewijs van de ongeldigheid van de assignmentregel kernachtig? Geeft
u een redenering of een concreet tegenvoorbeeld?
- Is elk van uw precondities inderdaad een preconditie? Is het evident dat
het inderdaad de zwakst mogelijke zijn?