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

1. Lees p. 183-190. Kernbegrippen:
   • invariant
   • bewijsbaar equivalent
   • soundness, completeness
   • valid ('geldig', 'waar')
   • wlp
2. 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.
3. Toon aan dat uw bewijsregel sound is ten opzichte van de standaard semantiek.
4. Laat zien dat de (misschien voor de hand liggende) alternatieve regel voor de toewijzing

   [ass_p^alt] { true } x := a { x = a }

   niet sound is.
5. 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.
6. Bepaal de zwakste preconditie P in de volgende gevallen. Schrijf P zo simpel mogelijk op.
   1. { P } x := x+10 { x>0 }
   2. { P } x := x+x { x>0 }
   3. { P } x := x+y { x=2y }
   4. { P } x := x+y { x=-1 en y=1 }
   5. { P } x := 2*y; w := -x { x>y>0 en wx>=0 }
   6. { P } x := x+1 { true }
   7. { P } x := (m+n) div 2 { m<=x<=n }
   8. { P } x := x div y { x = 7 }
   9. { P } z := 0 { er bestaat w zodat x^2 + y^2 = w^2 en z=0 }
   10. { P } if x = 2*y then x := 3 else y := x div 3 { x=3y }
   11. { P } if x = y then x := 0 else y := 0 { x = y }
   12. { P } if x < 0 then x := x+2 { x>0 }

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?