[FMFP] Mostly finish exercises section

semester4/fmfp/formal-methods-functional-programming-summary.tex

@@ -81,6 +81,9 @@
 \input{parts/01_induction-proofs/02_structural-induction.tex}
 \input{parts/01_induction-proofs/03_induction-on-trees.tex}
 \input{parts/01_induction-proofs/04_other-induction.tex}
+\input{parts/01_induction-proofs/05_induction-on-proof-trees.tex}
+\input{parts/01_induction-proofs/06_induction-on-derivation-sequence.tex}
+\input{parts/01_induction-proofs/07_workflow.tex}
 % \input{parts/01_induction-proofs/}
 
 \newsection
@@ -178,6 +181,7 @@
 For induction proofs, see Section~\ref{sec:induction-proofs}, which were moved up, since they are used in both FP and FM,
 as well as being mentioned a few times in the rest of the summary.
 
+\newpage
 \subsection{Formal Methods}
 \input{parts/06_exercises/02_fm/00_imp.tex}
 \input{parts/06_exercises/02_fm/01_operational-semantics.tex}
@@ -187,6 +191,7 @@ as well as being mentioned a few times in the rest of the summary.
 % \input{parts/06_exercises/02_fm/}
 % \input{parts/06_exercises/}
 
+\newpage
 \input{parts/06_exercises/03_checklist.tex}
 
 

semester4/fmfp/parts/01_induction-proofs/05_induction-on-proof-trees.tex

@@ -0,0 +1,31 @@
+\subsection{Induction on Proof Trees}
+\label{sec:induction-on-proof-trees}
+This type of induction is used to prove that a statement exhibits given behaviour.
+Since often, we are not restricted to just simple statements, such where we know that we are applying the $\textsc{Ass}_{\text{NS}}$ rule,
+we need to perform case distinction on all possible last rules applied in the derivation tree $T$.
+If all are to be proven, this will yield $7$, one for each rule of the big-step semantics.
+
+\inlinedefinition[Subderivation] We define $T' \sqsubset T$, where $T$ is a derivation tree. $T'$ is called a \textit{subderivation} of $T$,
+or more simply, a \textit{subtree} of $T$. Definition is analogous to the subterm relation.
+
+
+\shade{ForestGreen}{Rundown} Below a rundown of how such proofs are expected to be laid out.
+
+We define $P(T) \equiv \forall \sigma, \sigma', s . (\texttt{root}(T) \equiv \text{statement})$.
+The quantifier-bound variables / states / statements can of course differ, so adjust accordingly.
+This step is the crucial step to setting up this type of induction.
+
+We then prove $\forall T . P(T)$ by strong induction on the shape of the derivation tree $T$.
+Thus, for some arbitrary $T$, the induction hypothesis is $\forall T' \sqsubset T . P(T')$ and we prove $P(T)$.
+
+Let $\sigma, \sigma', s$ (and more, if applicable) be arbitrary.
+
+Then, for rules, such as $\textsc{WhT}_{\text{NS}}$, we draw up a derivation tree, like so (from solutions of Exercise Session 11, FS2026):
+\begin{center}
+    \includegraphics[width=0.6\linewidth]{assets/proof-on-shape-of-tree.png}
+\end{center}
+After it, we need to put final constraints and bind free variables in some way, e.g. here:
+
+For some $b, s', \sigma'', T_4, T_5$, such that $s \equiv \texttt{while}\; b \; \texttt{do} \; s' \; \texttt{end}$ and $\cB \llbracket b \rrbracket \sigma = \texttt{tt}$.
+
+Then use the induction hypothesis on the subderivations $T_i$ and finish the proof by showing the original statement holds under the induction hypothesis.

semester4/fmfp/parts/01_induction-proofs/06_induction-on-derivation-sequence.tex

@@ -0,0 +1,18 @@
+\newpage
+\subsection{Induction on Derivation Sequence}
+A finite derivation sequence has a length $n \in \N$.
+We typically reason about finite derivation sequences using \bi{strong induction on the length of a derivation sequence},
+i.e. we reason about a multi-step execution $\gamma \rightarrow_1^k \gamma'$ using strong induction on the number of steps $k$.
+
+We define $P(k) \equiv$ ``for all executions of length $k$, our property holds''
+
+We then prove $P(k)$ for arbitrary $k$, with induction hypothesis $\forall k' < k. P(k')$, as is usually the case with induction on natural numbers.
+
+After the setup, the proof \textit{typically} proceeds by case distinction on:
+\begin{itemize}
+    \item $k = 0$ step execution
+    \item $k > 0$ step execution, by splitting off the first execution (i.e. an execution $\langle s, \sigma \rangle \rightarrow_1^k \sigma''$
+        can be split up as $\langle s, \sigma \rangle \rightarrow_1^1 \gamma \rightarrow_1^{k - 1} \sigma''$.)
+\end{itemize}
+In the $k > 0$ case, we can then apply the induction hypothesis. Sometimes a further case distinction can become necessary, depending on the rules that are possible.
+For instance, if $s = s_1; s_2$, two rules are possible, \textsc{Seq1} and \textsc{Seq2} from the SOS.

