eth-janishutz/eth-summaries
1
0
Fork 0
mirror of https://github.com/janishutz/eth-summaries.git synced 2026-07-27 21:29:09 +02:00
Code Issues Packages Projects Releases Wiki Activity

[FMFP] Remark on axiomatic semantics

Browse Source
This commit is contained in:
janishutz
2026-07-21 10:39:52 +02:00
parent 51da8be172
commit 0b98da10eb
1 changed files with 2 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
semester4/fmfp/parts/06_exercises/02_fm/02_axiomatic-semantics.tex
+2
View File
@@ -8,6 +8,8 @@ This typically involves finding a loop invariant that holds before and after eac
This invariant should mention every variable used in 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. 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}, as the next value of the loop variant has to be lower than the previous one. A typical for-loop loop variant would be \texttt{n - x = Z}, 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. 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. Proof outlines work by providing post and pre-condition for each sub-statement in a statement.