Merge branch 'master' of https://github.com/dopefishh/sec2014
[sec1415.git] / an_faculteit.tex
1 \subsection{Faculteit}
2 Als we de analyse op een compleet programma toepassen komt er een \textit{Piet}
3 programma uit dat behoorlijk fors is maar netjes zijn werk doet. Het programma
4 dat we gaan vertalen berekent de faculteit van $x$ en stopt dat uiteindelijk in
5 $y$.
6 \begin{lstlisting}[title=Faculteit in \textit{While}]
7 x:=5;
8 y:=1;
9 while $\neg$(x=1)
10 do (
11 y:=y*x;
12 x:=x-1
13 )
14 \end{lstlisting}
15
16 In \textit{Piet'} ziet dit er als volgt uit...
17 \begin{lstlisting}[title=Faculteit in \textit{Piet'}]
18 push 10 // x:=5
19 push 1 // y:=1
20
21 MARKERING A:
22 // Un(2)
23 // $\neg$(x=1) $\equiv$ $\neg$(x-1)>0)
24
25
26 // x-1
27 // Un(2)
28 push 2 //
29 push 1 //
30 roll //
31 dup //
32 push 3 //
33 push 1 //
34 roll //
35 push 1 //
36 sub //
37 not // $\neg(x-1)$
38
39 push 1 // zet $0$ op de stack
40 push 1
41 sub
42
43 gre // $\neg(x-1)>0$ oftewel x=1
44
45 pointer // als x=0 dan draait de DP niet en gaat het programma naar pad B
46 // als x$\neq$ dan draait de DP en gaat het programma naar pad A
47
48 PAD A:
49 skip // een oneindig aantal witte blokken, y is nu x!
50 // evt een outchar om $y$ naar standardout te printen
51
52 PAD B:
53 // y:=y*x
54 // Bin(1, 2)
55 dup // Un(1)
56 push 3 // Un(2+1)
57 push 2 //
58 roll //
59 dup //
60 push 4 //
61 push 1 //
62 roll //
63 mul // x*y
64 push 2 // Ass(1)
65 push 1
66 roll
67 pop
68
69 // x:=x-1
70 push 2 // Un(2)
71 push 1
72 roll
73 dup
74 push 3
75 push 1
76 roll
77
78
79 push 1 //
80 sub // x-1
81 push 3 // Ass(2)
82 push 2
83 roll
84 pop
85 push 2
86 push 1
87 roll
88 // nu gaat het programma weer via een wit pad naar markering A
89 \end{lstlisting}
90
91 Wat in \textit{Piet} er uit ziet als in Figuur~\ref{fig:img3}
92 \begin{figure}[H]
93 \caption{Faculteit vanuit \textit{While} naar \textit{Piet}}
94 \label{fig:img3}
95 \centering
96 \fbox{\includegraphics[natheight=320px, natwidth=256px, height=320px,
97 width=256px]{img3.png}}
98 \end{figure}
99
100 \begin{landscape}
101 De afleidingsrij voor 1! ziet er als volgt uit:\\
102 $
103 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1;push \: 2;push \: 1;push \: 1, [\:], [\:], [\:]\rangle \Rightarrow\\
104 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1;push \: 2;push \: 1, [\:], [\:], [1]\rangle \Rightarrow\\
105 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1;push \: 2, [\:], [\:], [1,1]\rangle \Rightarrow\\
106 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1, [\:], [\:], [2,1,1]\rangle \Rightarrow\\
107 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll, [\:], [\:], [1,2,1,1]\rangle \Rightarrow\\
108 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup, [\:], [\:], [1,1]\rangle \Rightarrow\\
109 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
110 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1, [\:], [\:], [3,1,1,1]\rangle \Rightarrow\\
111 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll, [\:], [\:], [1,3,1,1,1]\rangle \Rightarrow\\
112 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
113 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;, [\:], [\:], [1,1,1,1]\rangle \Rightarrow\\
114 \langle pointer; not;greater;subtract;push\:1;push \: 1;not, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
115 \langle pointer; not;greater;subtract;push\:1;push \: 1, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
116 \langle pointer; not;greater;subtract;push\:1, [\:], [\:], [1,1,1,1]\rangle \Rightarrow\\
117 \langle pointer; not;greater;subtract, [\:], [\:], [1,1,1,1,1]\rangle \Rightarrow\\
118 \langle pointer; not;greater, [\:], [\:], [0,1,1,1]\rangle \Rightarrow\\
119 \langle pointer; not, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
120 \langle pointer [\:], [\:], [0,1,1]\rangle \Rightarrow\\
121 \langle [\:], [\:], [1,1]\rangle\\
122 \\
123 $
124 Eerst worden x en y op de stack gestopt zodat de stack [y,x] = [1,1].
125 Deze stack is gelijk aan de stack in de termineerende configuratie: 1 = 1! dus y = x!.
126 Als bewijs dat de wiskundige operaties op de stack goed zijn uitgevoerd staat in
127 de appendix onder het kopje voorbeelden een stukje code. In het programma
128 eenfaculteit worden alle wiskundige operaties die bij de commando's horen
129 achter elkaar uitgevoerd op de stack, waarbij het resultaat [1,1] is.\\
130 Bij de voorbeelden staan ook nog de programma's tweefaculteit en
131 vijffaculteit die respectievelijk 2! en 5! uitrekenen.
132 \end{landscape}