eth-janishutz/eth-summaries
1
0
Fork 0
mirror of https://github.com/janishutz/eth-summaries.git synced 2026-05-30 16:21:19 +02:00
Code Issues Packages Projects Releases Wiki Activity

[FMFP] Axiomatic semantics

Browse Source
This commit is contained in:
Janis Hutz
2026-05-05 14:39:56 +02:00
parent 0ec1799321
commit 0e4ccf58f4
8 changed files with 370 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
semester4/fmfp/parts/03_language-semantics/01_operational-semantics/03_rules-summary.tex
+184
View File
@@ -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}
\]
semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/00_intro.tex
+45
View File
@@ -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.
semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/00_triples-assertions.tex
+17
View File
@@ -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$
semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/01_derivation-systems.tex
+78
View File
@@ -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}
\]
semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/02_total-correctness.tex
+12
View File
@@ -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
\]
semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/02_soundness-completeness.tex
+27
View File
@@ -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}