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
- 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
- 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.
- 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:
- 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?