mirror of
https://github.com/janishutz/eth-summaries.git
synced 2026-05-30 22:31:19 +02:00
46 lines
2.3 KiB
TeX
46 lines
2.3 KiB
TeX
\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.
|