diff options
Diffstat (limited to 'paper/interp.tex')
| -rw-r--r-- | paper/interp.tex | 6 |
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: |