Semantische analyse van Piet middels een

vergelijking met While

Eerste opzet

Mart Lubbers  Marjolein Zwerver

20 maart 2014

Inhoudsopgave

1 Introductie 2 1.1 Piet . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Beschrijving en gelijkenis met While . . . . . . . . . . . . . . . . . . . . . 2

2 Syntax 3 3 Semantiek 3 4 Analyse 3 5 Planning 4

1 Introductie

1.1 Piet

Piet is een esoterische, stack georiënteerde en geïnterpreteerde programmeertaal die is geïspireerd door de Nederlandse kunstenaar Piet Mondriaan. Programma geschreven in piet kunnen eruit zien als abstracte kunst en worden aangeleverd als een afbeelding. Een programma dat zijn doel nastreeft is bijvoorbeeld het volgende programma dat het woord ”Tetris”print en iedere groep blokken een blok is uit het originele Tetris spel.

1.2 Beschrijving en gelijkenis met While

Het belangrijkste verschil tussen Piet en While is het programmeer paradigma dat word gebruikt, Piet is een stack georiënteerde taal waar While een imperatieve taal is. De benadering is hierdoor totaal verschillend maar de een moet wel in de ander uit te drukken zijn. Stack georiënteerd betekent dat variabelen opslag in een stack gebeurt. Een stack is een geordende rij van, in het geval van Piet, gehele getallen. Instructies worden gegeven aan de interpreter door een bepaalde overgang in kleur naar de volgende codel^{1}, de volgende codel word bepaald door de richting van de interpreter. Er zijn twee verschillende overgangen mogelijk die beide cyclisch zijn, dat wil zeggen dat de opvolger van het laatste element het eerste element is. Dit maakt het totale aantal commando’s gelijk aan 6 ∗ 3 − 1 = 17.

• Tint: rood→ geel→ cyaan→ blauw→ magenta

• Intensiteit: licht→ normaal→ donker

De instructies die de overgangen uitdrukken staan beschreven in de onderstaande tabel, merk op dat zwart een blokkade is en wit een blok waar de interpreter overheen leest.

Tint\Intensiteit 0 donkerder 1 donkerder 2 donkerder
0 stappen  -  push  pop
1 stap  add  subtract  multiply
2 stappen  divide  mod  not
3 stappen  greater  pointer  switch
4 stappen  duplicate  roll  in(number)
5 stappen  in(char)  out(number) out(char)

1Een codel is blok n × n pixels waarbij n ∈ ℕ^{+}

2 Syntax

Omdat Piet niet heel complex is gaan we voor dit werkstuk de hele taal beschrijven. Tijdens het interpreteren van een Piet programma wordt een serie commandos uitgevoerd in een bepaalde toestand.

De grammatica ziet er zo uit: S ::= S1; S2 | push n1 | pop z | add z1 z2 | subtract z1 z2 | multiply z1 z2 | divide z1 z2 | mod z1 z2 | not z | greater z1 z2 | pointer z | switch z | duplicate z | roll z1 z2 | in(char) c | in(number) z | out(char) z | out(number) z waarbij n ∈ ℕ, z ∈ ℤ en c ∈ {1, 2, ..., m waar m het nummer is van het hoogste unicode karakter. Een probleem dat we verwachten is dat we op met deze beschrijving zeer grote bewijsbomen/rijen krijgen vanwege het grote aantal composities, hier moeten we misschien nog iets anders op verzinnen.

3 Semantiek

Bij natuurlijke semantiek(ns) ligt de nadruk op de relatie tussen de begin en de eind state. Het nadeel hiervan is dat programmas die niet termineren geen bewijsbomen hebben. Hierdoor is het niet mogelijk om eigenschappen te bewijzen voor zulke programmas. Bij structurele operationele semantiek(sos) ligt de nadruk juist op de individuele stappen van de executie en heeft wel bewijsrijen voor programmas die niet termineren. Om deze redenen hebben we gekozen voor sos. Een toestand in onze semantiek word beschreven door drie stacks; input, output en programma. Respectievelijk benoemen we deze met s_{i}, s_{o}, s en beschrijven ze de STDIN, STDOUT en interne stack van het programma. Stacks worden gerepresenteerd als: s = {n_{0}, n_{1}, ..., n_{n}} waarbij n_{i} ∈ ℤ Het transitie systeem zal twee verschillende transities kennen, namelijk: s → ⟨S, s_{i}, s_{o}, s⟩ en s → ⟨s_{i}, s_{o}, s⟩ Waarbij de laatste transitie duidt op een terminerende transitie en de eerste op een niet terminerende transitie. Bij de semantiek verwachten we nog een klein probleem dat te maken heeft met het feit dat we nog niet precies weten hoe we de righting van het programma en moeten implementeren, ook weten we nog niet of dit überhaupt nodig is in de semantiekbeschrijving.

4 Analyse

Voor onze analyse gaan we bewijzen dat voor elk programma in de taal While een semantisch equivalent programma in de taal Piet bestaat. Dit gaan we doen door voor elke constructie in While een programma in Piet te geven en vervolgens te bewijzen dat deze semantisch equivalent zijn met behulp van bewijsrijen in sos.

5 Planning

Week Dinsdag  Donderdag
10  Groep indeling en onderwerp

11

12  Opzet
13  Introductie af(verbeteren)
14  Kwartaalonderbreking
15 Kwartaalonderbreking Kwartaalonderbreking
16  Syntax en semantiek af
17  Analyse voor axiomas af
18  MEIVAKANTIE  MEIVAKANTIE
19  Voortgangsbespreking  Eerste versie
20  Analyse voor if af
21  Analyse voor while af
22  HEMELVAART
23  Demonstrerend piet programma/compiler/interpreter?
24  Definitieve versie

25

26  Eindbespreking  Eindbespreking
27  Eindbespreking  Eindbespreking