repositories
/
sec1415.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
semantics aangetikt maar niet gedaan, analysis mee begonnen, skip klaar en compositie ook
[sec1415.git]
/
semantics.tex
diff --git
a/semantics.tex
b/semantics.tex
index
00eca8a
..
f7fb7fa
100644
(file)
--- a/
semantics.tex
+++ b/
semantics.tex
@@
-1,21
+1,23
@@
\subsection{Structurele operationele semantiek}
Bij natuurlijke semantiek(ns) ligt de nadruk op de relatie tussen de begin en
\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
+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
bewijsbomen hebben. Hierdoor is het niet mogelijk om eigenschappen te bewijzen
-voor zulke programma
’
s. Bij structurele operationele semantiek(sos) ligt de
+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
nadruk juist op de individuele stappen van de executie en zijn er w\'el
-bewijsrijen voor programma
’
s die niet termineren.\\
+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}$
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}$
- en waarbij het bovenste element op de stack gerepresenteerd word door het
+ en waarbij het bovenste element op de stack gerepresenteerd word
t
door het
eerste element in de lijst.\\
eerste element in de lijst.\\
-Het transitie
systeem zal twee verschillende transities kennen, namelijk:\\
+Het transitiesysteem 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$\\
$\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
+Waarbij de laatste transitie duidt op een transitie waar een volgende transitie
+aanwezig is en genomen kan worden. De tweede duidt op een transitie waarbij er
+geen volgede beschikbaar is en het programma dus termineerd.
op een niet terminerende transitie.\\
\subsection{Semantiekbeschrijving}
op een niet terminerende transitie.\\
\subsection{Semantiekbeschrijving}
@@
-102,27
+104,25
@@
Deze functie haalt de bovenste twee elementen van de stack en stopt 1 bovenop
de stack als het tweede bovenste element een hogere waarde heeft als dat van het
bovenste element. Anders word 1 bovenop de stack gestopt.\\
de stack als het tweede bovenste element een hogere waarde heeft als dat van het
bovenste element. Anders word 1 bovenop de stack gestopt.\\
-out number (output stack) functie (outnum, r. 7
9
):\\
+out number (output stack) functie (outnum, r. 7
0
):\\
Deze functie past de output stack aan als er een integer naartoe geschreven word:\\
$$\mathcal{OUTN_{SO}} : Stack \rightarrow Stack$$\\
Deze functie haalt het bovenste element van de stack en stopt dit element bovenop de output stack.\\
Deze functie past de output stack aan als er een integer naartoe geschreven word:\\
$$\mathcal{OUTN_{SO}} : Stack \rightarrow Stack$$\\
Deze functie haalt het bovenste element van de stack en stopt dit element bovenop de output stack.\\
-in number (stack) functie (innum, r.
84
):\\
+in number (stack) functie (innum, r.
75
):\\
Deze functie past de stack aan als er een integer naartoe geschreven word:\\
$$\mathcal{INN_S} : Stack \rightarrow Stack$$\\
Deze functie haalt het bovenste element van de input stack en stopt dit element bovenop de output stack.\\
Deze functie past de stack aan als er een integer naartoe geschreven word:\\
$$\mathcal{INN_S} : Stack \rightarrow Stack$$\\
Deze functie haalt het bovenste element van de input stack en stopt dit element bovenop de output stack.\\
-(outchar, inchar)\\
-
Met behulp van deze gedefinieerde functies kunnen we nu de volgende semantiekregels opstellen:\\
\begin{alignat*}{2}
{[comp^1_{sos}]}\qquad &
Met behulp van deze gedefinieerde functies kunnen we nu de volgende semantiekregels opstellen:\\
\begin{alignat*}{2}
{[comp^1_{sos}]}\qquad &
-\frac{\langle S_
1, s\rangle \Rightarrow \langle S'_1
, s'\rangle}
-{\langle S_1 ;S_2, s\rangle \Rightarrow \langle S
'_1;S
_2, s'\rangle}\\
+\frac{\langle S_
2, s\rangle \Rightarrow \langle S'_2
, s'\rangle}
+{\langle S_1 ;S_2, s\rangle \Rightarrow \langle S
_1;S'
_2, s'\rangle}\\
{[comp^2_{sos}]}\qquad &
{[comp^2_{sos}]}\qquad &
-\frac{\langle S_
1
, s\rangle \Rightarrow \langle s'\rangle}
-{\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_
2
, s'\rangle}\\
+\frac{\langle S_
2
, s\rangle \Rightarrow \langle s'\rangle}
+{\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_
1
, s'\rangle}\\
{[pop_{sos}]}\qquad &
\langle pop, s_i, s_o, s\rangle \Rightarrow
\langle s_i, s_o,\mathcal{D}(s)\rangle\\
{[pop_{sos}]}\qquad &
\langle pop, s_i, s_o, s\rangle \Rightarrow
\langle s_i, s_o,\mathcal{D}(s)\rangle\\
@@
-168,11
+168,5
@@
Met behulp van deze gedefinieerde functies kunnen we nu de volgende semantiekreg
{[outnum_{sos}]} \qquad &
\langle outnum, s_i, s_o, s\rangle \Rightarrow
\langle s_i, \mathcal{OUTN_{SO}}(s_o),\mathcal{D}(s)\rangle\\
{[outnum_{sos}]} \qquad &
\langle outnum, s_i, s_o, s\rangle \Rightarrow
\langle s_i, \mathcal{OUTN_{SO}}(s_o),\mathcal{D}(s)\rangle\\
-{[inchar_{sos}]} \qquad &
-\langle inchar, s_i, s_o, s\rangle \Rightarrow
-\langle s_i, s_o, s\rangle\\
-{[outchar_{sos}]} \qquad &
-\langle outchar, s_i, s_o, s\rangle \Rightarrow
-\langle s_i, s_o, s\rangle\\
\end{alignat*}
\end{alignat*}