summaryrefslogtreecommitdiff
path: root/paper/interp.tex
diff options
context:
space:
mode:
authorCamil Staps2016-06-07 15:51:04 +0200
committerCamil Staps2016-06-07 15:51:04 +0200
commita82dc42e7c07fa47d2dab0cbe26a31e080ae9952 (patch)
treef2f7ec0b7851bfc4ed1887f66c254904e7b27487 /paper/interp.tex
parentFinishing first version paper (diff)
Processed feedback
Diffstat (limited to 'paper/interp.tex')
-rw-r--r--paper/interp.tex15
1 files changed, 9 insertions, 6 deletions
diff --git a/paper/interp.tex b/paper/interp.tex
index 5b8db03..f5101e5 100644
--- a/paper/interp.tex
+++ b/paper/interp.tex
@@ -15,9 +15,10 @@ $$
\end{prooftree}
$$
-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''$.
+This derivation rule consists of two premises, above the line, and one
+conclusion, beneath the line. It 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:
@@ -50,7 +51,8 @@ $$
\end{cases}
$$
-This gives the assignment rule:
+This gives the assignment axiom\footnote{An axiom, in this context, is nothing
+else than a derivation rule with zero premises.}:
$$
\begin{prooftree}
@@ -106,8 +108,9 @@ $$
\end{prooftree}
$$
-A similar rule exists for $S_2$ in the case that $\mathcal B\llbracket
-b\rrbracket s$ does not hold.
+This derivation rule has one premise, but can only be applied when the
+condition $\mathcal B\llbracket b\rrbracket s$ holds. A similar rule exists
+for $S_2$ in the case that the condition does not hold.
The problem with these rules is that they can only be applied when some
condition is met. In this case, the condition is still relatively easy. In