mirror of
https://github.com/janishutz/eth-summaries.git
synced 2026-07-28 03:39:08 +02:00
[FMFP] Restructure summary
This commit is contained in:
@@ -0,0 +1,38 @@
|
||||
\subsection{IMP Language}
|
||||
\subsubsection{The syntax}
|
||||
The allowed characters:
|
||||
\begin{code}{haskell}
|
||||
Letter = 'A' | . . . | 'Z' | 'a' | . . . | 'z'
|
||||
Digit = '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9'
|
||||
\end{code}
|
||||
|
||||
And the allowed tokens:
|
||||
\begin{code}{haskell}
|
||||
Ident = Letter { Letter | Digit }*
|
||||
Numeral = Digit | Numeral Digit
|
||||
Var = Ident
|
||||
\end{code}
|
||||
|
||||
Arithmetic and Boolean statements could be defined in Haskell as follows
|
||||
\begin{code}{haskell}
|
||||
data Aexp = Bin Op Aexp Aexp | Var String | Num Integer
|
||||
data Op = Add | Sub | Mul
|
||||
data Bexp = Or Bexp Bexp | And Bexp Bexp | Not Bexp | Rel Rop Aexp Aexp
|
||||
data Rop = Eq | Neq | Le | Leq | Ge | Geq
|
||||
\end{code}
|
||||
with the abbreviations for \texttt{Eq} (=), \texttt{Neq} (\#), \texttt{Le} ($<$), \texttt{Leq} ($\leq$), \texttt{Ge} ($>$) and \texttt{Geq} ($\geq$)
|
||||
|
||||
Statements could be defined in Haskell as follows
|
||||
\mint{haskell}+data Stm = Skip | Assign String Aexp | Seq Stm Stm | If Bexp Stm Stm | While Bexp Stm+
|
||||
|
||||
We use the following naming conventions for meta-variables:
|
||||
\begin{tables}{ll}{Variable & Type}
|
||||
$n$ & for numerals (\texttt{Numeral}) \\
|
||||
$x, y, z$ & for variables (\texttt{Var}) \\
|
||||
$e, e', e_1, e_2$ & for arithmetic expressions (\texttt{Aexp}) \\
|
||||
$b, b_1, b_2$ & for boolean expressions (\texttt{Bexp}) \\
|
||||
$s, s', s_1, s_2$ & for Statements (\texttt{Stm}) \\
|
||||
\end{tables}
|
||||
Meta-variables stand for arbitrary program variables, whereas program variables are concrete variables in a program.
|
||||
|
||||
To denote \bi{syntactic equality} of two variables or statements, we use $\equiv$
|
||||
@@ -0,0 +1,59 @@
|
||||
\newpage
|
||||
\subsubsection{The semantics}
|
||||
\paragraph{Numerals}
|
||||
The semantic function $\cN : \texttt{Numeral} \rightarrow \texttt{Val}$ maps a numeral $n$ to an integer value $\cN\llbracket n \rrbracket$,
|
||||
with $x \in \{ 0, \ldots, 9 \}$:
|
||||
\begin{align*}
|
||||
\cN\llbracket x \rrbracket = x & & \cN\llbracket n x \rrbracket = \cN\llbracket n \rrbracket \cdot 10 + x
|
||||
\end{align*}
|
||||
|
||||
|
||||
\paragraph{States}
|
||||
A state assigns a value to each program variable. It is a total function and is typically denoted by the meta-variable $\sigma$
|
||||
\[
|
||||
\sigma : \texttt{Var} \rightarrow \texttt{Val}
|
||||
\]
|
||||
To update states, we use the notation $\sigma[y \mapsto v]$, which is given by
|
||||
\[
|
||||
(\sigma[y \mapsto v])(x) = \begin{cases}
|
||||
v & \text{if } x \equiv y \\
|
||||
\sigma(x) & \text{if } x \not\equiv y
|
||||
\end{cases}
|
||||
\]
|
||||
Two states $\sigma_1, \sigma_2 $ are equal if they are equal as functions: $\sigma_1 = \sigma_2 \Leftrightarrow \forall x. (\sigma_1(x) = \sigma_2(x))$
|
||||
|
||||
|
||||
\paragraph{Arithmetic Expressions}
|
||||
$\cA : \texttt{Aexp} \rightarrow \texttt{State} \rightarrow \texttt{Val}$ maps an arithmetic expression $e$ and a state $\sigma$ to a value $\cA\llbracket e \rrbracket \sigma$,
|
||||
given by:
|
||||
\begin{align*}
|
||||
\cA\llbracket x \rrbracket \sigma & = \sigma(x) \\
|
||||
\cA\llbracket n \rrbracket \sigma & = \cN\llbracket n \rrbracket \\
|
||||
\cA\llbracket e_1 \; \texttt{op} \; e_2 \rrbracket \sigma & = \cA\llbracket e_1 \rrbracket \sigma \; \overline{\texttt{op}} \; \cA\llbracket e_2 \rrbracket \sigma
|
||||
\end{align*}
|
||||
For $\texttt{op} \in \texttt{Op}$, $\overline{\texttt{op}}$ is the corresponding operation $\texttt{Val} \times \texttt{Val} \rightarrow \texttt{Val}$
|
||||
|
||||
|
||||
\paragraph{Boolean Expressions}
|
||||
$\cB : \texttt{Bexp} \rightarrow \texttt{State} \rightarrow \texttt{Bool}$ maps boolean expression $b$ and a state $\sigma$ to a truth value $\cB\llbracket b \rrbracket \sigma$,
|
||||
given by:
|
||||
\[
|
||||
\cB\llbracket e_1 \; \texttt{op} \; e_2 \rrbracket \sigma = \begin{cases}
|
||||
\texttt{tt} & \text{if } \cA\llbracket e_1 \rrbracket \sigma \; \overline{\texttt{op}} \; \cA\llbracket e_2 \rrbracket \sigma \\
|
||||
\texttt{ff} & \text{otherwise}
|
||||
\end{cases}
|
||||
\]
|
||||
Thus, for the \texttt{op} \texttt{or}, we would have (analogous for \texttt{and})
|
||||
\[
|
||||
\cB\llbracket b_1 \; \texttt{or} \; b_2 \rrbracket \sigma = \begin{cases}
|
||||
\texttt{tt} & \text{if } \cA\llbracket b_1 \rrbracket \sigma = \texttt{tt} \; \texttt{or} \; \cA\llbracket b_2 \rrbracket \sigma = \texttt{tt} \\
|
||||
\texttt{ff} & \text{otherwise}
|
||||
\end{cases}
|
||||
\]
|
||||
\texttt{not} is defined as follows:
|
||||
\[
|
||||
\cB\llbracket \texttt{not}\; b \rrbracket \sigma = \begin{cases}
|
||||
\texttt{tt} & \text{if } \cA\llbracket b \rrbracket \sigma = \texttt{ff} \\
|
||||
\texttt{ff} & \text{otherwise}
|
||||
\end{cases}
|
||||
\]
|
||||
@@ -0,0 +1,80 @@
|
||||
\subsubsection{Properties of expression semantics}
|
||||
Since we have recursive definitions for the semantics and syntax, we can use structural induction.
|
||||
|
||||
\begin{recall}[]{Structural Induction}
|
||||
For the data structure \texttt{Nat}, given by
|
||||
\mint{haskell}+data Nat = Zero | Succ Nat+
|
||||
the structural induction derivation rule is given by
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\Gamma \vdash P(\texttt{Zero})}
|
||||
\hypo{\Gamma, P(m) \vdash P(\texttt{Succ}\; m)}
|
||||
\infer2[$m$ not free in $\Gamma$]{\Gamma \vdash \forall n \in \texttt{Nat}. P(n)}
|
||||
\end{prooftree}
|
||||
\]
|
||||
Where we now write $P(m)$ instead of $P[n \mapsto m]$ and the second premise needs to be proven for all $m$
|
||||
\end{recall}
|
||||
|
||||
|
||||
\paragraph{Inductive Definitions}
|
||||
If we are to introduce a new arithmetic expression $-e$, we could do this in two ways.
|
||||
For one, we could define $\cA\llbracket -e \rrbracket \sigma = 0 - \cA\llbracket e \rrbracket \sigma$. This \textit{is} an inductive definition because $e$ is a subterm of $-e$.
|
||||
|
||||
If on the other hand we define $\cA\llbracket -e \rrbracket \sigma = \cA\llbracket 0 - e \rrbracket \sigma$,
|
||||
it is \textit{not} an inductive definition because $0 - e$ is \textit{not} a subterm of $-e$
|
||||
|
||||
|
||||
\paragraph{Free Variables}
|
||||
For Arithmetic Expressions
|
||||
\begin{align*}
|
||||
FV(e_1 \; \texttt{op} \; e_2) & = FV(e_1) \cup FV(e_2) \\
|
||||
FV(n) & = \varnothing \\
|
||||
FV(x) & = \{ x \}
|
||||
\end{align*}
|
||||
|
||||
For Boolean Expressions
|
||||
\begin{align*}
|
||||
FV(b_1 \; \texttt{op} \; b_2) & = FV(b_1) \cup FV(b_2) \\
|
||||
FV(\texttt{not}\; b) & = FV(b) \\
|
||||
FV(b_1 \; \texttt{or} \; b_2) & = FV(b_1) \cup FV(b_2) \\
|
||||
FV(b_1 \; \texttt{and} \; b_2) & = FV(b_1) \cup FV(b_2)
|
||||
\end{align*}
|
||||
|
||||
And finally for Statements:
|
||||
\begin{align*}
|
||||
FV(\texttt{skip}) & = \varnothing \\
|
||||
FV(x := e) & = \{ x \} \cup FV(s_2) \\
|
||||
FV(s_1; s_2) & = FV(s_1) \cup FV(s_2) \\
|
||||
FV(\texttt{if}\; b\; \texttt{then} \; s_1 \; \texttt{else} \; s_2 \; \texttt{end}) & = FV(b) \cup FV(s_1) \cup FV(s_2) \\
|
||||
FV(\texttt{while}\; b\; \texttt{do} \; s \; \texttt{end}) & = FV(b) \cup FV(s)
|
||||
\end{align*}
|
||||
|
||||
|
||||
\paragraph{Substitution}
|
||||
{\scriptsize We have already seen this kind of expression in the states, with this explanation it should make a lot more sense intuitively.}
|
||||
|
||||
A substitution $f[x \mapsto e]$ replaces each free occurrence of variable $x$ in $f$ by $e$, where $f$ is any expression.
|
||||
|
||||
Detailed rules for arithmetic expressions (for the last, if variable $y$ is $x$, it is replaced, otherwise not):
|
||||
\begin{align*}
|
||||
(e_1 \; \texttt{op} \; e_2)[x \mapsto e] & \equiv (e_1[x \mapsto e] \; \texttt{op} \; e_2[x \mapsto e]) \\
|
||||
n[x \mapsto e] & \equiv n \\
|
||||
y[x \mapsto e] & \equiv \begin{cases}
|
||||
e & \text{if } x \equiv y \\
|
||||
y & \text{otherwise}
|
||||
\end{cases}
|
||||
\end{align*}
|
||||
|
||||
The same for boolean expressions:
|
||||
\begin{align*}
|
||||
(e_1 \; \texttt{op} \; e_2)[x \mapsto e] & \equiv (e_1[x \mapsto e] \; \texttt{op} \; e_2[x \mapsto e]) \\
|
||||
(\texttt{not} \; b)[x \mapsto e] & \equiv \texttt{not} \; (b[x \mapsto e]) \\
|
||||
(b_1 \; \texttt{or} \; b_2)[x \mapsto e] & \equiv (b_1[x \mapsto e] \; \texttt{or} \; b_2[x \mapsto e]) \\
|
||||
(b_1 \; \texttt{and} \; b_2)[x \mapsto e] & \equiv (b_1[x \mapsto e] \; \texttt{and} \; b_2[x \mapsto e])
|
||||
\end{align*}
|
||||
|
||||
\begin{lemma}[]{Substitution Lemma}
|
||||
\[
|
||||
\cB\llbracket b[x \mapsto e] \rrbracket \Leftrightarrow \cB\llbracket b \rrbracket (\sigma[x \mapsto \cA\llbracket e \rrbracket \sigma])
|
||||
\]
|
||||
\end{lemma}
|
||||
+24
@@ -0,0 +1,24 @@
|
||||
\newpage
|
||||
\subsection{Operational Semantics}
|
||||
\textbf{Big-step semantics} describe how the \bi{overall} results of the execution are obtained and use Natural semantics rules.
|
||||
\textbf{Small-step semantics} describe how the individual steps of the computations take place and use Structural Operational Semantics (SOS)
|
||||
|
||||
\subsubsection{Big-Step Semantics}
|
||||
\paragraph{Transition Systems}
|
||||
\inlinedefinition[Transition System] is a tuple $(\Gamma, T, \rightarrow)$, where $\Gamma$ is a set of \bi{configurations},
|
||||
$T$ is a set of terminal configurations, with $T \subseteq \Gamma$ and $\rightarrow$ is a transition relation, with $\rightarrow \; \subseteq \Gamma \times \Gamma$,
|
||||
which describes how executions take place. Big-step transitions are of form $\langle s, \sigma \rangle \rightarrow \sigma'$,
|
||||
e.g. $\langle \texttt{skip}, \sigma \rangle \rightarrow \sigma$
|
||||
|
||||
The transition relations are specified as rules of the form ($^*$ optional side-condition, $\varphi_i$ and $\psi$ transitions)
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\varphi_1}
|
||||
\hypo{\dots}
|
||||
\hypo{\varphi_n}
|
||||
\infer3[(Name)$^*$]{\psi}
|
||||
\end{prooftree}
|
||||
\]
|
||||
or spelled out, ``If $\varpi_1, \ldots, \varphi_n$ are transitions (and the \textit{side-condition} is true), then $\psi$ is a transition''.
|
||||
|
||||
Herein, $\varphi_1, \ldots, \varphi_n$ are called \bi{premises} of the rule and $\psi$ is the \bi{conclusion}. A rule without premises is an \bi{axiom rule}.
|
||||
+54
@@ -0,0 +1,54 @@
|
||||
\paragraph{Big-Step Semantics of IMP}
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{Skip}$_{NS}$]{\langle \texttt{skip}, \sigma \rangle \rightarrow \sigma}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{Ass}$_{NS}$]{\langle x := e, \sigma \rangle \rightarrow \sigma[x \mapsto \cA\llbracket e \rrbracket \sigma ]}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
\shade{gray}{Sequential Composition} $s;s'$ ($s$ is executed in state $\sigma$, then $s'$ in resulting $\sigma'$, resulting in $\sigma''$)
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow \sigma'}
|
||||
\hypo{\langle s', \sigma' \rangle \rightarrow \sigma''}
|
||||
\infer2[\textsc{Seq}$_{NS}$]{\langle s;s', \sigma \rangle \rightarrow \sigma''}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
\shade{gray}{Conditional Statements} $\texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}$ (If $b$ holds, execute $s$, otherwise execute $s'$)
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow \sigma'}
|
||||
\infer1[\textsc{IfT}$_{NS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow \sigma'}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow \sigma'}
|
||||
\infer1[\textsc{IfF}$_{NS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow \sigma'}
|
||||
\end{prooftree}
|
||||
\]
|
||||
Where the first rule applies if $\cB\llbracket b \rrbracket \sigma = \texttt{tt}$
|
||||
|
||||
\shade{gray}{Loop statements} $\texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}$ (If $b$ holds, execute $s$ once, whole statement executed in resulting state $\sigma$)
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow \sigma'}
|
||||
\hypo{\langle \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}, \sigma' \rangle \rightarrow \sigma''}
|
||||
\infer2[\textsc{WhT}$_{NS}$]{\langle \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}, \sigma \rangle \rightarrow \sigma''}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\text{if }
|
||||
\cB\llbracket b \rrbracket \sigma = \texttt{tt}
|
||||
\]
|
||||
If $b$ does not hold, the while statement does \textit{not} modify the state
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{WhF}$_{NS}$]{\langle \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}, \sigma \rangle \rightarrow \sigma}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\text{if }
|
||||
\cB\llbracket b \rrbracket \sigma = \texttt{ff}
|
||||
\]
|
||||
+17
@@ -0,0 +1,17 @@
|
||||
\paragraph{Rule Schemes and Instantiations}
|
||||
Each inference rule is actually a rule scheme, where the meta-variables are placeholders for statements, states, etc.
|
||||
Each rule scheme describes infinitely many \bi{rule instances}.
|
||||
|
||||
A rule is \bi{instantiated} when all meta-variables are replaced with syntactic elements.
|
||||
Assignment rule scheme vs. instance:
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{Ass}$_{NS}$]{\langle x := e, \sigma \rangle \rightarrow \sigma[x \mapsto \cA\llbracket e \rrbracket \sigma]}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{Ass}$_{NS}$]{\langle v := v + 1, \sigma_\text{zero} \rangle \rightarrow \sigma[v \mapsto \cA\llbracket v + 1 \rrbracket \sigma_\text{zero}]}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
The \bi{rule instances} can be combined to derive a transition $\langle s, \sigma \rangle \rightarrow \sigma'$ and we get a derivation tree.
|
||||
+9
@@ -0,0 +1,9 @@
|
||||
\newpage
|
||||
\paragraph{Termination}
|
||||
\begin{definition}[]{Termination}
|
||||
The execution of a statement $s$ in a state $\sigma$
|
||||
\begin{itemize}
|
||||
\item \bi{terminates successfully} if and only if there exists a state $\sigma'$ such that $\vdash \langle s, \sigma \rangle \rightarrow \sigma'$
|
||||
\item \bi{fails to terminate} if and only if there is no state $\sigma'$ such that $\vdash \langle s, \sigma \rangle \rightarrow \sigma'$
|
||||
\end{itemize}
|
||||
\end{definition}
|
||||
+5
@@ -0,0 +1,5 @@
|
||||
\paragraph{Semantic equivalence}
|
||||
\inlinedefinition Two statements $s_1$ and $s_2$ are \bi{semantically equivalent}, denoted $s_1 \simeq s_2$, if and only if
|
||||
\[
|
||||
\forall \sigma, \sigma' . (\vdash \langle s_1, \sigma \rangle \rightarrow \sigma' \Longleftrightarrow \; \vdash \langle s_2, \sigma \rangle \rightarrow \sigma')
|
||||
\]
|
||||
+45
@@ -0,0 +1,45 @@
|
||||
\paragraph{Unfolding loops}
|
||||
In languages like \texttt{C} (and by extension \texttt{C++}) and \texttt{Java}, unfolding a loop leads to non-equivalent code:
|
||||
|
||||
\begin{multicols}{2}
|
||||
\begin{code}{c}
|
||||
int i = 0;
|
||||
while ( i < 2 ) {
|
||||
|
||||
|
||||
while ( i < 1 )
|
||||
if ( i == 0 ) break;
|
||||
|
||||
i++;
|
||||
}
|
||||
printf( "i = %d", i );
|
||||
\end{code}
|
||||
Prints \shade{gray}{\texttt{i = 2}}
|
||||
\begin{code}{c}
|
||||
int i = 0;
|
||||
while ( i < 2 ) {
|
||||
if ( i == 0 ) {
|
||||
if ( i == 0 ) break;
|
||||
while ( i < 1 )
|
||||
if ( i == 0 ) break;
|
||||
}
|
||||
i++;
|
||||
}
|
||||
printf( "i = %d", i );
|
||||
\end{code}
|
||||
Prints \shade{gray}{\texttt{i = 0}}
|
||||
\end{multicols}
|
||||
|
||||
In IMP however, this kind of action leads to equivalence:
|
||||
\[
|
||||
\forall b, s.(\texttt{while b do s end} \; \simeq \; \texttt{if b then s; while b do s end end})
|
||||
\]
|
||||
So what we have to prove is this:
|
||||
\[
|
||||
\forall b, s, \sigma, \sigma'.(\vdash \langle \texttt{while b do s end}, \sigma \rangle \; \Leftrightarrow \;
|
||||
\vdash \langle \texttt{if b then s; while b do s end end}, \sigma \rangle \rightarrow \sigma')
|
||||
\]
|
||||
|
||||
A proof idea is to show equivalence by proving the implication in both directions. For each of them, we show that there is a derivation tree.
|
||||
|
||||
\inlineproof available in the lecture slides for Formal Methods, Slides 78 - 80 (Slide Deck 3, pages 23 - 25)
|
||||
+17
@@ -0,0 +1,17 @@
|
||||
\paragraph{Deterministic Semantics}
|
||||
\inlinelemma The big-step semantics of IMP is deterministic
|
||||
|
||||
\inlineproof We need to show $\forall s, \sigma, \sigma', \sigma''.
|
||||
(\vdash \langle s, \delta \rangle \rightarrow \sigma' \land \vdash \langle s, \sigma \rangle \rightarrow \sigma'' \implies \sigma' = \sigma'')$
|
||||
|
||||
The full proof for this is available on the slides for Formal Methods, pages 82 - 91 (Slide Deck 3, pages 27 - 40)
|
||||
|
||||
In there, \bi{Induction on Derivation Trees} is used.
|
||||
Similar like other induction proofs, we show that a property $P(T)$ holds for all derivation trees $T$,
|
||||
we prove that $P(T)$ holds for an arbitrary derivation tree $T$ under the assumption (the induction hypothesis) that $P(T')$ holds for all sub-trees $T'$ of $T$
|
||||
|
||||
This kind of induction is a special case of \bi{well-founded (Noetherian) induction}.
|
||||
We define $T' \sqsubset T$ (with $T, T'$ derivation trees) to mean that $T'$ is a proper sub-tree of $T$.
|
||||
$\sqsubset$ is a well-founded ordering, because derivation trees are finite and we call $T'$ a \bi{sub-derivation} of $T$ if $T' \sqsubset T$.
|
||||
Typically, \textit{case distinction} is used on the rule applied at the root of $T$ because that provides more information about the structure of the derivation,
|
||||
such as telling us about sub-derivation to which the induction hypothesis applies.
|
||||
+73
@@ -0,0 +1,73 @@
|
||||
\newpage
|
||||
\paragraph{Extensions of IMP}
|
||||
\subparagraph{Local Variable Declarations}
|
||||
\label{sec:big-step-local-var}
|
||||
A statement \texttt{var x := e in s end} declares a local variable that is visible in the sub-statement of the declaration, \texttt{s}.
|
||||
|
||||
Here, the Expression $e$ is evaluated in the initial state, then $s$ is executed in a state in which $x$ has the value of $e$ and after the execution,
|
||||
the original value of $x$ is restored.
|
||||
|
||||
The corresponding Big-step semantics rule is:
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma[x \mapsto \cA \llbracket e \rrbracket \sigma] \rangle \rightarrow \sigma' }
|
||||
\infer1[\textsc{Loc}$_{NS}$]{\langle \texttt{var x := e in s end}, \sigma \rangle \rightarrow \sigma'[x \mapsto \sigma(x)]}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
|
||||
\subparagraph{Procedure Declaration and Calls}
|
||||
\[
|
||||
\texttt{procedure p(}x_1, \ldots, x_n; y_1, \ldots, y_m \texttt{) begin s end}
|
||||
\]
|
||||
Here, the $x_i$ are the \bi{value} parameters and the $y_j$ are the \bi{variable} parameters. The latter can be used to assign values back to the procedure caller (return values).
|
||||
|
||||
In a \bi{procedure declaration} the \bi{formal} parameter names $x_i$ and $y_j$ must be pairwise distinct and the only free variables in $s$.
|
||||
|
||||
For the \bi{procedure call} $p(e_1, \ldots, e_n; z_1, \ldots, z_m)$, the \bi{actual} variable parameters must be pairwise distinct.
|
||||
|
||||
The corresponding Big-step semantics rule is:
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma_\text{zero}[\overrightharpoon{x_i} \mapsto \overrightharpoon{\cA \llbracket e_i \rrbracket \sigma}]
|
||||
[\overrightharpoon{y_j} \mapsto \overrightharpoon{\sigma(z_j)}] \rangle \rightarrow \sigma'}
|
||||
\infer1[\textsc{Call}$_{NS}$]{\langle p(\overrightharpoon{e_i}; \overrightharpoon{z_j}), \sigma \rangle
|
||||
\rightarrow \sigma[\overrightharpoon{z_j} \mapsto \overrightharpoon{\sigma'(y_j)}]}
|
||||
\end{prooftree}
|
||||
\]
|
||||
where the notation $\sigma[\overrightharpoon{x_i} \mapsto \overrightharpoon{v_i}]$ is an abbreviation of $\sigma[x_1 \mapsto v_1]\ldots[x_n \mapsto v_n]$
|
||||
|
||||
|
||||
\subparagraph{Non-determinism}
|
||||
For a statement $s \bigbox s'$, either $s$ or $s'$ is non-deterministically chosen to be executed.
|
||||
|
||||
\inlineexample In the statement \texttt{x := 1 $\bigbox$ (x := 2; x := x + 2)}, we either get $x = 1$ or $x = 4$
|
||||
(either the statement on the left or right of the box is evaluated)
|
||||
|
||||
The corresponding rules are:
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow \sigma'}
|
||||
\infer1[\textsc{ND1}$_{NS}$]{\langle s \bigbox s', \sigma \rangle \rightarrow \sigma'}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s', \sigma \rangle \rightarrow \sigma'}
|
||||
\infer1[\textsc{ND2}$_{NS}$]{\langle s \bigbox s', \sigma \rangle \rightarrow \sigma'}
|
||||
\end{prooftree}
|
||||
\]
|
||||
An important note on non-terminating branches, we will not ``see'' them, because big-step semantics can't encompass that concept.
|
||||
|
||||
|
||||
\subparagraph{Parallelism}
|
||||
In a statement \texttt{s par s'}, both $s$ and $s'$ are executed, but their execution can be \bi{interleaved}.
|
||||
|
||||
\inlineexample \texttt{x := 1 par (x := 2; x := x + 2)} could result in:
|
||||
\begin{multicols}{2}
|
||||
\begin{itemize}
|
||||
\item $4$: first \texttt{x:=1}, then \texttt{x:=2} and finally \texttt{x:=x+2}
|
||||
\item $1$: first \texttt{x:=2}, then \texttt{x:=x+2} and finally \texttt{x:=1}
|
||||
\item $3$: first \texttt{x:=2}, then \texttt{x:=1} and finally \texttt{x:=x+2}
|
||||
\end{itemize}
|
||||
\end{multicols}
|
||||
In Big-step semantics however, there are no rules for this, because it can only define atomic steps.
|
||||
+17
@@ -0,0 +1,17 @@
|
||||
\newpage
|
||||
\subsubsection{Small-Step semantics}
|
||||
\paragraph{Structural Operational Semantics (SOS)}
|
||||
Expressing each individual steps of execution allows one to express the \bi{order of execution} of these steps,
|
||||
thus allowing us to describe properties of non-terminating programs and parallelization.
|
||||
|
||||
$\gamma$ is used as the meta-variable for terminal and non-terminal configurations.
|
||||
For the transitions, we denote the relation $\rightarrow_1$, which can have two forms:
|
||||
\begin{itemize}
|
||||
\item $\langle s, \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle$ is for any non-complete computation,
|
||||
where the next computation is expressed by the intermediate configuration $\langle s', \sigma' \rangle$
|
||||
\item $\langle s, \sigma \rangle \rightarrow_1 \sigma'$ is the final execution that reaches a terminal state.
|
||||
\end{itemize}
|
||||
|
||||
Finally, a transition $\langle s, \sigma \rangle \rightarrow_1 \gamma$ describes the \bi{first step} of the execution of $s$ in state $\sigma$.
|
||||
|
||||
A non-terminal configuration $\langle s, \sigma \rangle$ is \bi{stuck}, if there does not exist a configuration $\gamma$ such that $\langle s, \sigma \rangle \rightarrow_1 \gamma$.
|
||||
+56
@@ -0,0 +1,56 @@
|
||||
\subparagraph{The rules}
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{Skip}$_{SOS}$]{\langle \texttt{skip}, \sigma \rangle \rightarrow_1 \sigma}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{Ass}$_{SOS}$]{\langle x := e, \sigma \rangle \rightarrow_1 \sigma[x \mapsto \cA\llbracket e \rrbracket \sigma ]}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
\shade{gray}{Sequential Composition} $s;s'$ ($s$ is executed in state $\sigma$, then $s'$ in resulting $\sigma'$, resulting in $\sigma''$).
|
||||
Then, either $s$ executes completely in one step (\textsc{Seq1}), or does not (\textsc{Seq2}).
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow_1 \sigma'}
|
||||
\infer1[\textsc{Seq1}$_{SOS}$]{\langle s;s', \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s', \sigma' \rangle \rightarrow_1 \langle s'', \sigma' \rangle}
|
||||
\infer1[\textsc{Seq2}$_{SOS}$]{\langle s;s', \sigma \rangle \rightarrow_1 \langle s'';s', \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
\shade{gray}{Conditional Statements} $\texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}$ (If $b$ holds, execute $s$, otherwise execute $s'$)
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{IfT}$_{SOS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{IfF}$_{SOS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\]
|
||||
Where the first rule applies if $\cB\llbracket b \rrbracket \sigma = \texttt{tt}$. Below a further two rules for the true case:
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow_1 \sigma'}
|
||||
\infer1[\textsc{IfT1}$_{SOS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow_1 \sigma'}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow_1 \langle s'', \sigma' \rangle}
|
||||
\infer1[\textsc{IfT2}$_{SOS}$]{\langle \texttt{if}\;b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow_1 \langle s''', \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
|
||||
\shade{gray}{Loop statements} $\texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}$ (If $b$ holds, execute $s$ once, whole statement executed in resulting state $\sigma$)
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{While}$_{SOS}$]{\langle \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}, \sigma \rangle \rightarrow_1
|
||||
\langle \texttt{if} \; b \; \texttt{then} \; s; \; \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end else skip end}, \sigma \rangle}
|
||||
\end{prooftree}
|
||||
\]
|
||||
+22
@@ -0,0 +1,22 @@
|
||||
\paragraph{Multi-Step Execution}
|
||||
We use the definitions we have to define a \bi{$k$-step execution}, denoted $\gamma \rightarrow_1^k \gamma'$.
|
||||
Of course, this means intuitively that there is an execution of exactly $k$ steps from $\gamma$ to $\gamma'$.
|
||||
|
||||
We define the relation inductively over $k$:
|
||||
\begin{itemize}
|
||||
\item $\gamma \rightarrow_1^0 \gamma'$ if and only if $\gamma = \gamma'$
|
||||
\item $\gamma \rightarrow_1^k \gamma'$ if and only if there exists $\gamma''$ such that both $\vdash \gamma \rightarrow_1$ and $\gamma'' \rightarrow_1^{k - 1} \gamma'$
|
||||
\end{itemize}
|
||||
Resulting from this, $\gamma \rightarrow_1^{k_1 + k_2} \gamma'$ if and only if $\exists \gamma'' . \gamma \rightarrow_1^{k_1} \gamma'' \land \gamma'' \rightarrow_1^{k_2} \gamma'$
|
||||
|
||||
We write $\gamma \rightarrow_1^* \gamma'$ to signify that there is an execution from $\gamma$ to $\gamma'$ in some finite number of steps, or more formally:
|
||||
\[
|
||||
\exists k. \gamma \rightarrow_1^k \gamma'
|
||||
\]
|
||||
|
||||
|
||||
\paragraph{Derivation Sequences}
|
||||
\inlinedefinition A \bi{derivation sequence} is a non-empty sequence of configurations $\gamma_0, \ldots$, for which $\gamma_i \rightarrow_1^1 \gamma_{i + 1}$ for each $0 \leq i$,
|
||||
such that $i + 1$ is in the range of the sequence. If the sequence is finite, then the last configuration in the sequence is either a terminal or stuck configuration.
|
||||
|
||||
The \bi{length} of the derivation sequence is the number of transitions (thus number of states minus one!)
|
||||
+10
@@ -0,0 +1,10 @@
|
||||
\paragraph{Termination}
|
||||
\inlinetheorem The execution of a statement $s$ in a state $\sigma$
|
||||
\begin{itemize}
|
||||
\item \bi{terminates} if and only if there is a finite derivation sequence starting with $\langle s, \sigma \rangle$
|
||||
\item \bi{runs forever} if and only if there is an infinite derivation sequence starting with $\langle s, \sigma \rangle$
|
||||
\end{itemize}
|
||||
|
||||
\inlinetheorem The execution of statement $s$ in state $\sigma$ \bi{terminates} successfully, if and only if $\exists \sigma'. \langle s, \sigma \rangle \rightarrow^*_1 \sigma'$
|
||||
|
||||
Of note is that these are properties of \bi{configurations} and not just statements.
|
||||
+6
@@ -0,0 +1,6 @@
|
||||
\paragraph{Proving properties of Derivation Sequences}
|
||||
For reasoning about finite derivation sequences, we commonly reason about a multi-step execution $\gamma \rightarrow_1^k \gamma'$
|
||||
by \bi{strong induction on the number of steps $k$}, where we define $P(k) \equiv$ ``for all executions of length k, our property holds'' and we prove $P(k)$ for arbitrary $k$
|
||||
with the \bi{induction hypothesis} $\forall k' < k. P(k')$ holds
|
||||
|
||||
After the setup, it \textit{often} proceeds by case distinction on the $0$ step and the other steps
|
||||
+16
@@ -0,0 +1,16 @@
|
||||
\paragraph{Semantic Equivalence and Determinism}
|
||||
\inlinedefinition Under the small-step semantics, two statements $s_1$ and $s_2$ are \bi{semantically equivalent} if for all states $\sigma$ both:
|
||||
\begin{itemize}
|
||||
\item for all stuck or terminal configurations $\gamma$ we have $\langle s_1, \sigma \rangle \rightarrow_1^* \gamma$ if and only if
|
||||
$\langle s_2, \sigma \rangle \rightarrow_1^* \gamma$, and
|
||||
\item there is and infinite derivation sequence starting in $\langle s_1, \sigma \rangle$ if and only if there is one starting in $\langle s_2, \sigma \rangle$
|
||||
\end{itemize}
|
||||
|
||||
\inlinelemma The small-step semantics of IMP is \bi{deterministic}. That is:
|
||||
\[
|
||||
\forall s, \sigma, \gamma, \gamma'. \vdash \langle s, \sigma \rangle \rightarrow_1 \gamma
|
||||
\land \vdash \langle s, \gamma \rangle \rightarrow_1 \gamma'
|
||||
\implies \gamma = \gamma'
|
||||
\]
|
||||
|
||||
\inlinecorollary There is exactly one derivation sequence starting in configuration $\langle s, \sigma \rangle$
|
||||
+67
@@ -0,0 +1,67 @@
|
||||
\paragraph{Extensions of IMP}
|
||||
|
||||
\subparagraph{Local Variable Declarations}
|
||||
As already partially established in Section \ref{sec:big-step-local-var}, the steps to define a local variable are (for \texttt{var x:=e in s end}):
|
||||
\begin{multicols}{3}
|
||||
\begin{enumerate}
|
||||
\item Assign $e$ to $x$
|
||||
\item Execute $s$ (possibly many steps)
|
||||
\item Restore the initial value of $x$
|
||||
\end{enumerate}
|
||||
\end{multicols}
|
||||
|
||||
Since we need to somehow inject he restore instruction into the statements $s$, we extend the \texttt{Stm} category with a \texttt{restore} statement,
|
||||
defined as \texttt{restore (Var, Val)}.
|
||||
|
||||
With that, we can define the rules:
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{Loc}$_{SOS}$]{\langle \texttt{var x:= e in s end}, \sigma \rangle \rightarrow_1 \langle \texttt{s;restore }(x, \sigma(x)),
|
||||
\sigma[x \mapsto \cA \llbracket e \rrbracket \sigma] \rangle}
|
||||
\end{prooftree}
|
||||
\]
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{Ret}$_{SOS}$]{\langle \texttt{restore }(x, \sigma(x)), \sigma \rangle \rightarrow_1 \sigma[x \mapsto v]}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
Of course, we could also just model execution stacks, as most languages do.
|
||||
|
||||
|
||||
\subparagraph{Non-determinism}
|
||||
The rules here are analogous to the ones from the big-step rules
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{ND1}$_{SOS}$]{\langle s \bigbox s', \sigma \rangle \rightarrow_1 \langle s, \sigma \rangle}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{ND2}$_{SOS}$]{\langle s \bigbox s', \sigma \rangle \rightarrow_1 \langle s, \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
|
||||
\subparagraph{Parallelism}
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow_1 \langle s'', \sigma' \rangle}
|
||||
\infer1[\textsc{Par1}$_{SOS}$]{\langle s \texttt{ par } s', \sigma \rangle \rightarrow_1 \langle s'' \texttt{ par } s', \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow_1 \sigma'}
|
||||
\infer1[\textsc{Par2}$_{SOS}$]{\langle s \texttt{ par } s', \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\]
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s', \sigma \rangle \rightarrow_1 \langle s'', \sigma' \rangle}
|
||||
\infer1[\textsc{Par3}$_{SOS}$]{\langle s \texttt{ par } s', \sigma \rangle \rightarrow_1 \langle s \texttt{ par } s'', \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s', \sigma \rangle \rightarrow_1 \sigma'}
|
||||
\infer1[\textsc{Par4}$_{SOS}$]{\langle s \texttt{ par } s', \sigma \rangle \rightarrow_1 \langle s, \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\]
|
||||
@@ -0,0 +1,24 @@
|
||||
\newpage
|
||||
\subsubsection{Equivalence}
|
||||
\begin{theorem}[]{Equivalence Theorem}
|
||||
For every statement $s$ of IMP, we have
|
||||
\[
|
||||
\vdash \langle s, \sigma \rangle \rightarrow \sigma' \Leftrightarrow \langle s, \sigma \rangle \rightarrow_1^* \sigma'
|
||||
\]
|
||||
{\scriptsize If the execution of $s$ from some state terminates successfully in one of the semantics, than so will it in the other.
|
||||
The execution fails to terminate in the big-step semantics if and only if it either gets stuck, or runs forever in the small-step semantics}
|
||||
\end{theorem}
|
||||
|
||||
|
||||
\inlinelemma[Equivalence Lemma 1] For every statement $s$ of IMP and states $\sigma$ and $\sigma'$ we have:
|
||||
\[
|
||||
\vdash \langle s, \sigma \rangle \rightarrow \sigma' \implies \langle s, \sigma \rangle \rightarrow_1^* \sigma'
|
||||
\]
|
||||
{\scriptsize If the execution of $s$ from $\sigma$ terminates successfully in the big-step semantics, so will it in the small-step semantics (in the same state, too!)}
|
||||
|
||||
|
||||
\inlinelemma[Equivalence Lemma 2] For every statement $s$ of IMP and states $\sigma$ and $\sigma'$ and $k \in \N$, we have:
|
||||
\[
|
||||
\langle s, \sigma \rangle \rightarrow_1^k \sigma' \implies \vdash \langle s, \sigma \rangle \rightarrow \sigma'
|
||||
\]
|
||||
{\scriptsize If the execution of $s$ from $\sigma$ terminates successfully in the small-step semantics, so will it in the big-step semantics (in the same state, too!)}
|
||||
+184
@@ -0,0 +1,184 @@
|
||||
\newpage
|
||||
\subsubsection{Operational Semantics Rules Overview}
|
||||
\paragraph{Big-Step Semantics}
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{Skip}$_{NS}$]{\langle \texttt{skip}, \sigma \rangle \rightarrow \sigma}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{Ass}$_{NS}$]{\langle x := e, \sigma \rangle \rightarrow \sigma[x \mapsto \cA\llbracket e \rrbracket \sigma ]}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow \sigma'}
|
||||
\hypo{\langle s', \sigma' \rangle \rightarrow \sigma''}
|
||||
\infer2[\textsc{Seq}$_{NS}$]{\langle s;s', \sigma \rangle \rightarrow \sigma''}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow \sigma'}
|
||||
\infer1[\textsc{IfT}$_{NS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow \sigma'}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow \sigma'}
|
||||
\infer1[\textsc{IfF}$_{NS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow \sigma'}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
\begin{align*}
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow \sigma'}
|
||||
\hypo{\langle \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}, \sigma' \rangle \rightarrow \sigma''}
|
||||
\infer2[\textsc{WhT}$_{NS}$]{\langle \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}, \sigma \rangle \rightarrow \sigma''}
|
||||
\end{prooftree}
|
||||
& &
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{WhF}$_{NS}$]{\langle \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}, \sigma \rangle \rightarrow \sigma}
|
||||
\end{prooftree} \\
|
||||
\text{if }
|
||||
\cB\llbracket b \rrbracket \sigma = \texttt{tt}
|
||||
& &
|
||||
\text{if }
|
||||
\cB\llbracket b \rrbracket \sigma = \texttt{ff}
|
||||
\end{align*}
|
||||
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{Ass}$_{NS}$]{\langle x := e, \sigma \rangle \rightarrow \sigma[x \mapsto \cA\llbracket e \rrbracket \sigma]}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{Ass}$_{NS}$]{\langle v := v + 1, \sigma_\text{zero} \rangle \rightarrow \sigma[v \mapsto \cA\llbracket v + 1 \rrbracket \sigma_\text{zero}]}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
\paragraph{Small-Step Semantics}
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{Skip}$_{SOS}$]{\langle \texttt{skip}, \sigma \rangle \rightarrow_1 \sigma}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{Ass}$_{SOS}$]{\langle x := e, \sigma \rangle \rightarrow_1 \sigma[x \mapsto \cA\llbracket e \rrbracket \sigma ]}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow_1 \sigma'}
|
||||
\infer1[\textsc{Seq1}$_{SOS}$]{\langle s;s', \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s', \sigma' \rangle \rightarrow_1 \langle s'', \sigma' \rangle}
|
||||
\infer1[\textsc{Seq2}$_{SOS}$]{\langle s;s', \sigma \rangle \rightarrow_1 \langle s'';s', \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{IfT}$_{SOS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{IfF}$_{SOS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow_1 \sigma'}
|
||||
\infer1[\textsc{IfT1}$_{SOS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow_1 \sigma'}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow_1 \langle s'', \sigma' \rangle}
|
||||
\infer1[\textsc{IfT2}$_{SOS}$]{\langle \texttt{if}\;b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow_1 \langle s''', \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{While}$_{SOS}$]{\langle \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}, \sigma \rangle \rightarrow_1
|
||||
\langle \texttt{if} \; b \; \texttt{then} \; s; \; \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end else skip end}, \sigma \rangle}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
\paragraph{Extensions}
|
||||
\subparagraph{Big-Step Semantics}
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma[x \mapsto \cA \llbracket e \rrbracket \sigma] \rangle \rightarrow \sigma' }
|
||||
\infer1[\textsc{Loc}$_{NS}$]{\langle \texttt{var x := e in s end}, \sigma \rangle \rightarrow \sigma'[x \mapsto \sigma(x)]}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma_\text{zero}[\overrightharpoon{x_i} \mapsto \overrightharpoon{\cA \llbracket e_i \rrbracket \sigma}]
|
||||
[\overrightharpoon{y_j} \mapsto \overrightharpoon{\sigma(z_j)}] \rangle \rightarrow \sigma'}
|
||||
\infer1[\textsc{Call}$_{NS}$]{\langle p(\overrightharpoon{e_i}; \overrightharpoon{z_j}), \sigma \rangle
|
||||
\rightarrow \sigma[\overrightharpoon{z_j} \mapsto \overrightharpoon{\sigma'(y_j)}]}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow \sigma'}
|
||||
\infer1[\textsc{ND1}$_{NS}$]{\langle s \bigbox s', \sigma \rangle \rightarrow \sigma'}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s', \sigma \rangle \rightarrow \sigma'}
|
||||
\infer1[\textsc{ND2}$_{NS}$]{\langle s \bigbox s', \sigma \rangle \rightarrow \sigma'}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
|
||||
\subparagraph{Small-Step Semantics}
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{Loc}$_{SOS}$]{\langle \texttt{var x:= e in s end}, \sigma \rangle \rightarrow_1 \langle \texttt{s;restore }(x, \sigma(x)),
|
||||
\sigma[x \mapsto \cA \llbracket e \rrbracket \sigma] \rangle}
|
||||
\end{prooftree}
|
||||
\]
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{Ret}$_{SOS}$]{\langle \texttt{restore }(x, \sigma(x)), \sigma \rangle \rightarrow_1 \sigma[x \mapsto v]}
|
||||
\end{prooftree}
|
||||
\]
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{ND1}$_{SOS}$]{\langle s \bigbox s', \sigma \rangle \rightarrow_1 \langle s, \sigma \rangle}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\infer0[\textsc{ND2}$_{SOS}$]{\langle s \bigbox s', \sigma \rangle \rightarrow_1 \langle s, \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\]
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow_1 \langle s'', \sigma' \rangle}
|
||||
\infer1[\textsc{Par1}$_{SOS}$]{\langle s \texttt{ par } s', \sigma \rangle \rightarrow_1 \langle s'' \texttt{ par } s', \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s, \sigma \rangle \rightarrow_1 \sigma'}
|
||||
\infer1[\textsc{Par2}$_{SOS}$]{\langle s \texttt{ par } s', \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\]
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s', \sigma \rangle \rightarrow_1 \langle s'', \sigma' \rangle}
|
||||
\infer1[\textsc{Par3}$_{SOS}$]{\langle s \texttt{ par } s', \sigma \rangle \rightarrow_1 \langle s \texttt{ par } s'', \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\hypo{\langle s', \sigma \rangle \rightarrow_1 \sigma'}
|
||||
\infer1[\textsc{Par4}$_{SOS}$]{\langle s \texttt{ par } s', \sigma \rangle \rightarrow_1 \langle s, \sigma' \rangle}
|
||||
\end{prooftree}
|
||||
\]
|
||||
@@ -0,0 +1,45 @@
|
||||
\newpage
|
||||
\subsection{Axiomatic Semantics}
|
||||
\subsubsection{Program Correctness}
|
||||
\inlinedefinition[Partial Correctness] \textit{if} a program terminates \textit{then} there will be a certain relationship between the initial and final state
|
||||
|
||||
\inlinedefinition[Total Correctness] Program terminates \textit{and} is partially correct, i.e.\\
|
||||
\texttt{total correctness = partial correctness + termination}
|
||||
|
||||
\inlinedefinition[Formal Specification] is used to expressed the aforementioned relationship between the initial and final state.
|
||||
It does not include guarantees for termination and can thus only be used to provide a starting point for a prove of partial correctness.
|
||||
|
||||
We typically express \bi{Formal Specifications} using Small- or Big-Step semantics.
|
||||
|
||||
\inlineexample Consider the factorial statement
|
||||
\begin{code}{text}
|
||||
y := 1;
|
||||
while not x = 1 do
|
||||
y := y * x;
|
||||
x := x - 1
|
||||
end
|
||||
\end{code}
|
||||
The specification that we want to prove is here given by ``The final value of \texttt{y} is the factorial of the initial value \texttt{x}''.
|
||||
Do note that this statement is only partially correct, as it does not terminate for $x < 1$.
|
||||
|
||||
We can express the specification formally as follows using big-step semantics:
|
||||
\[
|
||||
\forall \sigma, \sigma'. \vdash \langle y := 1; \texttt{while not x = 1 do y := y * x; x := x - 1 end}, \sigma \rangle \rightarrow \sigma'
|
||||
\implies \sigma'(\texttt{y}) = \sigma(\texttt{x})! \land \sigma(\texttt{x}) > 0
|
||||
\]
|
||||
|
||||
% We then prove the partial correctness in three steps:
|
||||
%
|
||||
% \bi{Step 1}: The body of the loop
|
||||
% \[
|
||||
% \forall \sigma, \sigma''. \vdash \langle \texttt{y := y * x; x := x - 1}, \sigma \rangle \rightarrow \sigma'' \land \sigma''(\texttt{x}) > 0
|
||||
% \implies \sigma(\texttt{y}) \times \sigma(\texttt{x})! = \sigma''(\texttt{y}) \times \sigma''(\texttt{x})! \land \sigma(\texttt{x}) > 0
|
||||
% \]
|
||||
%
|
||||
% \bi{Step 2}: The loop satisfies
|
||||
% \[
|
||||
% \forall \sigma, \sigma''. \vdash \langle \texttt{y := y * x; x := x - 1}, \sigma \rangle \rightarrow \sigma'' \land \sigma''(\texttt{x}) > 0
|
||||
% \implies \sigma(\texttt{y}) \times \sigma(\texttt{x})! = \sigma''(\texttt{y}) \times \sigma''(\texttt{x})! \land \sigma(\texttt{x}) > 0
|
||||
% \]
|
||||
Since these kinds of proofs take a lot of effort and get very complicated rather quickly, axiomatic semantics provide a nice and fast way of proving correctness,
|
||||
because we can focus on the essential properties.
|
||||
+17
@@ -0,0 +1,17 @@
|
||||
\newpage
|
||||
\subsubsection{Hoare Logic}
|
||||
\paragraph{Hoare Triples}
|
||||
\inlinedefinition Properties are specified as \bi{Hoare Triples} $\{ \bm{P} \} \ s \ \{ \bm{Q} \}$, with statement $s$, $\bm{P}$ the precondition and $\bm{Q}$ the postcondition.
|
||||
Here, $\bm{P}, \bm{Q}$ are assertions and are, together with $\bm{R}$, meta-variables over assertions.
|
||||
|
||||
\inlinedefinition[Logical Variables] To keep the original value of a variable, we can ``reassign'' values in the precondition
|
||||
(e.g. $x = N$ to then in the postcondition state something regarding $N$).
|
||||
|
||||
Pre- and Postconditions are assertions, i.e. they are boolean expressions plus logical variables.
|
||||
Often, quantification is used in assertions as well in practice, as well as other expressions such as $x!$ when it is convenient and we also assume that the \bi{substitution lemma}
|
||||
still holds:
|
||||
\[
|
||||
\cB \llbracket \bm{P}[x \mapsto e] \rrbracket \sigma = \cB \llbracket \bm{P} \rrbracket \sigma [x \mapsto \cA \llbracket e \rrbracket \sigma]
|
||||
\]
|
||||
|
||||
We use $P_1 \land P_2$ instead of $P_1 \texttt{and} P_2$, $P_1 \lor P_2$ instead of $P_1 \texttt{or} P_2$ and $\neg P$ instead of $\texttt{not} P$
|
||||
+78
@@ -0,0 +1,78 @@
|
||||
\paragraph{Derivation Systems}
|
||||
We again use derivation trees, where their rules specify which triples can be derived for each statement.
|
||||
The premises and conclusions of the derivation rules are Hoare Triples.
|
||||
|
||||
Again, we write $\vdash \{ \bm{P} \} \ s \ \{ \bm{Q} \}$ if there exists a (finite) derivation tree ending in $\{ \bm{P} \} \ s \ \{ \bm{Q} \}$, and
|
||||
\[
|
||||
\vdash \{ \bm{P} \} \ s \ \{ \bm{Q} \} \Leftrightarrow \exists T. \texttt{root}(T) \equiv \{ \bm{P} \} \ s \ \{ \bm{Q} \}
|
||||
\]
|
||||
|
||||
|
||||
\subparagraph{The rules}
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[$\textsc{Skip}_{Ax}$]{\{ \bm{P} \} \ \texttt{skip} \ \{ \bm{P} \}}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\infer0[$\textsc{Ass}_{Ax}$]{\{ \bm{P}[x \mapsto e] \} \ \texttt{x := e} \ \{ \bm{P} \}}
|
||||
\end{prooftree}
|
||||
\]
|
||||
|
||||
Sequential Composition \texttt{s;s'}, loop (\texttt{while b do s end}) and conditional statements (\texttt{if b then s1 else s2 end})
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\{ \bm{P} \} \ s \ \{ \bm{Q} \}}
|
||||
\hypo{\{ \bm{Q} \} \ s' \ \{ \bm{R} \}}
|
||||
\infer2[$\textsc{Seq}_{Ax}$]{\{ \bm{P} \} \ \texttt{s;s'} \ \{ \bm{P} \}}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\begin{prooftree}
|
||||
\hypo{\{ b \land \bm{P} \} \ s \ \{ \bm{Q} \}}
|
||||
\hypo{\{ \neg b \land \bm{P} \} \ s' \ \{ \bm{Q} \}}
|
||||
\infer2[$\textsc{If}_{Ax}$]{\{ \bm{P} \} \ \texttt{if b then s else s' end} \ \{ \bm{Q} \}}
|
||||
\end{prooftree}
|
||||
\]
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\{ b \land \bm{P} \} \ s \ \{ \bm{P} \}}
|
||||
\infer1[$\textsc{Wh}_{Ax}$]{\{ \bm{P} \} \ \texttt{while b do s end} \ \{ \neg b \land \bm{P} \}}
|
||||
\end{prooftree}
|
||||
\]
|
||||
With these rules, we can only evaluate \textit{syntactically}, thus expressions like $\{ x = 4 \land y = 5 \} \ \texttt{skip} \ \{ y = 5 \land x = 4 \}$
|
||||
are not an instance of the $\textsc{Skip}_{Ax}$ because the precondition and postcondition are not identical. Thus we often need to apply \textit{semantic} reasoning,
|
||||
e.g. applying mathematical properties.
|
||||
|
||||
\inlinedefinition[Semantic entailment] expresses the reasoning steps
|
||||
``We write $\bm{P} \models \bm{Q}$ if and only if for all states $\sigma$,
|
||||
$\cB \llbracket \bm{P} \rrbracket \sigma = \texttt{tt}$ implies $\cB \llbracket \bm{Q} \rrbracket \sigma = \texttt{tt}$''
|
||||
|
||||
This leads to the \bi{Rule of Consequence}
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\{ \bm{P}' \} \ s \ \{ \bm{Q}' \}}
|
||||
\infer1[$\textsc{Cons}_{Ax}$]{\{ \bm{P} \} \ s \ \{ \bm{Q} \}}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\text{if } \bm{P} \models \bm{P}' \text{ and } \bm{Q}' \models \bm{Q}
|
||||
\]
|
||||
a rule, where we can \bi{strengthen preconditions} ($\bm{P}$ cannot be weaker than $\bm{P}'$) and \bi{weaken postconditions} ($\bm{Q}$ cannot be stronger than $\bm{Q}'$)
|
||||
|
||||
Since the derivation trees often get quite large, we can group them around each line in the program text.
|
||||
|
||||
\shade{gray}{Inline Notation} can be used to make the changes more easily legible.
|
||||
For example, to express instances of $\textsc{Skip}_{Ax}$, instead of writing $\vdash \{ \bm{P} \} \ \texttt{skip} \ \{ \bm{P} \}$, we can write.
|
||||
More examples on slides 167 - 170 (pages 30 - 33 in Slide Deck 4)
|
||||
\rmvspace
|
||||
\begin{align*}
|
||||
& \{ \bm{P} \} \\
|
||||
& \quad \texttt{skip} \\
|
||||
& \{ \bm{P} \}
|
||||
\end{align*}
|
||||
|
||||
\shade{gray}{Forward Assignment}
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\infer0[$\textsc{AssF}_{Ax}$]{\{ \bm{P} \} \ x := e \ \{ \exists V. \bm{P}[x \mapsto V] \land x = e[x \mapsto V] \}}
|
||||
\end{prooftree}
|
||||
\]
|
||||
+12
@@ -0,0 +1,12 @@
|
||||
\paragraph{Total Correctness}
|
||||
We use a different form of Hoare triple $\{ \bm{P} \} \ s \ \{ \Downarrow \bm{Q} \}$, which describes total correctness.
|
||||
|
||||
All rules for total correctness are equivalent to the ones for partial correctness, apart from the rule for loops.
|
||||
\[
|
||||
\begin{prooftree}
|
||||
\hypo{\{ b \land \bm{P} \land e = Z \} \ s \ \{ \Downarrow \bm{P} \land e < Z \}}
|
||||
\infer1[$\textsc{WhTot}_{Ax}$]{\{ \bm{P} \} \ \texttt{while b do s end} \ \{ \Downarrow \neg b \land \bm{P} \}}
|
||||
\end{prooftree}
|
||||
\qquad
|
||||
\text{if } b \land \bm{P} \models 0 \leq e
|
||||
\]
|
||||
+27
@@ -0,0 +1,27 @@
|
||||
\subsubsection{Soundness and Completeness}
|
||||
\inlinedefinition[Soundness] If a property can be proven, then it holds.
|
||||
As a result, an unsound derivation system does not provide any guarantees, as we may miss errors (we may have false negatives).
|
||||
|
||||
\inlinedefinition[Completeness] If a property holds, then it can be proven.
|
||||
As a result, we may have a correct program that we can't prove in an incomplete derivation system (we may have false positives)
|
||||
|
||||
Both can be proven with regard to an operational semantics.
|
||||
|
||||
\inlineexample The partial correctness triple $\{ \bm{P} \} \ s \ \{ \bm{Q} \}$ is valid, written $\models \{ \bm{P} \} \ s \ \{ \bm{Q} \}$ if and only if
|
||||
\[
|
||||
\forall \sigma, \sigma'. \cB \llbracket \bm{P} \rrbracket \sigma = \texttt{tt} \land \vdash \langle s, \sigma \rangle \rightarrow \sigma'
|
||||
\implies \cB \llbracket \bm{Q} \rrbracket \sigma' = \texttt{tt}
|
||||
\]
|
||||
|
||||
More generally:
|
||||
\begin{itemize}
|
||||
\item \bi{Soundness} $\vdash \{ \bm{P} \} \ s \ \{ \bm{Q} \} \implies \models \{ \bm{P} \} \ s \ \{ \bm{Q} \}$
|
||||
\item \bi{Soundness} $\models \{ \bm{P} \} \ s \ \{ \bm{Q} \} \implies \vdash \{ \bm{P} \} \ s \ \{ \bm{Q} \}$
|
||||
\end{itemize}
|
||||
|
||||
\begin{theorem}[]{Soundness, Completeness}
|
||||
For all partial correctness triples $\{ \bm{P} \} \ s \ \{ \bm{Q} \}$ of IMP we have
|
||||
\[
|
||||
\vdash \{ \bm{P} \} \ s \ \{ \bm{Q} \} \Leftrightarrow \models \{ \bm{P} \} \ s \ \{ \bm{Q} \}
|
||||
\]
|
||||
\end{theorem}
|
||||
Reference in New Issue
Block a user