--- /dev/null
+\subsection{Aritmatische expressies}
+Het uitrekenen van een arithmatische expressie in \textit{Piet} moet in
+verschillende stappen gebeuren. Volgens de regels van de wiskunde worden er
+telkens binaire operaties uitgevoerd tot het vereenvoudigd is tot een enkele
+numerieke waarde. Het opvragen van variabelen uit het geheugen word in een
+volgende subsectie besproken en we gaan er nu van uit dat dat een triviale
+operatie is die een of twee variabelen boven aan zetten op een gekozen
+volgorde.\\
+Na het opvragen van variabele $n$ wordt de variabele boven aan gezet en krijgen
+de andere variabelen automatisch andere nummers. De variabelen met een positie
+strict kleiner dan $n$ krijgen een positie verhoging van $1$ en de variabelen
+met een positie strict groter dan $n$ krijgen een positie verlaging van $1$.\\
+Bijvoorbeeld bij de expressie $1+1$ is de eerste stap twee keen een $1$ op de
+stack duwen en vervolgens de binare $+$ operator toe te passen en dat gaat als
+volgt:\\
+\textbf{While} $x := 1 + 1$\\
+\textbf{Piet}
+\begin{tabular}{cccc}
+ {\color{red}\#} &
+ {\color{dred}\#} &
+ {\color{lred}\#} &
+ {\color{lyellow}\#}
+\end{tabular}\\
+\textbf{Piet'} $push 1, push 1, add$\\
+
+\textbf{While} $x := y + 3 * 2$\\
+\textbf{Piet}
+\begin{tabular}{cccccccc}
+ {\color{red}\#} & {\color{dred}\#} & {\color{dred}\#} & {\color{lred}\#}
+ {\color{dyellow}\#} & ...variable retrieval... & {\color{dyellow}\#} &
+ {\color{dgreen}\#}\\
+ {\color{red}\#} & {\color{dred}\#}\\
+\end{tabular}\\
+\textbf{Piet'} $push 2, push 3, mul, get y, add$\\
+
+\subsection{Booleaanse expressies}
+Het evalueren van booleaanse expressies gaat hetzelfde als aritmatische
+expressies, het enige verschil is dat er binnen de booleanse operatoren
+operatoren bestaan die niet voorkomen in \textit{Piet} en deze moeten dus
+herschreven worden. De operatoren die herschreven worden zijn: $=, \leq,
+\wedge\\
+\begin{array}{ll}
+ a \wedge b & a+b>1\\
+ a = b & \neg(a-b>0)\\
+ a \leq b & \neg(a>b)
+\end{array}$\\
+\textbf{While} $3=2\wedge 3\leq 4$\\
+\textbf{Piet}
+\begin{tabular}{ccccccccccccccc}
+ {\color{red}\#} & {\color{dred}\#} & {\color{lred}\#} & {\color{yellow}\#}
+ & {\color{dyellow}\#} & {\color{lyellow}\#} & {\color{dgreen}\#} &
+ {\color{dmagenta}\#} & {\color{lyellow}\#} & {\color{yellow}\#} &
+ {\color{blue}\#} & {\color{dred}\#} & {\color{magenta}\#} &
+ {\color{dmagenta}\#} & {\color{green}\#}\\
+ {\color{red}\#} & {\color{dred}\#} & & & & & & & {\color{lyellow}\#} &
+ {\color{yellow}\#}\\
+ {\color{red}\#} & & & & & & & & {\color{lyellow}\#} & {\color{yellow}\#}\\
+ & & & & & & & & & {\color{yellow}\#}
+\end{tabular}\\
+\textbf{Piet'} $push 3, push 2, sub, push 1, push 1, sub, gre, not, push 3,
+ push 4, gre, not, add, push 1, gre$\\
--- /dev/null
+\subsection{Assignment}
+Het toewijzen van waarden aan variabelen kost in \textit{Piet} een stuk meer
+werk omdat \textit{Piet} alle variabelen in een stack op slaat. Variabelen in
+piet kunnen we nummers toewijzen. De diepte van de variabele in de stack
+bepaald het nummer en als we aan de hand daarvan. Als er een assignment gedaan
+wordt krijgt de variabele nummer $1$ en alle nummers van de bestaande
+variabelen stijgen met $1$. Als er dus een waarde $n$ wordt toegewezen aan een
+naam dan moet er een blok gemaakt worden van grootte $n$ en dan een push gedaan
+worden op de volgende manier:\\
+\textbf{While} $x := 1$\\
+\textbf{Piet}
+\begin{tabular}{cc}
+ {\color{red}\#} & {\color{dred}\#}\\
+\end{tabular}\\
+\textbf{Piet'} $push 1$\\
+\textbf{While} $x := 5$\\
+\textbf{Piet}
+\begin{tabular}{cc}
+ {\color{red}\#} & {\color{dred}\#}\\
+ {\color{red}\#} & {\color{red}\#}\\
+ {\color{red}\#} & {\color{red}\#}
+\end{tabular}\\
+\textbf{Piet'} $push 5$\\
+Bij arithmatische expressies vindt automatisch een toewijzing plaatst doordat
+de uitkomst van de expressie boven op de stack staat en dus aan een waarde
+toegewezen word.\\
+Merk op dat de waarde $0$ niet gepushed kan worden dus om de waarde $0$ op de
+stack te krijgen moet men $n-n$ uitvoeren.
+%Notes: op een gegeven moment kan het sneller door een waarde te pushen en dan
+%met twee te vermenigvuldigen een aantal keren.
--- /dev/null
+\subsection{Compositie}
+De \textit{Composition} van $S_1$ en $S_2$ is gelijk aan de corresponderende
+blokken in \textit{Piet} waarbij het einde van het pad van het eerste blok met
+een wit blokje verbonden wordt met het blokje links bovenaan het tweede blok.
+Lukt dit niet omdat dan beide blokken overlappen of het einde van het pad van
+het eerste blok aan de boven of linkerkant ligt, dan kunnen het ook meerdere
+blokjes zijn eventueel door zwarte blokken gestuurd.\\
+In dit voorbeeld van \textit{Piet} geven de '*' aan dat je hier elk willekeurig blok voor in kan vullen. De verschillende grijstinten geven de verschillende blokken aan. Lichtoranje geeft het begin van het pad van dat blok aan en donkeroranje het eind. Als laatste staat een underscore voor een wit blokje.\\
+\textbf{While} $S_1;S_2$\\
+\textbf{Piet}
+\begin{tabular}{ccc}
+\color{orange}$\ast$ & \color{lgray}$\ast$ & \color{lgray}$\ast$\\
+\color{lgray}$\ast$ & \color{lgray}$\ast$ & \color{lgray}$\ast$\\
+\color{dorange}$\ast$ & \color{lgray}$\ast$ & \color{lgray}$\ast$\\
+\color{lgray}\_ & & \\
+\color{orange}$\ast$ & \color{gray}$\ast$ & \color{gray}$\ast$\\
+\color{gray}$\ast$ & \color{gray}$\ast$ & \color{gray}$\ast$\\
+\color{gray}$\ast$ & \color{gray}$\ast$ & \color{dorange}$\ast$\\
+\end{tabular}
\ No newline at end of file
--- /dev/null
+\subsection{If statement}
+De \textit{if} constructie in \textit{While} van de vorm if $b$ then $S_1$ else $S_2$
+kan worden gerepresenteerd in \textit{Piet} door de representatie van $b$ na een
+wit blokje te volgen door een pointer die op basis van het bovenste element op de
+stack de richting van de interpreter aanpast. Op het laaste blokje van dit commando
+volgen in 2 richtingen twee verschillende paden, waarbij 1 pad correspondeert met
+$S_1$ en het andere pad met $S_2$. Wel moeten beide paden uiteindelijk op hetzelfde
+punt uitkomen. \\
+In dit voorbeeld representeert het eerste blok een willekeurige boolean $b$, deze
+word na een wit blokje gevolgt door het pointer commando. Hierna splitsen de paden
+zich op: als de boolean 0 oplevert draait de richting van de interpreter 0 slagen met
+de klok mee en gaat dus rechtdoor, als de boolean 1 oplevert draait van de richting
+van de interpreter 1 slag met de klok mee en gaat dus naar rechts. In deze twee
+richtingen volgen vervolgens de representaties voor $S_1$ en $S_2$, die
+uiteindelijk doormiddel van witte blokjes weer op hetzelfde pad uitkomen.\\
+
+
+\textbf{While} if $b$ then $S_1$ else $S_2$ \\
+
+\textbf{Piet}
+\begin{tabular}{ccccccccccc}
+\color{orange}$\ast$ & \color{lgray}$\ast$ & \color{lgray}$\ast$\\
+\color{lgray}$\ast$ & \color{lgray}$\ast$ & \color{lgray}$\ast$\\
+\color{lgray}$\ast$ & \color{lgray}$\ast$ & \color{dorange}$\ast$ &
+\color{lgray}\_ & \color{red}\# & \color{dcyan}\# & \color{lgray}\_ &
+\color{orange}$\ast$ & \color{lgray}$\ast$ & \color{dorange}$\ast$\\
+ & & & & & \color{lgray}\_ & & & & \color{lgray}\_\\
+ & & & & & \color{orange}$\ast$ & & & & \color{lgray}\_\\
+ & & & & & \color{lgray}$\ast$ & & & & \color{lgray}\_\\
+ & & & & & \color{dorange}$\ast$ & \color{lgray}\_ & \color{lgray}\_ & \color{lgray}\_ & \color{lgray}\_ & \color{lgray}\_ \\
+
+
+\end{tabular}
\ No newline at end of file
--- /dev/null
+\subsection{Variabelen}
+Variabelen in \textit{While} worden op een totaal andere manier opgeslagen in
+\textit{Piet}. Waar variabelen in while een naam hebben, hebben variabelen in
+\textit{Piet} een nummer en kunnen ze door het aanroepen van een functie
+bovenaan gezet worden. De functie kan precies $1$ of precies $2$ variabelen
+boven aan de stack zetten. Hetzelfde kan voor de variabelen posities $a$ en $b$
+waarbij $b>a$. De piet' code om de variabele boven aan te krijgen is dan als
+volgt: $push b-1, push b-a, roll, push b, push b, push b*2, sub, roll$.\\
+Allereerst wordt $b-1$ op de stack gedrukt, dit bepaalt de diepte van de eerste
+$roll$ en zorgt ervoor dat $a$ tegen $b$ aan komt te liggen. $b-a$ wordt dat op
+de stack gepushed, dit is het verschil tussen $a$ en $b$ en bepaalt het aantal
+rolls er gedaan wordt op de stack, dit zijn er precies genoeg om $a$ bij $b$ te
+plaatsen. Vervolgens moeten ze nog naar boven en dat kan door $-b+1$ stappen te
+rollen met een diepte van $b$. de eerste $push b$ bepaalt de diepje en
+vervolgens wordt met $push b, push b*2-1, sub$ $b-1$ op de stack gepushed om te
+rollen en $a$ en $b$ bovenaan te plaatsen.
--- /dev/null
+\subsection{While statement}
+De \textit{while} constructie in \textit{While} van de vorm while $b$ do $S$
+kan worden gerepresenteerd in \textit{Piet} door de representatie van $b$ na een
+wit blokje te volgen door een pointer die op basis van het bovenste element op de
+stack de richting van de interpreter aanpast. Op het laaste blokje van dit commando
+volgen in 2 richtingen twee verschillende paden, waarbij 1 pad correspondeert met
+$S$ en het andere pad met het einde van de loop.
+In dit voorbeeld representeert het eerste blok een willekeurige boolean $b$, deze
+word na een wit blokje gevolgt door het pointer commando. Hierna splitsen de paden
+zich op: als de boolean 0 oplevert draait de richting van de interpreter 0 slagen met
+de klok mee en gaat dus rechtdoor, als de boolean 1 oplevert draait van de richting
+van de interpreter 1 slag met de klok mee en gaat dus naar rechts. Het pad na rechts
+word na een aantal witte blokjes gevolgt door de representatie van $S$. Hierna volgt
+weer een aantal witte blokjes waardoor het pad uiteindelijk uitkomt bij het begin van
+boolean $b$.\\
+
+\textbf{While} while $b$ do $S$ \\
+
+\textbf{Piet}
+\begin{tabular}{ccccccccccccc}
+\color{lgray}\_ & \color{lgray}\_ & \color{orange}$\ast$ & \color{lgray}$\ast$ & \color{lgray}$\ast$\\
+\color{lgray}\_ & & \color{lgray}$\ast$ & \color{lgray}$\ast$ & \color{lgray}$\ast$\\
+\color{lgray}\_ & & \color{lgray}$\ast$ & \color{lgray}$\ast$ & \color{dorange}$\ast$ &
+\color{lgray}\_ & \color{red}\# & \color{dcyan}\# & \color{lgray}\_\\
+\color{lgray}\_ & & & & & & & \color{lgray}\_\\
+\color{lgray}\_ & & & & & & & \color{lgray}\_\\
+\color{lgray}\_ & \color{lgray}\_ & \color{lgray}\_ & \color{dorange}$\ast$ & \color{lgray}$\ast$ & \color{orange}$\ast$ & \color{lgray}\_ & \color{lgray}\_ \\
+ & & & \color{lgray}$\ast$ & \color{lgray}$\ast$ & \color{lgray}$\ast$ \\
+ & & & \color{lgray}$\ast$ & \color{lgray}$\ast$ & \color{lgray}$\ast$ \\
+\end{tabular}
\ No newline at end of file
--- /dev/null
+\input{an_assignment.tex}
+
+\subsection{Skip}
+De \textit{Skip} is gelijk aan een enkel wit blokje. Als er naar een locatie
+gegaan moet worden voor de volgende operatie kunnen het ook meerdere blokjes
+zijn eventueel door zwarte blokken gestuurd.\\
+\textbf{While} $skip$\\
+\textbf{Piet} {\color{white}\#}\\
+
+\input{an_compositie.tex}
+
+\input{an_if_statement.tex}
+
+\input{an_while_statement.tex}
+
+\input{an_arit_expr.tex}
+
+\input{an_variabelen.tex}
--- /dev/null
+\subsection{\textit{Piet}}
+\textit{Piet} is een esoterische, stack geori\"enteerde en ge\"interpreteerde
+programmeertaal die is ge\"inspireerd door de Nederlandse kunstenaar Piet
+Mondriaan. Programma's geschreven vooor \textit{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
+``\textit{Tetris}'' print en iedere groep blokken een blok is uit het originele
+\textit{Tetris} spel.
+\begin{figure}[h]
+ \includegraphics[natheight=200px, natwidth=160px, height=50px, width=40px]{img1.png}
+\end{figure}
+
+\subsection{Beschrijving en vergelijking met \textit{While}}
+\textit{Piet} en \textit{While} zijn beide imperatieve talen maar zijn toch erg
+verschilled als het gaat om variabelenopslag en instructies. \textit{Piet}
+slaat zijn variabelen op in een stack waar \textit{While} dit niet doet. In een
+staat in \textit{While} kan iedere gedeclareerde variabele opgevraagd worden,
+omdat \textit{Piet} de variabelen in een stack opslaat kan er alleen maar de
+bovenste waarde opgevraagd worden.\\
+In \textit{Piet} is een stack een geordende rij van gehele getallen. De stack
+gedraagd zich volgens het LIFO(Last in First Out) principe werkt wat inhoudt
+dat er slechts \'e\'en element per keer kan worden opgevraagd en dat dat alleen
+het eerste element kan zijn.\\
+Instructies worden gegeven door het binnengaan van een nieuwe codel
+\footnote{Een codel is een blok $n\times n$ pixels waarbij $n\in\mathbb{N}$,
+een argument aan de compiler bepaalt de waarde van $n$. De standaard waarde is
+$1$} als de kleur van de nieuwe codel wit of hetzelfde is als de codel die
+verlaten word zal er niks gebeuren, is de codel zwart dan wordt er een nieuwe
+richting gekozen door de interpreter. Alle andere kleuren beschrijven een
+overgang die te beschrijven is in twee parameter; tint en intensiteit. Beide
+parameters zijn cyclisch, wat betekent dat de opvolger van de grootste
+waarde de kleinste waarde is. Iedere mogelijke overgang beschrijft een
+instructie voor de interpreter. Deze overgangen zijn beschreven in tabel
+\ref{tab:in1}.
+
+\begin{table}[h!]
+ \caption{Beide overgangcykels}
+ \label{tab:in1}
+ \centering
+ \begin{itemize}
+ \item{Tint:} rood$\rightarrow$ geel$\rightarrow$ cyaan$\rightarrow$ blauw$\rightarrow$ magenta
+ \item{Intensiteit:} licht$\rightarrow$ normaal$\rightarrow$ donker
+ \end{itemize}
+\end{table}
+
+De instructies die de overgangen uitdrukken staan beschreven in de onderstaande
+tabel \ref{tab:in2}.
+\begin{table}[h!]
+ \caption{Commando's}
+ \label{tab:in2}
+ \centering
+ \begin{tabular}{|l|l|l|l|}
+ \hline
+ Tint\textbackslash Intensiteit & 0 donkerder & 1 donkerder & 2 donkerder\\
+ \hline
+ 0 stappen & - & push & pop\\\hline
+ 1 stap & add & subtract & multiply\\\hline
+ 2 stappen & divide & mod & not\\\hline
+ 3 stappen & greater & pointer & switch\\\hline
+ 4 stappen & duplicate & roll & in(number)\\\hline
+ 5 stappen & in(char) & out(number) & out(char)\\\hline
+ \end{tabular}
+\end{table}
--- /dev/null
+\begin{tabular}{|p{2em}|l|l|}
+ \hline
+ Week & Dinsdag & Donderdag\\
+ \hline
+ 10 & Groep indeling en onderwerp &\\\hline
+ 11 & &\\\hline
+ 12 & & Opzet\\\hline
+ 13 & & Introductie af(verbeteren)\\\hline
+ 14 & & Kwartaalonderbreking\\\hline
+ 15 & Kwartaalonderbreking & Kwartaalonderbreking\\\hline
+ 16 & & Syntax en semantiek af\\\hline
+ 17 & & Analyse voor axiomas af\\\hline
+ 18 & MEIVAKANTIE & MEIVAKANTIE\\\hline
+ 19 & Voortgangsbespreking & Eerste versie\\\hline
+ 20 & & Analyse voor if af\\\hline
+ 21 & & Analyse voor while af\\\hline
+ 22 & & HEMELVAART\\\hline
+ 23 & & Demonstrerend piet programma/compiler/interpreter?\\\hline
+ 24 & & Definitieve versie\\\hline
+ 25 & &\\\hline
+ 26 & Eindbespreking & Eindbespreking\\\hline
+ 27 & Eindbespreking & Eindbespreking\\
+ \hline
+\end{tabular}
--- /dev/null
+\documentclass{scrartcl}
+
+\usepackage[dutch]{babel}
+\usepackage[hidelinks]{hyperref}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{graphicx}
+\usepackage{xcolor}
+\usepackage{proof}
+
+\graphicspath{{./img/}}
+
+\definecolor{lred}{HTML}{FFC0C0}
+\definecolor{lyellow}{HTML}{FFFFC0}
+\definecolor{lgreen}{HTML}{C0FFC0}
+\definecolor{lcyan}{HTML}{C0FFFF}
+\definecolor{lblue}{HTML}{C0C0FF}
+\definecolor{lmagenta}{HTML}{FFC0FF}
+\definecolor{red}{HTML}{FF0000}
+\definecolor{yellow}{HTML}{FFFF00}
+\definecolor{green}{HTML}{00FF00}
+\definecolor{cyan}{HTML}{00FFFF}
+\definecolor{blue}{HTML}{0000FF}
+\definecolor{magenta}{HTML}{FF00FF}
+\definecolor{dred}{HTML}{C00000}
+\definecolor{dyellow}{HTML}{C0C000}
+\definecolor{dgreen}{HTML}{00C000}
+\definecolor{dcyan}{HTML}{00C0C0}
+\definecolor{dblue}{HTML}{0000C0}
+\definecolor{dmagenta}{HTML}{C000C0}
+\definecolor{black}{HTML}{000000}
+\definecolor{white}{HTML}{FFFFFF}
+\definecolor{lgray}{HTML}{D3D3D3}
+\definecolor{dorange}{HTML}{FF4500}
+
+\author{Mart Lubbers\and Marjolein Zwerver}
+\title{Semantische analyse van \textit{Piet} middels een vergelijking met \textit{While}}
+\subtitle{Eerste opzet}
+\date{\today}
+
+\begin{document}
+\maketitle
+\tableofcontents
+\newpage
+
+\section{Introductie}
+\input{introduction.tex}
+
+\section{Syntax}
+\input{syntax.tex}
+
+\section{Semantiek}
+\input{semantics.tex}
+
+\section{Analyse}
+\input{analysis.tex}
+
+\section{Planning}
+\input{planning.tex}
+
+\end{document}
--- /dev/null
+\subsection{Structurele operationele semantiek}
+Bij natuurlijke semantiek(ns) ligt de nadruk op de relatie tussen de begin en
+de eind state. Het nadeel hiervan is dat programma’s die niet termineren geen
+bewijsbomen hebben. Hierdoor is het niet mogelijk om eigenschappen te bewijzen
+voor zulke programma’s. Bij structurele operationele semantiek(sos) ligt de
+nadruk juist op de individuele stappen van de executie en zijn er w\'el
+bewijsrijen voor programma’s die niet termineren.\\
+Om deze redenen hebben we gekozen voor sos.\\
+Een toestand in onze semantiek wordt 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=[e_0, e_1, \dots, e_n]$ waarbij $e_i\in\mathbb{Z}$\\
+Het transitie systeem zal twee verschillende transities kennen, namelijk:\\
+$\langle S, s_i, s_o, s\rangle\Rightarrow\langle S', s_i', s_o', s'\rangle$ en\\
+$\langle S, s_i, s_o, s\rangle\Rightarrow\langle s_i', s_o', s'\rangle$\\
+Waarbij de laatste transitie duidt op een terminerende transitie en de eerste
+op een niet terminerende transitie.\\
+
+\subsection{Semantiek beschrijving}
+Om het eerste element van een stack weg te kunnen gooien gebruiken we de volgende functie:\\
+$$\mathcal{D} : s \rightarrow s$$\\
+Deze neemt een stack en gooit het bovenste element weg.\\
+
+Om een stack uit te kunnen breiden met een element gebruiken we de volgende functie:\\
+$$\mathcal{E} : s, \mathbb{Z} \rightarrow s$$\\
+Deze functie neemt een stack en een integer en voegt de integer toe bovenop de stack.\\
+
+\footnotesize
+$\infer [{[}delete_{sos}{]}]
+ { \langle delete, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i,s_o,\mathcal{D}[s]\rangle}{}\\
+\infer [{[}extend_{sos}{]}]
+ { \langle extend \: z, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o,\mathcal{E}[s, z]\rangle}{}\\
+\infer [{[}pop_{sos} {]}]
+ { \langle delete, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'\rangle}
+ { \langle pop, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'\rangle}\\
+\infer [{[}add_{sos} {]}]
+ { \langle delete, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'\rangle \quad
+ \langle delete, s_i, s_o, s'\rangle \Rightarrow
+ \langle s_i, s_o, s''\rangle \quad
+ \langle extend\: x+y, s_i, s_o, s''\rangle \Rightarrow
+ \langle s_i, s_o, s'''\rangle}
+ { \langle add \: x,y, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'''\rangle}\\
+\infer [{[}subtract_{sos} {]}]
+ { \langle delete, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'\rangle \quad
+ \langle delete, s_i, s_o, s'\rangle \Rightarrow
+ \langle s_i, s_o, s''\rangle \quad
+ \langle extend\: x-y, s_i, s_o, s''\rangle \Rightarrow
+ \langle s_i, s_o, s'''\rangle}
+ { \langle subtract \: x,y, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'''\rangle}\\
+\infer [{[}multiply_{sos} {]}]
+ { \langle delete, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'\rangle \quad
+ \langle delete, s_i, s_o, s'\rangle \Rightarrow
+ \langle s_i, s_o, s''\rangle \quad
+ \langle extend\: x*y, s_i, s_o, s''\rangle \Rightarrow
+ \langle s_i, s_o, s'''\rangle}
+ { \langle multiply \: x,y, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'''\rangle}\\
+\infer [{[}divide_{sos} {]}]
+ { \langle delete, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'\rangle \quad
+ \langle delete, s_i, s_o, s'\rangle \Rightarrow
+ \langle s_i, s_o, s''\rangle \quad
+ \langle extend\: x/y, s_i, s_o, s''\rangle \Rightarrow
+ \langle s_i, s_o, s'''\rangle}
+ { \langle divide \: x,y, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'''\rangle}\\
+\infer [{[}mod_{sos} {]}]
+ { \langle delete, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'\rangle \quad
+ \langle delete, s_i, s_o, s'\rangle \Rightarrow
+ \langle s_i, s_o, s''\rangle \quad
+ \langle extend\: x \: mod \: y, s_i, s_o, s''\rangle \Rightarrow
+ \langle s_i, s_o, s'''\rangle}
+ { \langle mod \: x,y, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'''\rangle}\\
+\infer [{[}duplicate_{sos} {]}]
+ { \langle extend\: x, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'\rangle}
+ { \langle duplicate \: x, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'\rangle}\\
+\infer [{[}not^0_{sos} {]}]
+ { \langle delete, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'\rangle \quad
+ \langle extend\: 1, s_i, s_o, s'\rangle \Rightarrow
+ \langle s_i, s_o, s''\rangle}
+ { \langle not \: x, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s''\rangle}$ if $x = 0\\
+\infer [{[}not^*_{sos} {]}]
+ { \langle delete, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'\rangle \quad
+ \langle extend\: 0, s_i, s_o, s'\rangle \Rightarrow
+ \langle s_i, s_o, s''\rangle}
+ { \langle not \: x, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s''\rangle}$ if $x\neq 0\\
+\infer [{[}greater^<_{sos} {]}]
+ { \langle delete, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'\rangle \quad
+ \langle delete, s_i, s_o, s'\rangle \Rightarrow
+ \langle s_i, s_o, s''\rangle \quad
+ \langle extend\:,1, s_i, s_o, s''\rangle \Rightarrow
+ \langle s_i, s_o, s'''\rangle}
+ { \langle greater \: x,y, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'''\rangle}$ if $x>y\\
+\infer [{[}greater^>_{sos} {]}]
+ { \langle delete, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'\rangle \quad
+ \langle delete, s_i, s_o, s'\rangle \Rightarrow
+ \langle s_i, s_o, s''\rangle \quad
+ \langle extend\: 0, s_i, s_o, s''\rangle \Rightarrow
+ \langle s_i, s_o, s'''\rangle}
+ { \langle greater \: x,y, s_i, s_o, s\rangle \Rightarrow
+ \langle s_i, s_o, s'''\rangle}$ if $x<y
+$
+\normalsize
--- /dev/null
+\subsection{Originele Syntax}
+De ware syntax voor piet is makkelijk te beschrijven in een zeer grote tabel
+jie gedeeltelijk beschreven is in tabel \ref{tab:sy1}.
+\begin{table}[h]
+ \caption{Gedeeltelijke ware syntax van \textit{Piet}}
+ \label{tab:sy1}
+ \begin{tabular}{l|cccccc} %p{1em}|p{1em}p{1em}p{1em}p{1em}p{1em}p{1em}p{1em}}
+ \textbackslash & {\color{lred}\#} & {\color{lyellow}\#} &
+ {\color{lgreen}\#}& {\color{lcyan}\#} &
+ {\color{lblue}\#} & ...\\
+ \hline
+ {\color{lred}\#} & - & inc & dup & gre & ... & ...\\
+ {\color{lyellow}\#} & add & - & inc & dup & ... & ...\\
+ {\color{lgreen}\#} & div & add & - & inc & ... & ...\\
+ {\color{lcyan}\#} & gre & div & add & - & ... & ...\\
+ {\color{lblue}\#} & dup & gre & div & add & ... & ...\\
+ {\color{lmagenta}\#} & inc & dup & gre & div & ... & ...\\
+ {\color{red}\#} & pus & oun & rol & ... & ... & ...\\
+ {\color{yellow}\#} & sub & pus & oun & ... & ... & ...\\
+ {\color{green}\#} & mod & sub & pus & ... & ... & ...\\
+ {\color{cyan}\#} & poi & mod & sub & ... & ... & ...\\
+ {\color{blue}\#} & rol & poi & mod & ... & ... & ...\\
+ {\color{magenta}\#} & oun & rol & poi & ... & ... & ...\\
+ {\color{dred}\#} & pop & ouc & ouc & ... & ... & ...\\
+ {\color{dyellow}\#} & mul & pop & ouc & ... & ... & ...\\
+ {\color{dgreen}\#} & not & mul & pop & ... & ... & ...\\
+ {\color{dcyan}\#} & swi & not & mul & ... & ... & ...\\
+ {\color{dblue}\#} & inn & swi & not & ... & ... & ...\\
+ {\color{dmagenta}\#} & ouc & ouc & swi & ... & ... & ...\\
+ {\color{black}\#} & blo & blo & blo & ... & ... & ...\\
+ {\color{white}\#} & ski & ski & ski & ... & ... & ...\\
+ \end{tabular}
+\end{table}
+
+\subsection{Tussentaal}
+Om de notatie leesbaar en overzichtelijk te houden beschrijven we de syntax
+niet in de oorspronkelijke kleuren notatie maar gebruiken we een woordelijke
+notatie. Dan ziet de grammatica er als volgt 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\in\mathbb{N}, z\in\mathbb{Z}$ en $c\in\{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 bewijs-bomen/rijen krijgen vanwege het grote
+aantal composities, hier moeten we misschien nog iets anders op verzinnen.
repositories / sec1415.git / commitdiff