mirror of
https://github.com/janishutz/eth-summaries.git
synced 2026-07-28 09:49:11 +02:00
20 lines
1.4 KiB
TeX
20 lines
1.4 KiB
TeX
\subsubsection{Axiomatic Semantics}
|
|
Here, we need to find pre- and postconditions for expressions and prove that they are correct.
|
|
|
|
To do the proofs, we again apply transition rules, as was the case already with operational semantics.
|
|
Contrary to those however, we have pre- and postconditions, which we typically need to define ourselves.
|
|
|
|
This typically involves finding a loop invariant that holds before and after each iteration of the loop.
|
|
This invariant should mention every variable used in the loop.
|
|
Any other variable should also be mentioned in it. The loop \textit{variant} may also be added for proving termination.
|
|
A typical for-loop loop variant would be \texttt{n - x = Z}, or the same for a while loop like \texttt{while i < n do s end},
|
|
as the next value of the loop variant has to be lower than the previous one.
|
|
|
|
The preconditions and postconditions in the loops then reflect that the update to the loop variant variable(s) leads to them being smaller than $Z$,
|
|
which allows proving that the loop variant is decreasing, signifying that the loop terminates \textit{eventually}.
|
|
Of course, if \texttt{x} is decreasing, it itself can become the variant, as it fulfils the condition.
|
|
|
|
Proof outlines work by providing post and pre-condition for each sub-statement in a statement.
|
|
If we need to rewrite a statement (e.g. before the first loop body to change to our loop invariant from the overall precondition),
|
|
we use the $\models$ symbol.
|