summaryrefslogtreecommitdiff
path: root/paper/interp.tex
diff options
context:
space:
mode:
authorCamil Staps2016-06-03 13:31:46 +0200
committerCamil Staps2016-06-03 13:31:46 +0200
commit14ec0ad883bc51fb16c72472e060ff0443e29533 (patch)
treeac2174232e9546987b988f34a5a2ef6140998093 /paper/interp.tex
parentRewrite eval for AExpr (diff)
Finishing first version paper
Diffstat (limited to 'paper/interp.tex')
-rw-r--r--paper/interp.tex6
1 files changed, 3 insertions, 3 deletions
diff --git a/paper/interp.tex b/paper/interp.tex
index 0f73b2d..5b8db03 100644
--- a/paper/interp.tex
+++ b/paper/interp.tex
@@ -15,9 +15,9 @@ $$
\end{prooftree}
$$
-This specifies nothing else than the intuition: the composition
-$\whcomp{S_1}{S_2}$ executed in state $s$ will yield a state $s''$ which we get
-by executing $S_1$ and $S_2$ in $s$, consecutively.
+This specifies nothing else than the intuition: if the execution of statement
+$S_1$ in state $s$ yields state $s'$, and $S_2$ in $s'$ yields $s''$, then
+$\whcomp{S_1}{S_2}$ in $s$ yields $s''$.
The translation of this rule in a functional program looks as follows: