Leertaak 4

Inleiding axiomatische semantiek

Achtergrond

Eigenschappen van (de werking van) programma's zijn te bewijzen aan de hand van een gegeven operationele semantiek. Correctheid van programma's kunnen we formuleren in termen van eigenschappen van toestanden vóór en na de uitvoering van het programma, en vervolgens het semantisch gereedschap gebruiken om deze eigenschappen te bewijzen.

Deze strategie is vaak wat omslachtig. Daarom zijn er formele systemen ('correctheidscalculi') gemaakt waarin eigenschappen van programma's rechtstreeks kunnen worden afgeleid met behulp van regels die de opbouw van statements volgen: net zoals de ns- en sos-semantiek. Eigenlijk is een correctheidscalculus dus een alternatieve manier om semantiek te beschrijven: niet in termen van toestanden, maar in termen van eigenschappen.

Leerdoel

Na het voltooien van deze taak kunt u

• onderstaande kernbegrippen (zie 'Werkwijze') verklaren;
• verschillende methoden voor het bewijzen van programma-eigenschappen aangeven;
• de afleidingsregels voor partiële correctheid verklaren.
• de afleidingsregels gebruiken om de eigenschappen van programma's aan te tonen.

Instructie

1. Lees p. 169-172 en p. 175-180. Kernbegrippen:
   • partiële correctheid, totale correctheid
   • 'directe' correctheidsbewijzen via semantiek
   • assertie, preconditie, postconditie
   • assertie-taal, intensioneel, extensioneel
   • axiomatische semantiek, afleidingssysteem
2. Bewijs de correctheid van het 'faculteitsprogramma' in Example 6.9 (p. 181). Gebruik de notatie die we in deze cursus hebben ingevoerd: geef uw correctheidsbewijs in de vorm van annotaties (volgens de afleidingsregels) in het programma.
3. Ontwikkel stapsgewijs een correctheidsbewijs.
   • Beschouw het volgende programma.
     

         z := 0;
         odd := 1;
         sum := 1;
         while sum <= x
         do ( z := z + 1;
              odd := odd + 2;
              sum := sum + odd )
     

   • Maak een tabel met het verloop van de waarden van z, odd en sum gedurende drie iteraties van de while-loop:
     
     

     z	odd	sum
     0
     1
     2
     3

   • Toon aan dat dit programma een worteltrekking uitvoert: als x initieel waarde n heeft en n is een natuurlijk getal, dan heeft z uiteindelijk de waarde van wortel-n (naar beneden afgerond). Hint: dat wil zeggen: z^2 <= n en (z+1)^2 > n.

Product

• Correctheidsbewijs in de vorm van een geannoteerd programma.
• Ingevulde tabel.
• Correctheidsbewijs van het worteltrekprogramma.

Reflectie

• Gebruikt u de vereenvoudigingen in de assertietaal die we in het college hebben afgesproken?
• Zijn programmavariabelen en logische variabelen op de juiste manier gebruikt?
• Worden de metavariabelen alle gedeclareerd, gedefinieerd of gequantificeerd?
• Zijn de annotaties volledig: komen ze overeen met de afleidingsregels?
• Zou u desgevraagd ook een afleidingsboom kunnen tekenen voor uw correctheidsbewijs?