Leertaak 6

Structurele operationele semantiek en uitbreidingen van While

Achtergrond

Semantiek van programma's en programmeerconstructies kan op verschillende manieren vastgelegd worden. De stijl van natuurlijke semantiek karakteriseert de uitkomst van een statement (in termen van uitkomsten van andere statements). Structurele operationele semantiek (sos) is een beschrijvingsvorm die zich richt op de rekenstappen die leiden tot de uitkomst. Daarmee is deze sos-methode bij uitstek geschikt als hulpmiddel voor het construeren van compilers en interpreters. Ook informatici die berekeningen analyseren zullen doorgaans de voorkeur geven aan sos-semantiek.

Voor het specificeren van semantiek van taaluitbreidingen maakt een informaticus een keuze voor een bepaalde beschrijvingsmethode. Daarbij spelen verschillende overwegingen een rol. In deze leertaak maken we (voor enkele specifieke uitbreidingen) kennis met een paar van deze overwegingen en met de overeenkomsten en verschillen tussen de ns- en sos-benadering.

Leerdoel

Na het voltooien van deze taak kunt u

Instructie

  1. Lees p. 32-36. Kernbegrippen:
  2. Werk Exercise 2.16 (p. 35) uit.
  3. Construeer een sos-semantiekbeschrijving van een zelf gekozen loop-variant, bijvoorbeeld de repeat-until of de for-do. Zie bijvoorbeeld Exercise 2.17 en Exercise 2.18 (p. 36).
  4. Lees p. 36-39.
  5. Maak Exercise 2.21.
  6. Op p. 39 staat de definitie van semantische equivalentie. Die bestaat uit twee eigenschappen gekoppeld via een 'en'. Wat als die twee eigenschappen niet met een 'en' maar met een 'of' zouden zijn gekoppeld? Zou u het dan ook een zinnige definitie noemen? Geef een toelichting.
  7. Lees p. 40 (tot aan Lemma 2.27). Theorem 2.26 geeft de equivalentie van ns- en sos-semantiek weer in een alternatieve notatie, die er nu even niet toe doet; de uitleg eronder is voorlopig voldoende.
  8. Lees p. 44-46 (het gedeelte 'Abortion'). Werk het eerste gedeelte van Exercise 2.32 uit: karakteriseer de semantiek van het 'assert'-statement.
  9. Kies één van de onderwerpen 'Non-determinism' en 'Parallelism'. (Het is de bedoeling dat beide aan bod komen -- enige onderlinge coördinatie is dus gewenst.) Lees het betreffende gedeelte: p. 46-48 resp. p. 48-50.
  10. Beantwoord Exercise 2.33 (als u voor 'Non-determinism' hebt gekozen) respectievelijk 2.35 ('Parallelism').

Product

Reflectie