diff --git a/semester4/fmfp/assets/proof-on-shape-of-tree.png b/semester4/fmfp/assets/proof-on-shape-of-tree.png new file mode 100644 index 0000000..07c260b Binary files /dev/null and b/semester4/fmfp/assets/proof-on-shape-of-tree.png differ diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.pdf b/semester4/fmfp/formal-methods-functional-programming-summary.pdf index 405b061..f8f924a 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 cad04a9..da1dc39 100644 --- a/semester4/fmfp/formal-methods-functional-programming-summary.tex +++ b/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} diff --git a/semester4/fmfp/parts/01_induction-proofs/05_induction-on-proof-trees.tex b/semester4/fmfp/parts/01_induction-proofs/05_induction-on-proof-trees.tex new file mode 100644 index 0000000..2e9d864 --- /dev/null +++ b/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. diff --git a/semester4/fmfp/parts/01_induction-proofs/06_induction-on-derivation-sequence.tex b/semester4/fmfp/parts/01_induction-proofs/06_induction-on-derivation-sequence.tex new file mode 100644 index 0000000..2f320b5 --- /dev/null +++ b/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. diff --git a/semester4/fmfp/parts/01_induction-proofs/05_workflow.tex b/semester4/fmfp/parts/01_induction-proofs/07_workflow.tex similarity index 100% rename from semester4/fmfp/parts/01_induction-proofs/05_workflow.tex rename to semester4/fmfp/parts/01_induction-proofs/07_workflow.tex 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 5207be0..fb2eda7 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 @@ -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. diff --git a/semester4/fmfp/parts/06_exercises/02_fm/00_imp.tex b/semester4/fmfp/parts/06_exercises/02_fm/00_imp.tex index 96c45a9..d525d3e 100644 --- a/semester4/fmfp/parts/06_exercises/02_fm/00_imp.tex +++ b/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. diff --git a/semester4/fmfp/parts/06_exercises/02_fm/01_operational-semantics.tex b/semester4/fmfp/parts/06_exercises/02_fm/01_operational-semantics.tex index b7e1975..9be88bd 100644 --- a/semester4/fmfp/parts/06_exercises/02_fm/01_operational-semantics.tex +++ b/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. diff --git a/semester4/fmfp/parts/06_exercises/02_fm/02_axiomatic-semantics.tex b/semester4/fmfp/parts/06_exercises/02_fm/02_axiomatic-semantics.tex index 5704294..56cc883 100644 --- a/semester4/fmfp/parts/06_exercises/02_fm/02_axiomatic-semantics.tex +++ b/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. diff --git a/semester4/fmfp/parts/06_exercises/02_fm/03_modelling.tex b/semester4/fmfp/parts/06_exercises/02_fm/03_modelling.tex index ec73bfa..5f181b4 100644 --- a/semester4/fmfp/parts/06_exercises/02_fm/03_modelling.tex +++ b/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. diff --git a/semester4/fmfp/parts/06_exercises/02_fm/04_ltl.tex b/semester4/fmfp/parts/06_exercises/02_fm/04_ltl.tex index 0b85fbb..6d43903 100644 --- a/semester4/fmfp/parts/06_exercises/02_fm/04_ltl.tex +++ b/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.