Leertaak 2

Afleidingsregels voor natuurlijke semantiek

Achtergrond

Eén van de stijlen om semantiek van programmeertalen vast te leggen is de 'natuurlijke semantiek'. Met behulp van afleidingsregels kan het effect van taalconstructies trefzeker en beknopt worden weergegeven. Dat maakt deze vorm van beschrijven zeer geschikt om te gebruiken in specifcaties van programmeertalen.

De betekenis van concrete statements kan met behulp van afleidingsbomen in het systeem worden aangetoond. In het geval van complexere statements is deze gestileerde aanpak niet zo geschikt voor gebruik door mensen, maar des te meer voor de inzet in systemen voor computerondersteunde verificatie.

In veel situaties is het belangrijk om precies en trefzeker te kunnen redeneren over de werking van programma's. Analyse van het terminatiegedrag van programmafragmenten is zo'n geval. We kunnen het formele systeem van natuurlijke semantiek niet alleen gebruiken om te laten zien dat een programma tot een bepaald resultaat leidt (en dus termineert), maar ook om te staven dat een bepaald statement niet termineert ('looping').

Leerdoel

Na het voltooien van deze taak kunt u

• onderstaande kernbegrippen (zie 'Instructie') verklaren;
• van gegeven statements de semantiek bepalen;
• deze semantiek aan de hand van afleidingen motiveren;
• semantiekregels opstellen voor nieuwe varianten van herhalingsstatements;
• de semantiekregels hanteren om terminatie-eigenschappen van statements te beredeneren.

Instructie

1. Lees p. 19-25. Kernbegrippen:
   • natuurlijke semantiek
   • afleidingsregel, instantie, premisse, conclusie, voorwaarde (condition), axioma
   • afleidingsboom
   • terminatie, looping
2. Beantwoord Exercise 2.3 op p. 25. Bepaal eerst 'met de hand' de semantiek van het gegeven statement; geef daarna de rechtvaardiging met behulp van een afleidingsboom.
3. Lees Paragraaf 14.13 van de Java Language Specification over het do statement.
4. Breid de BNF voor While uit met syntax voor een do statement.
5. Geef de semantiek voor deze uitbreiding in de stijl van Natuurlijke semantiek (Tabel 2.1 van Nielson & Nielson). Licht uw afleidingsregel(s) toe.
6. Bepaal van elk van de statements in Exercise 2.4 (p. 25) of het altijd termineert en of altijd 'loopt'. Staaf uw antwoord voor één van de statements met een redenering aan de hand van de semantiekregels. (Het is natuurlijk prettig als binnen de groep alle drie de statements aan bod komen.)

Product

• Aanduiding van de semantiek van het statement in Exercise 2.3. Een afleidingsboom om de uitkomst te staven.
• Beschrijving van syntaxis en semantiek van het 'do' statement. Motivatie van de afleidingsregel(s).
• De uitkomst van de terminatie-analyse voor de drie statements. Een uitgewerkte redenering voor één ervan.

Reflectie

• Is de weergave van de afleidingsboom overzichtelijk? Zijn de parameters in de afleidingsregels (substatements S, S1, S2, states s, s', etc.) correct ingevuld met concrete statements en states?
• Is de toelichting bij de semantiekdefinite van het nieuwe statement duidelijk voor een informaticus die vertrouwd is met de terminologie en uitleg op p. 20-22 van Nielson & Nielson?
• Maakt een bewijs van 'looping' gebruik van het formalisme van afleidingsregels en afleidingsbomen?