From: Mart Lubbers Date: Thu, 8 May 2014 15:54:18 +0000 (+0200) Subject: cleaned up code X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=0039f1b4471d13af48e769f1d76084f2cbe03c20;p=sec1415.git cleaned up code --- diff --git a/project.tex b/project.tex index 20c24e4..a1fed4e 100644 --- a/project.tex +++ b/project.tex @@ -6,6 +6,7 @@ \usepackage{amssymb} \usepackage{graphicx} \usepackage{xcolor} +\usepackage{proof} \graphicspath{{./img/}} diff --git a/semantics.tex b/semantics.tex index e977049..fb4c747 100644 --- a/semantics.tex +++ b/semantics.tex @@ -16,8 +16,6 @@ $\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$$\\ @@ -27,28 +25,99 @@ Om een stack uit te kunnen breiden met een element gebruiken we de volgende func $$\mathcal{E} : s, \mathbb{Z} \rightarrow s$$\\ Deze functie neemt een stack en een integer en voegt de integer toe bovenop de stack.\\ -$[delete_{sos} ] \; \Rightarrow $\\ - -$[extend_{sos} ] \; \Rightarrow $\\ - -$[pop_{sos} ] \; \frac{ \Rightarrow }{ \Rightarrow }$\\ - -$[add_{sos} ] \; \frac{ \Rightarrow \; \Rightarrow \; \Rightarrow }{ \Rightarrow }$\\ - -$[subtract_{sos} ] \; \frac{ \Rightarrow \; \Rightarrow \; \Rightarrow }{ \Rightarrow }$\\ - -$[multiply_{sos} ] \; \frac{ \Rightarrow \; \Rightarrow \; \Rightarrow }{ \Rightarrow }$\\ - -$[divide_{sos} ] \; \frac{ \Rightarrow \; \Rightarrow \; \Rightarrow }{ \Rightarrow }$\\ - -$[mod_{sos} ] \; \frac{ \Rightarrow \; \Rightarrow \; \Rightarrow }{ \Rightarrow }$\\ - -$[duplicate_{sos} ] \; \frac{ \Rightarrow }{ \Rightarrow }$\\ - -$[not^0_{sos} ] \; \frac{ \Rightarrow \; \Rightarrow }{ \Rightarrow }$ if x = 0\\ - -$[not^*_{sos} ] \; \frac{ \Rightarrow \; \Rightarrow }{ \Rightarrow }$ if x $\neq$ 0\\ - -$[greater^<_{sos} ] \; \frac{ \Rightarrow \; \Rightarrow \; \Rightarrow }{ \Rightarrow }$ if x$<$y\\ - -$[greater^>_{sos} ] \; \frac{ \Rightarrow \; \Rightarrow \; \Rightarrow }{ \Rightarrow }$ if x$>$y\\ \ No newline at end of file +\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