[FMFP] First rework complete

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

@@ -32,6 +32,7 @@
 
 \begin{document}
 \startDocument
+\mediumverticalspacing
 
 \vspace{1cm}
 \begin{center}
@@ -53,8 +54,10 @@
     FS2026, ETHZ
 
     \begin{Large}
-        Summary of the Lectures
+        Summary of the Lecture Slides
     \end{Large}
+
+    \url{https://infsec.ethz.ch/education/ss2026/fmfp.html}
 \end{center}
 
 

semester4/fmfp/parts/01_induction-proofs/02_structural-induction.tex

@@ -1,19 +1,27 @@
 \subsection{Structural Induction}
+In this subsection, we present structural induction over lists.
+The same concept also applies similarly to trees and more.
+Weak Structural Induction on treees is presented in the subsequent subsection.
+
+For both, we only provide the natural deduction rules, as the proofs proceed analogously to the ones for mathematical induction.
+
 \subsubsection{Weak Structural Induction}
-Induction is based on the structure of terms
-\mint{haskell}+data T t = Leaf t | Node1 (T t) | Node2 t (T t) (T t)+
-
-\shade{blue}{Base Case} $T_0 = \{ \texttt{Leaf}\ a \divider a \in t \}$
-
-\shade{green}{Step Case} $T_i = T_{i - 1} \cup \{ \texttt{Node1}\ s \divider s \in T_{i - 1} \} \cup \{ \texttt{Node2}\ a\ l\ r \divider a \in t \text{ and } l, r \in T_{i - 1} \}$
-
-A natural deduction rule structural induction is:
 \[
     \begin{prooftree}
-        \hypo{\Gamma \vdash P[x \mapsto \texttt{Leaf}\ a]}
-        \hypo{\Gamma, P[x \mapsto s] \vdash P[xs \mapsto \texttt{Node1}\ s]}
-        \hypo{\Gamma, P[x \mapsto l], P[x \mapsto r] \vdash P[ \mapsto \texttt{Node2}\ a\ l\ r]}
-        \infer3[$(*)$]{\Gamma \vdash \forall x \in \texttt{T}\ t. P}
+        \hypo{\Gamma \vdash P(\texttt{[]})}
+        \hypo{\Gamma, P(\texttt{xs}) \vdash P(\texttt{x : xs})}
+        \infer2[where \texttt{x}, \texttt{xs} not free in $\Gamma$]{\Gamma \vdash \forall \texttt{xs} . P(\texttt{xs})}
     \end{prooftree}
 \]
-(*) $a$, $l$, $r$, $s$ not free in $\Gamma, P$
+
+\subsubsection{Strong Structural Induction}
+\inlinedefinition[Subterm relation] denoted $\sqsubset$ is defined as follows:
+\[
+    \forall xs, ys . xs \sqsubset ys \Leftrightarrow (\exists x. ys = x:xs) \lor (\exists zs . xs \sqsubset zs \land zs \sqsubset ys)
+\]
+\begin{align*}
+    \begin{prooftree}
+        \hypo{\Gamma, \forall ys \sqsubset xs . P(ys) \vdash P(xs)}
+        \infer1[$xs$ not free in $\Gamma$, $ys$ not free in $P(xs)$]{\Gamma \vdash \forall xs . P(xs)}
+    \end{prooftree}
+\end{align*}

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

@@ -1 +1,17 @@
 \subsection{Induction on Trees}
+\mint{haskell}+data T t = Leaf t | Node1 (T t) | Node2 t (T t) (T t)+
+
+\shade{blue}{Base Case} $T_0 = \{ \texttt{Leaf}\ a \divider a \in t \}$
+
+\shade{green}{Step Case} $T_i = T_{i - 1} \cup \{ \texttt{Node1}\ s \divider s \in T_{i - 1} \} \cup \{ \texttt{Node2}\ a\ l\ r \divider a \in t \text{ and } l, r \in T_{i - 1} \}$
+
+A natural deduction rule structural induction is:
+\[
+    \begin{prooftree}
+        \hypo{\Gamma \vdash P[x \mapsto \texttt{Leaf}\ a]}
+        \hypo{\Gamma, P[x \mapsto s] \vdash P[xs \mapsto \texttt{Node1}\ s]}
+        \hypo{\Gamma, P[x \mapsto l], P[x \mapsto r] \vdash P[ \mapsto \texttt{Node2}\ a\ l\ r]}
+        \infer3[$(*)$]{\Gamma \vdash \forall x \in \texttt{T}\ t. P}
+    \end{prooftree}
+\]
+(*) $a$, $l$, $r$, $s$ not free in $\Gamma, P$

semester4/fmfp/parts/01_induction-proofs/04_other-induction.tex

@@ -7,5 +7,3 @@ To prove $P$ for all $xs$ in \texttt{[T]}, we do the following:
 \shade{green}{Step case} We prove that $\forall y :: T, ys :: [T]. P[xs \mapsto ys] \rightarrow P[xs \mapsto y : ys]$, or in other words:
 We fix arbitrary $y :: T$ and $ys :: [T]$, which both are not free in $P$.
 We then apply our induction hypothesis $P[xs \mapsto ys]$ to prove $P[xs \mapsto y : ys]$
-
-

semester4/fmfp/parts/04_language-semantics/02_axiomatic-semantics/01_hoare-logic/00_triples-assertions.tex

@@ -14,4 +14,4 @@ still holds:
     \cB \llbracket \bm{P}[x \mapsto e] \rrbracket \sigma = \cB \llbracket \bm{P} \rrbracket \sigma [x \mapsto \cA \llbracket e \rrbracket \sigma]
 \]
 
