\subsubsection{Axiomatic Semantics}
\begin{examdetails}
    Typically one task, accounting for a fairly large portion of points
\end{examdetails}
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.
Note that we want to describe each variable and for future assignments, we want to substitute all values with that assignments written out before
they actually happen, for instance if down the line, in the same scope, we have \texttt{n := n - 1}, we substitute all occurrences of $n$ with $n - 1$ and update things accordingly.

There are also tasks in which we need to find errors in rule applications. This works ``simply'' by checking that the rules are applied correctly
and semantic entailment and general transformation rules hold for the transformations.