From 1e99906ba6bf2dc7453ba366e2e7c8f77ac4b916 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Tue, 6 May 2014 22:14:10 +0200 Subject: [PATCH] initial commit --- .gitignore | 5 +++ Makefile | 7 +++++ analysis.tex | 2 ++ img/img1.png | Bin 0 -> 4165 bytes img/img2.gif | Bin 0 -> 2538 bytes img/img2.png | Bin 0 -> 684 bytes introduction.tex | 63 ++++++++++++++++++++++++++++++++++++++ pietpy | 1 + planning.tex | 24 +++++++++++++++ project.tex | 58 +++++++++++++++++++++++++++++++++++ semantics.tex | 19 ++++++++++++ syntax.tex | 48 +++++++++++++++++++++++++++++ versie-0/Makefile | 7 +++++ versie-0/analysis.tex | 2 ++ versie-0/img/img1.png | Bin 0 -> 4165 bytes versie-0/img/img2.gif | Bin 0 -> 2538 bytes versie-0/img/img2.png | Bin 0 -> 684 bytes versie-0/introduction.tex | 31 +++++++++++++++++++ versie-0/planning.tex | 24 +++++++++++++++ versie-0/project.dvi | Bin 0 -> 14224 bytes versie-0/project.tex | 41 +++++++++++++++++++++++++ versie-0/project.txt | 26 ++++++++++++++++ versie-0/semantics.tex | 11 +++++++ versie-0/syntax.tex | 9 ++++++ 24 files changed, 378 insertions(+) create mode 100644 .gitignore create mode 100644 Makefile create mode 100644 analysis.tex create mode 100755 img/img1.png create mode 100755 img/img2.gif create mode 100644 img/img2.png create mode 100644 introduction.tex create mode 160000 pietpy create mode 100644 planning.tex create mode 100644 project.tex create mode 100644 semantics.tex create mode 100644 syntax.tex create mode 100644 versie-0/Makefile create mode 100644 versie-0/analysis.tex create mode 100755 versie-0/img/img1.png create mode 100755 versie-0/img/img2.gif create mode 100644 versie-0/img/img2.png create mode 100644 versie-0/introduction.tex create mode 100644 versie-0/planning.tex create mode 100644 versie-0/project.dvi create mode 100644 versie-0/project.tex create mode 100644 versie-0/project.txt create mode 100644 versie-0/semantics.tex create mode 100644 versie-0/syntax.tex diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..6ab5fb3 --- /dev/null +++ b/.gitignore @@ -0,0 +1,5 @@ +*.aux +*.log +*.out +*.pdf +*.toc diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..e9aaf43 --- /dev/null +++ b/Makefile @@ -0,0 +1,7 @@ +all: + pdflatex project.tex + pdflatex project.tex + pdflatex project.tex + +clean: + rm -vf *.toc *.dvi *.pdf *.aux *.log *.out *.txt diff --git a/analysis.tex b/analysis.tex new file mode 100644 index 0000000..58d649d --- /dev/null +++ b/analysis.tex @@ -0,0 +1,2 @@ +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. diff --git a/img/img1.png b/img/img1.png new file mode 100755 index 0000000000000000000000000000000000000000..8dca1754507f10d1cf7226c49760429e3811827d GIT binary patch literal 4165 zcmeHJ2U8Qu7G4DDRq2S*oAfG3P3XM@2qH=mLJ>n#nqUy=3euZF5a~q$4MadgM@kTs z8j3U#6}VCiO38~}=lzE_^LA$U?D2-1Oy?ye6D)}5H^Fh zL%{6TIkkxMyAZQPRF)aimV;Kn7LtNuPZyICq+>Nr6fBwMu<2kkFreb=FHWRPO-0@3 zu#sj=rk|o&5qy#wTbh_WaIhFz>Nn9w{4{+0a#DM(b_d-wLW84a%rRE7Q9&_QLC&&$ zjP2|0U0jjXjiDC_0Ial4*93!)geky&w5H~HAso$XKoRzyffnE_3UTsh5=bmxAo-Um zQ1>WsA?X*)Xi@AyHzE~M4s;DEQ0P1{J5WpoTn9bemw~kma23Dv={-Q9_wyqufOD20 z2Ssr@5IF6bs1Lj^g4z*>WCH+~2kc&E-RfXU2FRN@dKrV~%>ajIWoQJnj6mKdF-{Ut zMFQ7;Vc{@vFCVZQZaZpzKVQ$fCPii{zflt_qHYl5Oe+&eZ3sTk&~GGE?MlZ4#emycIRY65ftSPY3C zJ(iYh;zeDgM)@B<5#6NnzQRy^lbGVw$fEla6tB-X?gaei#-QXOc6xesWo62=8{+IX z;23p`=)8(^Ji7ifTJw;&_wn_TNQ|OOj1krT$IhW$^RhD|8FcsDXFsJG9X2zN4*A~; zb(^?j;Zp3&Hm3qp^$YIrD3%E&K{6zJM8`bV}@ zZU?tCj`~c;$=MEuLs!*%5RvXq2rGpC8tP1tt7Pq6h(!GGbABmTxevPh$~YVE_{;!i z*-rZwW~~60Uv9KT9TIIZbX0o%w5Qz!XA&vgli|Xtv|Rad`+^TsC}_ez6}Y-aU+OGg8QkX|&P$!1xl1tyJT^XZVES-L(*f zf;7(J!goP0c(v}UmaM(2@n)Gx(}woR<34lKD0N?#m+kF>G+dCT%k&s*5UORY>E(Uy zP)pgGwC6F>5K46_#sEjBN)-wba67AK3^#{cP8nAUoDorGo1s&qqr7L+DK3;*Y4$?w z72D5lZg)k61h}!Z@WiRK({ikliO_B}kyA-fMRDxI6DAE$VPmJp499NR3a?976)GF^ z3TM8Zx#rhMqn;%#aK1lo1-;U>qO`)dBDn2Lk9OA$e7bM9Bw;(?Ys$0Ax~jZN?U|>j zXJ1-iJ6Bl(V^c}H1gR^**gmsKs64HFvp{_~mea(ntnNwndtPrYZ=%n$&mpha=CaRP z=Du?r8(cT~ocoz_HA4<@gs@HKBOpCun@ z50}D7-R4LipwBkV7R%<7l7m%MmsihMGuZFg55m%_uGmG@8`>+`EmzTf$f>cfMq7Wi zSH*O@4}BiNDuuZle*MmTj7qX;#D z5znpJqY{YJCN+_K$r7w@HGM>R{w4Idb?-1q6dyezWp-|OF7Dn>0P zC}w8y#bUF-)&g5DS$@&{qIuu&(D0MtiF}npErm(NwZgT+$-;$Z*GplSq%oD47EhDL zl}qJLo0zs6ahKGc%HZ~wT$&8)&~>5{t#z#xY!z6`Ov{?02}IZP@0hoks%D<&t5ej3 zdW=6N$_?Spg=p@n@7m04&y0E%_25X0hACm1xrYA|e{}GRAa)H0jrjunqfMQtp52^v zIRt!!b!19u8FPA2vfBr3SNPrt!G*vE$L=JiB$?eEl+D$aE#&K+>u+B%4cQBHS&SIl zLl-s`c5YM>o^7gb`fMi5J|0qjELr5F6#TBMANtW|bySDpakjkQLT$7a)G7w?a!pvy zLoVI1Zt{6^S!gxUZHr6$hj!58W$k56wRy#Pr>jG1xaR)mL8~rg(bc#G=pA9wHBtm= z6jY!@DG-!NF?uo1Cl2-_ZVSFi)zKh${%D-u(7RuZ)#K1hyIXg6wWChZyZ_t6Izi%E z9zGrK!yIQF{dwXYjoT-;l&)w-@wkLI$9SF8fJ8X&s6wtv=;$moctQV{evbZpAwt1Q z{h5rZij;P>tgq&b+AHN(I=!-9PDA5xG~DF6*%@_Nse08L*IzFjZtNs1p_dqzBf0YA z`dtFTOYoh$aTT0ZvZtgqa&*lTEiYvKqsJ;$$$4LN`*f&iDt&k-ea69qv6Mwb#<%n~m2i^~Ii22%bRc1dDVil!0a>FD)lIB7sV zr>5xq@WxQn0O6t9qpioJjZ>Yc7Betq@n()P{P0ihwZ7_&nt|a2`elxj=i?oyYc*Sv zF;f2HRy7-rx%JWQVi6X8F;_YU?smMS@cYVOPrn)$^>ub~!^H|N=d|$B?N>aSPn#nt zxt^WCmCJEwN@6x_l`jD~@FssY>qS*fH}=|y*O=G(r+JwoXXc#h+)ug8H<+epUN9{< zyx7?LVL*_}9hM-p#$uq@(l?qdZJrfx@xvE&U{7JYuwO9M&9S+cZj<{rMmPB)+kPm2 z8z(ro5s$Rrz9!gH*jtQyje8!L95fMi>XWM1_j3;XUFt0T12_68$0(0zgqbmu*bn3U zV_GoVw2AXyjhOq+y*@^7g~~9gGTA?P)Vm}cpdY@nPNZ8Po@LUQxphCXc9G`&xm)}Q zemP%A!FGXRpti7)dJhem{RERU2mox)9bU~he9*6+U0L~M`TM`xp> zqGf;1x)PpXBG)|d3%)GKtyioei(>|)l(ma(7x9<3TSB%Q39F|aTO13XX)Nc^uI}n?=uJcC62^6$k7uX0X7BjoLW_4sXN`!|aj_%E>3eA`(35HT zX@l`h@n4HBXsfF)=>#3EA67s|u8oKlaUDN79<1l$l#AXU|2l~u%^NMr-OkN?u*oFr0v^V;763$u0)UDI;3tVJ*8#XG55N~!05tLd z;6i3x?J)#^5?GtV49E`TLBiq48ytBwlm>F2A8aE@U&=@^AE? z6#rlT&%pm614d)k8~~hvnds}m!e+jqM{jh>Ga3*^A&%U&ha@#-g@I&KBjSs&vHDu` z$PU8y%o6!o<5Nm7&ZQQSWP|7Epn^FhRS z(wEi0sm8qQALD=X>5KZzZ3+hS?j6*myi2ZFnRXf~t-Lk=w;DUncilmVFyvF~u1-6C zAt~{JHIvG@e{;5lihe(zE*X5&VLC*}Au4fB+KItJ&jkE#U|AyR%^j5#)tmK;q_gk` zHM4<_S}17+P#~V-Fled%2UaXpl%eDTMydQ(^EXY;?6!IP^R|p+`w4C%6W`G~ygYA- z(tshG4Xvn6cE9ewtds%=a`_rd{HAFZen`ljT}g-bNT7$ziU5i&yL;;jLtMX#U7~F8 zBOdY1zoMup$c!o|?vcI%(z|L{Kt{=E+9en0*DF8~q(04AY~ zt1s?Ml8{IEGwVyb(quJlsV&8&J(O>OT%tlLm4{`GG@I7_44l=~0kZ({D*bbct&>-gXeQ$6@)rLy28!Aa#cwqxzZ7 zOHhW_Y4rNLC$~VBLx^Zt05|>U#jQ4v(2Kc${A{dhAF~lWnCE61FroD6Qg)SoU7$BV zk~Lm(owT;Ptr_-=5iGB-w;mNReJAf&+Je_+*qZ@O)I8oi#pQ; zd?H#E1~2iEs-0CQOogz1N=f&~SH2?Kp!F`j#5vH{WjZl`lBj}AcFU5anN%B59E|h(S>FR_0`5f1kg|FR_bLw8jlm#C)|xIU8-a>*?q@mQx${8`=A9%uYxI$NrEZOU9BOrbe>=m0;g||fb!!bN1wNbn2b|j)4xnWKd!dC zH3aLKj3j@+w~VFh)1oG_OkWw#D%nX#&C$t)Pxe21WRRzqBW=c9To^vgP9;N13D^SmB!jlL~SSbxqf+R5e~BeiZszI_=x+3(_G zKKjP5V`o(~Os0K)`nsvb+}y!C=KQ5tVf^;^6UT&|4dV|xd{XShW~-Ro#YGlIT9O3p zYe54BVTtya(n0RYOeka_Q6y{%3{j9zJMCnpVAhvvP>I>|1b+s;J(YS=qD&!MHc314 z!b`={laPnx!>E|)J*LkHN{EG2fgO7qY$t(HtI; z`0J$jt4=E{tc@u?`?wS6zQ+DV8%$A1grAPq`L*F5Gs905;#I8?^#i~uK?)_|l-8ji z2vlbZB{SiGzgATc3#rjh$#dnvk9#1Q(f#_x1q8U?9jZrZgh=&@mX3Bbt8ayp-O#Od z1bmTuA)z7vVlqr0beLHNoQlDjn?sDU@T)IuJth0{ii}JSEBtjD z8iS-@sb$9HaB26(0ehvv3YZw)*Wbk%qR@2P+!_zJZ*`?2-7q?CGsth1n)A3^Yd7nx zvtuLAYa=&nW)>HIDSV1!?8ya!uD$y8UjJF8!p}7kDjE;vq899&ABwz8*_e> zAr-RXInSZC5?M7-3cB(<&XBe0J|n`-6<={~_tT~IhK$!MJ`m<`xk;oYITwFU+isYH zkZa6ze!UX(6WViBr1(+eoT?^cUU%MVs+qYrRJ6CJMMUvU3t&Nn{1`8HDg)W(?P z?e4-X$m8<~$l)yTh%5%u9$@TtGTRQQAkNdpF(l*O+nfCPO$Gw21^4_1gdf3*y=J^7np3nN+J-H9~#AIroY&$8sY(n;_s_p9Aec#Pciu#u4 zH|<=}wgdOxA1x|yURR~3a6tC@d)b|@EN6T?@Zox?!MRQDiuW}asrp?Eyc1zKLAchn z@KZ(pmwOYHzw^JVYnx`rzV`2vN2fO=D3~AJ=^plY8Q;X}zt!g3)bj1yzSAN5 zLym%V`m05OTU6ZpWOlY%Moj&=dGURgf}5+4v@d*eVxsbPopN76-Na~KiyKYNQx#1L zHyNtBAsT7~u5ki2 OFnGH9xvXn#nqUy=3euZF5a~q$4MadgM@kTs z8j3U#6}VCiO38~}=lzE_^LA$U?D2-1Oy?ye6D)}5H^Fh zL%{6TIkkxMyAZQPRF)aimV;Kn7LtNuPZyICq+>Nr6fBwMu<2kkFreb=FHWRPO-0@3 zu#sj=rk|o&5qy#wTbh_WaIhFz>Nn9w{4{+0a#DM(b_d-wLW84a%rRE7Q9&_QLC&&$ zjP2|0U0jjXjiDC_0Ial4*93!)geky&w5H~HAso$XKoRzyffnE_3UTsh5=bmxAo-Um zQ1>WsA?X*)Xi@AyHzE~M4s;DEQ0P1{J5WpoTn9bemw~kma23Dv={-Q9_wyqufOD20 z2Ssr@5IF6bs1Lj^g4z*>WCH+~2kc&E-RfXU2FRN@dKrV~%>ajIWoQJnj6mKdF-{Ut zMFQ7;Vc{@vFCVZQZaZpzKVQ$fCPii{zflt_qHYl5Oe+&eZ3sTk&~GGE?MlZ4#emycIRY65ftSPY3C zJ(iYh;zeDgM)@B<5#6NnzQRy^lbGVw$fEla6tB-X?gaei#-QXOc6xesWo62=8{+IX z;23p`=)8(^Ji7ifTJw;&_wn_TNQ|OOj1krT$IhW$^RhD|8FcsDXFsJG9X2zN4*A~; zb(^?j;Zp3&Hm3qp^$YIrD3%E&K{6zJM8`bV}@ zZU?tCj`~c;$=MEuLs!*%5RvXq2rGpC8tP1tt7Pq6h(!GGbABmTxevPh$~YVE_{;!i z*-rZwW~~60Uv9KT9TIIZbX0o%w5Qz!XA&vgli|Xtv|Rad`+^TsC}_ez6}Y-aU+OGg8QkX|&P$!1xl1tyJT^XZVES-L(*f zf;7(J!goP0c(v}UmaM(2@n)Gx(}woR<34lKD0N?#m+kF>G+dCT%k&s*5UORY>E(Uy zP)pgGwC6F>5K46_#sEjBN)-wba67AK3^#{cP8nAUoDorGo1s&qqr7L+DK3;*Y4$?w z72D5lZg)k61h}!Z@WiRK({ikliO_B}kyA-fMRDxI6DAE$VPmJp499NR3a?976)GF^ z3TM8Zx#rhMqn;%#aK1lo1-;U>qO`)dBDn2Lk9OA$e7bM9Bw;(?Ys$0Ax~jZN?U|>j zXJ1-iJ6Bl(V^c}H1gR^**gmsKs64HFvp{_~mea(ntnNwndtPrYZ=%n$&mpha=CaRP z=Du?r8(cT~ocoz_HA4<@gs@HKBOpCun@ z50}D7-R4LipwBkV7R%<7l7m%MmsihMGuZFg55m%_uGmG@8`>+`EmzTf$f>cfMq7Wi zSH*O@4}BiNDuuZle*MmTj7qX;#D z5znpJqY{YJCN+_K$r7w@HGM>R{w4Idb?-1q6dyezWp-|OF7Dn>0P zC}w8y#bUF-)&g5DS$@&{qIuu&(D0MtiF}npErm(NwZgT+$-;$Z*GplSq%oD47EhDL zl}qJLo0zs6ahKGc%HZ~wT$&8)&~>5{t#z#xY!z6`Ov{?02}IZP@0hoks%D<&t5ej3 zdW=6N$_?Spg=p@n@7m04&y0E%_25X0hACm1xrYA|e{}GRAa)H0jrjunqfMQtp52^v zIRt!!b!19u8FPA2vfBr3SNPrt!G*vE$L=JiB$?eEl+D$aE#&K+>u+B%4cQBHS&SIl zLl-s`c5YM>o^7gb`fMi5J|0qjELr5F6#TBMANtW|bySDpakjkQLT$7a)G7w?a!pvy zLoVI1Zt{6^S!gxUZHr6$hj!58W$k56wRy#Pr>jG1xaR)mL8~rg(bc#G=pA9wHBtm= z6jY!@DG-!NF?uo1Cl2-_ZVSFi)zKh${%D-u(7RuZ)#K1hyIXg6wWChZyZ_t6Izi%E z9zGrK!yIQF{dwXYjoT-;l&)w-@wkLI$9SF8fJ8X&s6wtv=;$moctQV{evbZpAwt1Q z{h5rZij;P>tgq&b+AHN(I=!-9PDA5xG~DF6*%@_Nse08L*IzFjZtNs1p_dqzBf0YA z`dtFTOYoh$aTT0ZvZtgqa&*lTEiYvKqsJ;$$$4LN`*f&iDt&k-ea69qv6Mwb#<%n~m2i^~Ii22%bRc1dDVil!0a>FD)lIB7sV zr>5xq@WxQn0O6t9qpioJjZ>Yc7Betq@n()P{P0ihwZ7_&nt|a2`elxj=i?oyYc*Sv zF;f2HRy7-rx%JWQVi6X8F;_YU?smMS@cYVOPrn)$^>ub~!^H|N=d|$B?N>aSPn#nt zxt^WCmCJEwN@6x_l`jD~@FssY>qS*fH}=|y*O=G(r+JwoXXc#h+)ug8H<+epUN9{< zyx7?LVL*_}9hM-p#$uq@(l?qdZJrfx@xvE&U{7JYuwO9M&9S+cZj<{rMmPB)+kPm2 z8z(ro5s$Rrz9!gH*jtQyje8!L95fMi>XWM1_j3;XUFt0T12_68$0(0zgqbmu*bn3U zV_GoVw2AXyjhOq+y*@^7g~~9gGTA?P)Vm}cpdY@nPNZ8Po@LUQxphCXc9G`&xm)}Q zemP%A!FGXRpti7)dJhem{RERU2mox)9bU~he9*6+U0L~M`TM`xp> zqGf;1x)PpXBG)|d3%)GKtyioei(>|)l(ma(7x9<3TSB%Q39F|aTO13XX)Nc^uI}n?=uJcC62^6$k7uX0X7BjoLW_4sXN`!|aj_%E>3eA`(35HT zX@l`h@n4HBXsfF)=>#3EA67s|u8oKlaUDN79<1l$l#AXU|2l~u%^NMr-OkN?u*oFr0v^V;763$u0)UDI;3tVJ*8#XG55N~!05tLd z;6i3x?J)#^5?GtV49E`TLBiq48ytBwlm>F2A8aE@U&=@^AE? z6#rlT&%pm614d)k8~~hvnds}m!e+jqM{jh>Ga3*^A&%U&ha@#-g@I&KBjSs&vHDu` z$PU8y%o6!o<5Nm7&ZQQSWP|7Epn^FhRS z(wEi0sm8qQALD=X>5KZzZ3+hS?j6*myi2ZFnRXf~t-Lk=w;DUncilmVFyvF~u1-6C zAt~{JHIvG@e{;5lihe(zE*X5&VLC*}Au4fB+KItJ&jkE#U|AyR%^j5#)tmK;q_gk` zHM4<_S}17+P#~V-Fled%2UaXpl%eDTMydQ(^EXY;?6!IP^R|p+`w4C%6W`G~ygYA- z(tshG4Xvn6cE9ewtds%=a`_rd{HAFZen`ljT}g-bNT7$ziU5i&yL;;jLtMX#U7~F8 zBOdY1zoMup$c!o|?vcI%(z|L{Kt{=E+9en0*DF8~q(04AY~ zt1s?Ml8{IEGwVyb(quJlsV&8&J(O>OT%tlLm4{`GG@I7_44l=~0kZ({D*bbct&>-gXeQ$6@)rLy28!Aa#cwqxzZ7 zOHhW_Y4rNLC$~VBLx^Zt05|>U#jQ4v(2Kc${A{dhAF~lWnCE61FroD6Qg)SoU7$BV zk~Lm(owT;Ptr_-=5iGB-w;mNReJAf&+Je_+*qZ@O)I8oi#pQ; zd?H#E1~2iEs-0CQOogz1N=f&~SH2?Kp!F`j#5vH{WjZl`lBj}AcFU5anN%B59E|h(S>FR_0`5f1kg|FR_bLw8jlm#C)|xIU8-a>*?q@mQx${8`=A9%uYxI$NrEZOU9BOrbe>=m0;g||fb!!bN1wNbn2b|j)4xnWKd!dC zH3aLKj3j@+w~VFh)1oG_OkWw#D%nX#&C$t)Pxe21WRRzqBW=c9To^vgP9;N13D^SmB!jlL~SSbxqf+R5e~BeiZszI_=x+3(_G zKKjP5V`o(~Os0K)`nsvb+}y!C=KQ5tVf^;^6UT&|4dV|xd{XShW~-Ro#YGlIT9O3p zYe54BVTtya(n0RYOeka_Q6y{%3{j9zJMCnpVAhvvP>I>|1b+s;J(YS=qD&!MHc314 z!b`={laPnx!>E|)J*LkHN{EG2fgO7qY$t(HtI; z`0J$jt4=E{tc@u?`?wS6zQ+DV8%$A1grAPq`L*F5Gs905;#I8?^#i~uK?)_|l-8ji z2vlbZB{SiGzgATc3#rjh$#dnvk9#1Q(f#_x1q8U?9jZrZgh=&@mX3Bbt8ayp-O#Od z1bmTuA)z7vVlqr0beLHNoQlDjn?sDU@T)IuJth0{ii}JSEBtjD z8iS-@sb$9HaB26(0ehvv3YZw)*Wbk%qR@2P+!_zJZ*`?2-7q?CGsth1n)A3^Yd7nx zvtuLAYa=&nW)>HIDSV1!?8ya!uD$y8UjJF8!p}7kDjE;vq899&ABwz8*_e> zAr-RXInSZC5?M7-3cB(<&XBe0J|n`-6<={~_tT~IhK$!MJ`m<`xk;oYITwFU+isYH zkZa6ze!UX(6WViBr1(+eoT?^cUU%MVs+qYrRJ6CJMMUvU3t&Nn{1`8HDg)W(?P z?e4-X$m8<~$l)yTh%5%u9$@TtGTRQQAkNdpF(l*O+nfCPO$Gw21^4_1gdf3*y=J^7np3nN+J-H9~#AIroY&$8sY(n;_s_p9Aec#Pciu#u4 zH|<=}wgdOxA1x|yURR~3a6tC@d)b|@EN6T?@Zox?!MRQDiuW}asrp?Eyc1zKLAchn z@KZ(pmwOYHzw^JVYnx`rzV`2vN2fO=D3~AJ=^plY8Q;X}zt!g3)bj1yzSAN5 zLym%V`m05OTU6ZpWOlY%Moj&=dGURgf}5+4v@d*eVxsbPopN76-Na~KiyKYNQx#1L zHyNtBAsT7~u5ki2 OFnGH9xvXHH5`b1q~jZH1R34cEe=y-Rz z$^>0e8#fBH=AfuY+>zlpQ&kpn$Av&t2(zY^u7n;zpQe^AsuD~DnA#W|5HWMCsbvEj z9#qtz*4VUm?bOn^fT5Z=!q&8RtZZ)gtn6rw>&sTPwKsd(R&=z*^;B~FcmJAA8mDYq zJ=Mx(W18-6jANN*ZnFCB_2n)}jW`d3a!(v7Lq?z(&KOC^)L zKZ&%uch^N)dy>Yf+daEKdAPM2B1Z z1W}Q(^jf^8E-oGKD~{hHGJW>IgughpF#2oNM_kKG~(vJ7?1v2c6IVA$?}$Ods1o8wIG;>Wf9QnC}$N^t^TC3;HR$XQ$L7yt#h2Q|7OP` zxY~k1Ow;^BUe8m#w$^Z_Ed8aOhXh*<=71oZWG7}!3C%xIz&nKEm|W-X+uRNqQMK z{C@lN>DNDW^$CuXLLmo@tPjLgukYzi*sbAuyk%p;?;j0bjtNqD(U>vED^ttS+^$c*ZBJm$JELh_2&KH!W#WI zHT@O7Pm;K7pA+llh>{3uN<1tKu+)R++xIwfDq(cLKzu!&BQnF9Azk-iD*(^hp~&xM|o?kdmLRC+ls7kc(UV(|`Vn z-<1W7rmYXWQ4}Nh40KrZOpHKAI4Jm)I_#9l}azTV~za@AI$%M_rI)zq;aO} zHCWJ|FVK8!*iU+!ecVte0PTEiX(0xso%=#eHf=nzC=QtfM+Z0_8IFJ1Q(`&wJ*WJi zw4A~z?ECx?Ca?S_p?lzi9iC@23Iq}V?PzN%^#!bK$LnOPy>KD8m#ux>ZM(jhwe5JH zY~yR^Q-iXV89VgFtZXL>$#%YSA+ac1`liiC+7Q>qTkg%+5%AYPU!3*g8@%qOe7X*Q zwY)AoM)K;bA-Onq@>-Iy6jRF@CLKQkIYx2v2bM`sLSn-7xFnl%3Fg*$oMDb%LMRc7}{ zW7@c?gjFFH!w_8%Br7N~Q`GDzTsBmTiz>~Vc1`?MP#N8HL{T%YiQ9tAyow=5K-wA9 zm=#UPNT_6_HaumsHYsvY6$L?VHWpmzL5;%~6Cjnn5tSi1k^$MGoOT}G8>ci6bI8~Q zQxl?|aUQ;ZM8qcnd7t3dbX5rGjJjw#2AYG=2IVNSg*AY?G#zBbR5SppGlh^J!ZIcW zksvl>r5=W*Zh5Y-als4nWH)TxdAZXB=%ho9Q@1!|~QR*@n0(;ye&0ERi(GtguRY zWpT?dDbXmlhs9+6!4fqK+ORM)gb>3h!X##u&gi=P)~pt%;Zk#I{L-t>gg;LCDT5MY zRP*`$$`B=QZtn_Dv&ZA{u0r|C-}&0y0ZELbX;2KJMs4#nd)qx8RFv)r6T=bR-HvZo zt!!U`ZyK9h#8{aAyv=b`8E!cG__^17XHHkB#d*h1I5Ndu0l*GdD6Q(!NX>DGc0?V$ zub~)I?G%4sGP{n!NPH4MWEf!>$h;0Fm^L8s6tQ-#{>&TVhxfJs6m`OeuY?eAx1!BQ^$;x8f^mLQ< z$RrDv8DtiG8cHC;gUHv{5-|9h6YBTwwz^Xk-Y#{C2 zb`A*uD8Pa18)&(#|`7i^W74S}EYFYNLpv8qPa^1G!8fMjQu?ehPL&@DzrX z(ohH$l~_Ur-Uz%q`jmo7K*8ZiQ`db?Wzf2iqUfmbhz%l22Ic0*^Piq}-}22HzT{Yd zAWeTR6uGNjLfcEjTUx+-yNz)}G0s+pIN+m0j%I_(?S zl6Gx54F(fq{NOXLEvJ)l0WZ*I%`|Xdo&U=>yG2kJf)M5K&HWMB4f7$Zfi(t{7|5ca za)Aa*C;rMr8x~rTu9M%L{_4_(WjjkNQEk}knRJ@jR&&x}X1!_Wq6gNP-j&U%y=S3t z#tXUealwi%pUN`*=`j8HbY)XWBkNg8_RmxP2h zNbe|S$d)cZj*2PQ%QzAQc}>)rXwNK(09jMdPb@1c_RHrEDl*3m6%%!{v@^UxEO9Ix zk>Lz)B&C=529q=B2h`z+Ltzl^E+7z6bfe?9lLlavJ=j8yLApmDV3wZ8lVz!KViICZ zjnZzFxE<%omx*`bu1R5*qY#-O(goxbIIBXFX#+F0K^6JDNi`Li2U8=|OJZQb5N=nV zdLpzmesG}wZyb(LXkJtOU+-P`oh8ZS=)v4x*BRfs!*Sxh_fm^dfAG-wfBybIeCLGy7Qsbr%ec*X1uEH^qQycKdl;CMod7#AJ*T16XVr0JBn zvFuw~d24E4EmCn+kW@zN6OYW6M+gRuWiMV`KCi7p54FiyU zT)E7ar@~#)6M|FE;%uirI=9S}vTyqB4(>^g2R8n6e9^`n;45j=pSgAX0sPFqfHKdv2>^#UJBRQddv=8t(jZ(fC@X!)9h z7m<$2NDc6c^x~w369Z~^oiK6?Qlqs7{^2u|8nqQ$oYX+61yaN2&~PDe^Igg8<`~b+ zcTEu&k#X(%gG|*p0v*p$;u0Iekyv4bS)LIiS+(pM!$9940_Py&B5JQh6tx4!NuVHh z{eh|v+m*C{#fehn&&XCNIQNPD$k(-W-K}9{P?@@0Lk0NY9EFMyTS&nu+>%^Yp*$0K zse-iJ4%iw>AZ8VEDUFI2r0M_~Uf1xVjVK22vzW+Fb$&i8*A)vv9H|49GsdFnc1lzB zg>0Te2aF(Jr0fpqs6w-LqT6)C3A_DkOS7^V?gw(chV$W$Y-i^h14&t~H|^Lnmi4YS z=Dp<2^_p2GdQJWTiOGoJyt08lAU2sJJHNReZMhLE>*GCmR6;xi z@nPc2(xzBK+Oe{U0+KmwI6V?I(<(EA5llvdCS|~7L$QZkOhFO2FI2G}VhAL1E&V%^ zD2&l63oqy~un+AJPM43VYwPf;Rw87C0GEhE(HE9ll-oSLOIA;++1r9lc)NW`R90oclk_1yI1hi?2diZ*FxO zC!O`>R-2ujovY25l_d&@*LLWMkFaq|HWMJ*)HDXenF=Kk)ejM#orkH0NXTLUc{&w1 zc7Cd&dSEJ9Cox93&4(_OvKX!Xnn%M0(STNL2b?kKan|1$~YSY(oX^X5DMv(i`a*cn4IvL3X>S< zK*CBCbig*$c#ICtZ_<$&m@~rs{1mB$*p0jV>o`GVDr&m!kw0N_vOkXY#p+p!nIQiF z&UQ)>j}v6#oF4fj8HYtHj9|3_FKUh?Bwpy1$Vlc2J*Mk^@xINaB%l?Rsr$uyN|D%7 zh{!a#Qprw8t(u}WnWR@zQ(me42@!lR)o=`DAJ32zd|1_k+DGEY={LCbOewR zF$`obH?VvxA_Z|{E(Wm@!Hdd8X;x4!ZDw=Ko*Ukyg0Ur%8mi?7TL_6^7PSfZv3SlPbCB!+-jagA` zwc!jd6=gij1dqD*H-JFAr47SSI7dUwzR+yUKl1K1OpDX`)2%xl8fO|ZuB)Sd^jAzG zGdRD=V7()-^sD=U6jn}4j?ddWGW{2?%sbmxB#C$iw(5|W!t%egVbAV&NC9t@c?Jlm z5keL!cK8kt{8-5vp#`kozV7u`ErUw&X7koQqyC1?z?J$Ner~fBOqC0JMAOp+FCZ%| zxb3idW2NYTKKz5Be8Oq6gS1)=}X|P@nw zC?%<`r_&k+sI!_L`86+YM`!S2sn!yAv z4hZ-Ne`Z_;PFU=vfJl_i98)#F1PeX%NG7S%f$PH!IZ_{JbRE z&mA}0YA8(daT8b4h@1H9+QB)DBBD` z;cLUGeU;XOQvjFf;s9>VvoxDwmNjbO!sO#AbU}s)2qu6i-=#Hsi*yNNkqz@1B4$DY zbD4AQ=-$CC;$$ikBf zsojqB_Z|navHR%IK-?w{Cw_Nsk(n){TarY}f&w|1vr&(+D5#31-*%Pqu@}4*?FN4x z6vBr1(v@Z7iG_Xo*;~3f7mW^Mj+dXjrMyQ8s|qn}R<*3hj0|2+)y1#OUl0?bBMm}e zK;90E;)`st0LhsrOv_&p$nCLz>FK^yrm$LyvtM@mi|rz~x?%d&yz z9sB_ee$;-IMRD|Fj@>u?{c*0|Ua`6X>z-pF+ft63c#Rpqc_Jp!eo z>U5)xdJ`pvZJ5RdcP}Yl%oeJLUy+g{@e%|-XJBKFLtk$!?^~;2zDkgs(^jgVlNjPh z^y81#9H#^|q9a*rbqNOPCkkAM`=eh!P9Z)6fUfJ=)Uz=S>$%qK>bi!qwZ1XO{)etO z&Xqp{oOZJq&zLCH<-B8@@}gpr)&k}>4ppcv%ZJ|E^ literal 0 HcmV?d00001 diff --git a/versie-0/project.tex b/versie-0/project.tex new file mode 100644 index 0000000..291b1bb --- /dev/null +++ b/versie-0/project.tex @@ -0,0 +1,41 @@ +\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} diff --git a/versie-0/project.txt b/versie-0/project.txt new file mode 100644 index 0000000..6e8ec43 --- /dev/null +++ b/versie-0/project.txt @@ -0,0 +1,26 @@ +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" +> Aan: "marjolein zwerver" +> 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 diff --git a/versie-0/semantics.tex b/versie-0/semantics.tex new file mode 100644 index 0000000..3715278 --- /dev/null +++ b/versie-0/semantics.tex @@ -0,0 +1,11 @@ +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. diff --git a/versie-0/syntax.tex b/versie-0/syntax.tex new file mode 100644 index 0000000..3d3b59d --- /dev/null +++ b/versie-0/syntax.tex @@ -0,0 +1,9 @@ +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. -- 2.20.1