-We use $P_1 \land P_2$ instead of $P_1 \texttt{and} P_2$, $P_1 \lor P_2$ instead of $P_1 \texttt{or} P_2$ and $\neg P$ instead of $\texttt{not} P$
+We use $P_1 \land P_2$ instead of $P_1 \; \texttt{and} \; P_2$, $P_1 \lor P_2$ instead of $P_1 \; \texttt{or} \; P_2$ and $\neg P$ instead of $\texttt{not}\; P$

semester4/fmfp/parts/05_modelling/00_intro.tex

@@ -16,8 +16,8 @@ The first and most important phase is the \bi{modeling phase}, where we model th
 It also includes formalizing the properties to be checked in said language.
 
 Next, we run the model checker to check the validity of the model. 
-In the case of this course, we use \texttt{spin}, and we can run a promela model using \texttt{spin -x <promela file>.pml},
+In the case of this course, we use \texttt{spin}, and we can run a Promela model using \texttt{spin -x <promela file>.pml},
 which wraps \texttt{spin -a <promela file>.pml}, \texttt{gcc <promela file>.c} and \texttt{./a.out} into a single command.
 
-After running, it is time to analyze the output of the model checker. If the property is violated, analyze the found conter example.
-If the mdeol is too large, it can happen that the checker runs out of memory. In that case, reduce the model and try again.
+After running, it is time to analyze the output of the model checker. If the property is violated, analyze the found counter example.
+If the model is too large, it can happen that the checker runs out of memory. In that case, reduce the model and try again.

semester4/fmfp/parts/05_modelling/01_promela/00_syntax.tex

@@ -8,10 +8,13 @@ The number of states is given by
     \prod_{i = 1}^N (l(p_i) \times \prod_{\texttt{var} x_i \in p_i} |\texttt{dom}(x_i)|) \times \prod_{j = 1}^{K} |\texttt{dom}(c_j)|^{\texttt{cap}(c_j)}
 \]
 where $l(p_i)$ returns the number of program locations for process $i$, $|\texttt{dom}(x_i)|$ denotes the number of values a variable can take,
-$\texttt{dom}(c_j)$ denotes the number of values each message in the channel can take and $\texttt{cap}(c_j)$ returns the capacity of the buffer fo the channel.
+$\texttt{dom}(c_j)$ denotes the number of values each message in the channel can take and $\texttt{cap}(c_j)$ returns the capacity of the buffer of the channel.
+
 
 \shade{orange}{THUS:} \hl{Keep the model as small as possible} to prevent the above, which is called \bi{state space explosion}
 
+On the next page, the basic syntax of Promela is presented.
+
 \newpage
 
 \inputcode{promela}{code/promela/00_basics.pml}

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

@@ -65,7 +65,7 @@ The LT-Properties are typically specified over infinite sequences of abstract st
 \inlinedefinition An LT-property $P$ is a safety property if for all infinite sequences $t \in \cP(AP)^{\omega}$:
 if $t \notin P$ then there is a finite prefix $\hat{t}$ of $t$ such that for every $t'$ with prefix $\hat{t}$, $t \notin P$.
 
-\inlineintuition More informally, it \textit{does not allow anything bad to happen}. Or, more exhaustively, if a sequence $t$ is no allowed by the LT-property,
+\inlineintuition More informally, it \textit{does not allow anything bad to happen}. Or, more exhaustively, if a sequence $t$ is not allowed by the LT-property,
 then there exists a finite prefix $\hat{t}$, which contains everything that makes the sequence violate the LT-property.
 Thus, whatever sequence we append to it, it will always remain in violation of the property $P$.
 

semester4/fmfp/parts/05_modelling/02_linear-temporal-logic/01_linear-temporal-logic.tex

@@ -2,10 +2,10 @@
 This is used to formalize LT-properties of traces.
 
 \paragraph{Operators}
-The basic operators are, with $p$ a proposition from $AP \neq \emptyset$ and $\Phi$ and $\Psi$ LTL formulas:
+The basic operators are, with $p$ a proposition from $AP \neq \emptyset$, and $\Phi$ and $\Psi$ LTL formulas:
 \begin{itemize}
     \item $p$ states that it is true ``\textit{now}''
-    \item $\Phi U \Psi$ states that $\Phi$ holds ``\textit{until}'' $\Psi$ holds. I.e. there are no other valid propositions that hold in between.
+    \item $\Phi \; U \; \Psi$ states that $\Phi$ holds ``\textit{until}'' $\Psi$ holds. I.e. there are no other valid propositions that hold in between.
     \item $\bigcirc \Phi$ states that the $\Phi$ holds for the ``\textit{next}''
 \end{itemize}