semester4/fmfp/parts/05_modelling/02_linear-temporal-logic/00_linear-time-properties.tex

@@ -1,6 +1,7 @@
 % TOOD: Some more intuition
 \newpage
 \subsection{Linear Temporal Logic}
+\label{sec:ltl}
 \subsubsection{Transition System of a Promela Model}
 For the transition systems, compared to earlier, we use a fixed initial configuration because we only model one program or system,
 as opposed to all programs of a programming language, as previously.

semester4/fmfp/parts/06_exercises/02_fm/00_imp.tex

@@ -1 +1,9 @@
-\subsubsection{IMP}
+\subsubsection{IMP Proofs}
+\begin{examdetails}
+    Typically, the exam contains some operational semantics tasks,
+    rarely proofs of properties of IMP.
+\end{examdetails}
+The property proofs can be acheived either using a direct proof of the implication, or using an induction proof.
+The latter of which is more common and we typically define $P$ in such a way that we bind everything apart from variables, natural numbers and constant values
+using quantifiers, then prove $\forall n \in \N . P(n)$, if we have a free natural numbers.
+Before the definition of $P$ we typically state ``Let $<$variables, constants$>$ be arbitrary'', as with any induction proof.

semester4/fmfp/parts/06_exercises/02_fm/01_operational-semantics.tex

@@ -1,5 +1,34 @@
 \subsubsection{Operational Semantics}
-\paragraph{Big Step Semantics}
+\paragraph{Big Step Semantics (Natural Semantics, NS)}
+Proving something using the big step semantics rules tends to be fairly easy if you understand how natural deduction and the like work.
+The concept is very similar, just with other rules. It is advisable to name each sub-statement in the main statement, to reduce the required amount writing.
+
+Sometimes, Induction on (the shape of) Proof Trees may be required, for that, see Section~\ref{sec:induction-on-proof-trees}
+
+Where it gets more interesting and challenging, is providing rules in the big step semantics.
+Here, it is important to think about the different cases that could be introduced by the statement.
+
+For instance, for loops, there will (almost certainly) be two cases, one in which some boolean expression (denoted $\cB \llbracket e \rrbracket \sigma$) is \texttt{ff},
+the other in which it is \texttt{tt}.
+For these, you need to make sure to state the side condition (i.e. that the boolean expression is true or false, respectively).
+
+In addition, think thoroughly about how to define the states of the rules. For instance, for a \texttt{time} statement, that counts the number of assignments,
+the state we map to would ideally be defined as $\sigma' [x \mapsto n]$, where $n$ is the number of assignments.
 
 
-\paragraph{Small Step Semantics}
+\paragraph{Small Step Semantics (Structural Operational Semantics, SOS)}
+Small Step semantics proofs tend to be a bit more challenging. Unlike Natural Semantics, here we can't create a single derivation tree, but one per step.
+This means, that we do one single step transition at a time, denoted $\rightarrow_1^1$, and justify each step with a proof tree and SO Semantics (SOS).
+Typically, only \textit{some} of the statements are asked to be proven in the exam, as proving all is time intensive due to the typically fairly
+large number of steps in the proofs.
+For the proof trees, they need to be complete for each transition that we prove, i.e. no hypothesis in any branches.
+
+Defining rules here is similar in concept as with the Natural Semantics.
+We want to make sure, to also consider the effects it has on other rules, as with Natural Semantics.
+
+The sole difference here is that we return \textit{both} the next statement to be evaluated \textit{and} the next state,
+unlike with Natural Semantics, where we only return the next state.
+
+
+\paragraph{Other proofs}
+Induction proofs for these two are also outlined in Section~\ref{sec:induction-on-proof-trees} and subsequent subsections.

semester4/fmfp/parts/06_exercises/02_fm/02_axiomatic-semantics.tex

@@ -1 +1,11 @@
 \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}, as the next value of the loop variant has to be lower than the previous one.
+Of course, if \texttt{x} is decreasing, it itself can become the variant, as it fulfils the condition.

semester4/fmfp/parts/06_exercises/02_fm/03_modelling.tex

@@ -1 +1,12 @@
 \subsubsection{Modelling}
+Many of the tasks here are pretty straight forward, converting IMP into Promela,
+and putting an \texttt{assert} (or more) into the \texttt{init} block, to check if the required state is reached.
+
+Note that for non-determinism, we use Promela conditionals without conditions.
+
+For parallelism, we can use the \texttt{run} keyword for a \texttt{proctype}, then we wait for the processes to terminate using
+\texttt{\_nr\_pr == 1} and do our assertion.
+
+
+If we are given a text description only however, things get more challenging, as we need to model the properties given there.
+A possible simplification of the process may be to model things one property at a time, then combine them as needed.

semester4/fmfp/parts/06_exercises/02_fm/04_ltl.tex

@@ -1 +1,2 @@
 \subsubsection{Linear Time Properties (LTL)}
+We refer to Section~\ref{sec:ltl} for intuition, as these tend to mostly be intuition exercises.