--- /dev/null
+*.aux
+*.log
+*.out
+*.pdf
+*.toc
--- /dev/null
+all:
+ pdflatex project.tex
+ pdflatex project.tex
+ pdflatex project.tex
+
+clean:
+ rm -vf *.toc *.dvi *.pdf *.aux *.log *.out *.txt
--- /dev/null
+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.
--- /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
+Subproject commit b8ddba9ee206821431d58dd62a1b1fa9ca8d3dd8
--- /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}
+
+\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}
+
+\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}
--- /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.
--- /dev/null
+all:
+ latex project.tex
+ latex project.tex
+ dvipdfmx project.dvi
+
+clean:
+ rm -f *.toc *.dvi *.pdf *.aux *.log
--- /dev/null
+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.
--- /dev/null
+\subsection{\textit{Piet}}
+\textit{Piet} is een esoterische, stack geori\"enteerde en ge\"interpreteerde programmeertaal die is ge\"ispireerd 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 "\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 gelijkenis met \textit{While}}
+Het belangrijkste verschil tussen \textit{Piet} en \textit{While} is het programmeer paradigma dat word gebruikt, \textit{Piet} is een stack geori\"enteerde taal waar \textit{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\"enteerd betekent dat variabelen opslag in een stack gebeurt. Een stack is een geordende rij van, in het geval van \textit{Piet}, gehele getallen.
+Instructies worden gegeven aan de interpreter door een bepaalde overgang in kleur naar de volgende codel\footnote{Een codel is blok $n\times n$ pixels waarbij $n\in\mathbb{N}^+$}, 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$.
+\begin{itemize}
+ \item{Tint:} rood$\rightarrow$ geel$\rightarrow$ cyaan$\rightarrow$ blauw$\rightarrow$ magenta
+ \item{Intensiteit:} licht$\rightarrow$ normaal$\rightarrow$ donker
+\end{itemize}
+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.\\
+\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}
--- /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[dvipdfmx]{graphicx}
+\usepackage[dvipdfmx, hidelinks]{hyperref}
+\usepackage{amsmath}
+\usepackage{amssymb}
+
+\graphicspath{ {./img/} }
+
+\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
+
+%1 Mart
+\section{Introductie}
+\input{introduction.tex}
+
+%2 Marjolein
+\section{Syntax}
+\input{syntax.tex}
+
+%3 Marjolein
+\section{Semantiek}
+\input{semantics.tex}
+
+%4 Marjolein
+\section{Analyse}
+\input{analysis.tex}
+
+%5 Mart
+\section{Planning}
+\input{planning.tex}
+
+\end{document}
--- /dev/null
+Dat is goed, dan doe ik de syntax, semantiek en analyse. Ik zal het voor donderdag na jou sturen, dan kan je het nog aanvullen als dat nodig is.
+Voor de semantiek: heb je nu al voorkeur voor ns, sos of iets anders?
+En voor de analyse: wil je daar hetzelfde programma gebruiken als bij de inleiding of iets anders? en is er een bepaalde eigenschap die we willen bewijzen, of willen we gewoon bewijzen dat het programma doet wat het zou moeten doen?
+
+Groetjes, Marjolein.
+
+----- Oorspronkelijk bericht -----
+> Van: "Mart Lubbers" <mart@martlubbers.net>
+> Aan: "marjolein zwerver" <marjolein.zwerver@student.ru.nl>
+> Verzonden: Dinsdag 18 maart 2014 21:35:05
+> Onderwerp: Semantiek en correctheid piet
+> Wat moet er in de opzet:
+>
+> - titel
+> - inleiding(hier moet een voorbeeldprogramma in)
+> - syntax(evt grammatica)
+> - beschrijving semantiek(welke)
+> - analyse
+> - planning
+>
+> welke wil jij doen?
+>
+> Mij lijkt de planning en de inleiding met het voorbeeldprogramma wel
+> leuk om te doen.
+>
+> Mart
--- /dev/null
+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 heeft wel bewijsrijen voor programma’s 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\in\mathbb{Z}$\\
+Het transitie systeem zal twee verschillende transities kennen, namelijk:\\
+$s\rightarrow \langle S, s_i, s_o, s\rangle$ en $s\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.\\
+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 \"uberhaupt nodig is in de semantiekbeschrijving.
--- /dev/null
+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 commando’s 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\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
