summaryrefslogtreecommitdiff
path: root/paper/interp.tex
diff options
context:
space:
mode:
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: