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
- onderstaande kernbegrippen (zie 'Instructie') verklaren;
- van gegeven statements de semantiek volgens sos bepalen;
- sos-semantiekregels opstellen voor nieuwe varianten van herhalingsstatements;
- het verband tussen ns- en sos-semantiek van de taal While aangeven;
- overeenkomsten en verschillen tussen ns- en sos-semantiek bij uitbreidingen
van While met expliciete stop-instructie, nondeterministische keuze en parallellisme
aangeven en verklaren;
- voor een (informeel) gegeven uitbreiding de ns- en sos-semantiek vastleggen
en met elkaar vergelijken.
Instructie
- Lees p. 32-36. Kernbegrippen:
- structurele operationele semantiek
- hangende (stuck) configuratie
- afleidingsrij (derivation sequence)
- terminatie, succesvolle terminatie, looping
- Werk Exercise 2.16 (p. 35) uit.
- 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).
- Lees p. 36-39.
- Maak Exercise 2.21.
- 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.
- 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.
- Lees p. 44-46 (het gedeelte 'Abortion'). Werk het eerste gedeelte van Exercise
2.32 uit: karakteriseer de semantiek van het 'assert'-statement.
- 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.
- Beantwoord Exercise 2.33 (als u voor 'Non-determinism' hebt gekozen) respectievelijk
2.35 ('Parallelism').
Product
- De berekeningsrij voor het statement in Exercise 2.16. Specificatie van
een state waarin de berekeningsrij oneindig is.
- Een specificatie van (syntaxis en) sos-semantiek van een loopconstructie.
- Uw uitwerking van Exercise 2.21.
- Uw mening over de alternatieve definitie van semantische equivalentie.
- Karakterisering van de semantiek van 'assert'.
- De uitwerking van Exercise 2.33 respectievelijk 2.35.
Reflectie
- Is uw redenering voor de oneindigheid van de berekeningsrij kernachtig?
Heeft u overtuigend bewezen dat er een regelmaat of herhaling ten grondslag
ligt aan die oneindigheid?
- Is de sos-karakterisering van het gekozen herhalingsstatement eenduidig
en is de toelichting adequaat?
- Is de specificatie van de semantiek van loop-statements onafhankelijk van
de semantiek van andere taalconstructies?
- Snapt u hoe bewijzen naar de lengte van de afleidingsrij werken?
- Als u de alternatieve definitie van semantische equivalentie niet zinnig
vond, heeft u dat dan met een vaag verhaal toegelicht of juist met concrete
voorbeelden?
- Sluit uw 'assert'-semantiek aan bij de stijl van de sos-semantiek in Tabel
2.2?