diff options
| author | Camil Staps | 2016-06-03 13:31:46 +0200 |
|---|---|---|
| committer | Camil Staps | 2016-06-03 13:31:46 +0200 |
| commit | 14ec0ad883bc51fb16c72472e060ff0443e29533 (patch) | |
| tree | ac2174232e9546987b988f34a5a2ef6140998093 /paper/interp.tex | |
| parent | Rewrite eval for AExpr (diff) | |
Finishing first version paper
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: |