Leertaak 3
Herhalingsconstructies en semantische equivalentie
Achtergrond
Een formele semantiekbeschrijving kan helpen bij het vastleggen
van ontwerpbeslissingen over de uitvoering van nieuwe taalconstructies. Ook
het analyseren van (vaak subtiele) verschillen in werking verloopt vaak aan
de hand van afleidingsregels.
Informatici die programmatransformaties ontwerpen (bijvoorbeeld
voor optimalisatie binnen een compiler), zullen moeten aantonen dat de getransformeerde
programma's tot dezelfde uitkomsten leiden als de oorspronkelijke. Deze relatie
tussen programma's noemen we semantische equivalentie.
Leerdoel
Na het voltooien van deze taak kunt u
- onderstaande kernbegrippen (zie 'Instructie') verklaren;
- semantiekregels opstellen voor nieuwe varianten van herhalingsstatements;
- verschillen in uitvoeringsgedrag uitleggen aan de hand van de formele semantiek;
- semantische equivalentie van statements (ten opzichte van ns) aantonen.
Instructie
- Lees p. 26-30. Kernbegrippen:
- semantische equivalentie
- inductie naar de opbouw van afleidingsbomen
- gedetermineerdheid
- Beantwoord de opgave over for-loops in de bijlage.
- Breid de taal While uit met een repeat-until
constructie. De semantiek van deze uitbreiding (in natuurlijke-semantiekstijl)
hebben we eerder al beschreven.
- Tijdens het hoorcollege hebben we gewerkt aan het bewijs van semantische
equivalentie van
repeat S until b en S; while ¬b do S .
Werk de tweede helft van het bewijs uit: bewijs voor elke s, s':
als <S; while ¬b do S, s> —> s' ,
dan <repeat S until b, s> —> s' .
Product
- Uitleg over het effect van toewijzingen op het aantal herhalingen van de
loop.
- Alternatieve semantiekregels voor het for-statement.
- Statements die een verschil in terminatiegedrag aantonen.
- Tweede helft van het bewijs van semantische equivalentie.
Reflectie
- Is de structuur van de redeneringen helder? Zijn de bewijsstappen duidelijk
aangegeven?
- Is de specificatie van de semantiek van loop-statements onafhankelijk van
de semantiek van andere taalconstructies?
- Bij elk bewijs: maakt u gebruik van een inductieprincipe? Zo ja, welk? Blijkt
dit duidelijk uit de formulering? Is de inductiehypothese expliciet benoemd?