diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.pdf b/semester4/fmfp/formal-methods-functional-programming-summary.pdf index ec78e9e..517d2b3 100644 Binary files a/semester4/fmfp/formal-methods-functional-programming-summary.pdf and b/semester4/fmfp/formal-methods-functional-programming-summary.pdf differ diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.tex b/semester4/fmfp/formal-methods-functional-programming-summary.tex index 9be707c..e895674 100644 --- a/semester4/fmfp/formal-methods-functional-programming-summary.tex +++ b/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} diff --git a/semester4/fmfp/parts/01_induction-proofs/02_structural-induction.tex b/semester4/fmfp/parts/01_induction-proofs/02_structural-induction.tex index 1edbc48..bedac4a 100644 --- a/semester4/fmfp/parts/01_induction-proofs/02_structural-induction.tex +++ b/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*} diff --git a/semester4/fmfp/parts/01_induction-proofs/03_induction-on-trees.tex b/semester4/fmfp/parts/01_induction-proofs/03_induction-on-trees.tex index 9c034af..7a2dea5 100644 --- a/semester4/fmfp/parts/01_induction-proofs/03_induction-on-trees.tex +++ b/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$ diff --git a/semester4/fmfp/parts/01_induction-proofs/04_other-induction.tex b/semester4/fmfp/parts/01_induction-proofs/04_other-induction.tex index 7ca3fec..3a66f73 100644 --- a/semester4/fmfp/parts/01_induction-proofs/04_other-induction.tex +++ b/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]$ - - diff --git a/semester4/fmfp/parts/04_language-semantics/02_axiomatic-semantics/01_hoare-logic/00_triples-assertions.tex b/semester4/fmfp/parts/04_language-semantics/02_axiomatic-semantics/01_hoare-logic/00_triples-assertions.tex index 8ffd66f..50d4efc 100644 --- a/semester4/fmfp/parts/04_language-semantics/02_axiomatic-semantics/01_hoare-logic/00_triples-assertions.tex +++ b/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$ diff --git a/semester4/fmfp/parts/05_modelling/00_intro.tex b/semester4/fmfp/parts/05_modelling/00_intro.tex index 9f76c87..7c9fc27 100644 --- a/semester4/fmfp/parts/05_modelling/00_intro.tex +++ b/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 .pml}, +In the case of this course, we use \texttt{spin}, and we can run a Promela model using \texttt{spin -x .pml}, which wraps \texttt{spin -a .pml}, \texttt{gcc .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. diff --git a/semester4/fmfp/parts/05_modelling/01_promela/00_syntax.tex b/semester4/fmfp/parts/05_modelling/01_promela/00_syntax.tex index 5a1106d..8703791 100644 --- a/semester4/fmfp/parts/05_modelling/01_promela/00_syntax.tex +++ b/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} diff --git a/semester4/fmfp/parts/05_modelling/02_linear-temporal-logic/00_linear-time-properties.tex b/semester4/fmfp/parts/05_modelling/02_linear-temporal-logic/00_linear-time-properties.tex index 7d23cdb..5207be0 100644 --- a/semester4/fmfp/parts/05_modelling/02_linear-temporal-logic/00_linear-time-properties.tex +++ b/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$. diff --git a/semester4/fmfp/parts/05_modelling/02_linear-temporal-logic/01_linear-temporal-logic.tex b/semester4/fmfp/parts/05_modelling/02_linear-temporal-logic/01_linear-temporal-logic.tex index c04a3fb..ea0c325 100644 --- a/semester4/fmfp/parts/05_modelling/02_linear-temporal-logic/01_linear-temporal-logic.tex +++ b/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}