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

Instructie

  1. Lees p. 26-30. Kernbegrippen:
  2. Beantwoord de opgave over for-loops in de bijlage.
  3. Breid de taal While uit met een repeat-until constructie. De semantiek van deze uitbreiding (in natuurlijke-semantiekstijl) hebben we eerder al beschreven.
  4. 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

Reflectie