diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.pdf b/semester4/fmfp/formal-methods-functional-programming-summary.pdf index b1994b5..c4f5af5 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/parts/04_language-semantics/00_imp/02_properties.tex b/semester4/fmfp/parts/04_language-semantics/00_imp/02_properties.tex index 0e71782..e42c19e 100644 --- a/semester4/fmfp/parts/04_language-semantics/00_imp/02_properties.tex +++ b/semester4/fmfp/parts/04_language-semantics/00_imp/02_properties.tex @@ -43,7 +43,7 @@ For Boolean Expressions And finally for Statements: \begin{align*} FV(\texttt{skip}) & = \varnothing \\ - FV(x := e) & = \{ x \} \cup FV(s_2) \\ + FV(x := e) & = \{ x \} \cup FV(e) \\ FV(s_1; s_2) & = FV(s_1) \cup FV(s_2) \\ FV(\texttt{if}\; b\; \texttt{then} \; s_1 \; \texttt{else} \; s_2 \; \texttt{end}) & = FV(b) \cup FV(s_1) \cup FV(s_2) \\ FV(\texttt{while}\; b\; \texttt{do} \; s \; \texttt{end}) & = FV(b) \cup FV(s) diff --git a/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/06_deterministic-semantics.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/06_deterministic-semantics.tex index 1e348a0..168dc60 100644 --- a/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/06_deterministic-semantics.tex +++ b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/06_deterministic-semantics.tex @@ -7,7 +7,7 @@ The full proof for this is available on the slides for Formal Methods, pages 82 - 91 (Slide Deck 3, pages 27 - 40) In there, \bi{Induction on Derivation Trees} is used. -Similar like other induction proofs, we show that a property $P(T)$ holds for all derivation trees $T$, +Similar to other induction proofs, we show that a property $P(T)$ holds for all derivation trees $T$, we prove that $P(T)$ holds for an arbitrary derivation tree $T$ under the assumption (the induction hypothesis) that $P(T')$ holds for all sub-trees $T'$ of $T$ This kind of induction is a special case of \bi{well-founded (Noetherian) induction}. diff --git a/semester4/fmfp/parts/06_exercises/01_fp/00_eval-strats.tex b/semester4/fmfp/parts/06_exercises/01_fp/00_eval-strats.tex index 49c6d71..39d3177 100644 --- a/semester4/fmfp/parts/06_exercises/01_fp/00_eval-strats.tex +++ b/semester4/fmfp/parts/06_exercises/01_fp/00_eval-strats.tex @@ -1,6 +1,6 @@ \subsubsection{Evaluation strategies} \begin{examdetails} - It is likely that one such task will appear. + It is not very likely that one such task will appear. \end{examdetails} Evaluation strategies formalize how programming languages evaluate the code. Most of the commonly used programming languages use \textit{eager evaluation}, whereas functional programming languages tend to prefer \textit{lazy evaluation} diff --git a/semester4/fmfp/parts/06_exercises/01_fp/01_haskell.tex b/semester4/fmfp/parts/06_exercises/01_fp/01_haskell.tex index 39814e3..313484d 100644 --- a/semester4/fmfp/parts/06_exercises/01_fp/01_haskell.tex +++ b/semester4/fmfp/parts/06_exercises/01_fp/01_haskell.tex @@ -1,6 +1,6 @@ \subsubsection{Haskell} \begin{examdetails} - typically either short coding task or proof of program + Typically one large coding task (split up into many subtasks) and proof of program \end{examdetails} \paragraph{Programming} diff --git a/semester4/fmfp/parts/06_exercises/01_fp/02_natural-deduction.tex b/semester4/fmfp/parts/06_exercises/01_fp/02_natural-deduction.tex index f4da7bc..e9b1cfe 100644 --- a/semester4/fmfp/parts/06_exercises/01_fp/02_natural-deduction.tex +++ b/semester4/fmfp/parts/06_exercises/01_fp/02_natural-deduction.tex @@ -1,5 +1,8 @@ \newpage \subsubsection{Natural Deduction} +\begin{examdetails} + From time to time there is one such task, has become more common in recent times. Inference rules are provided +\end{examdetails} \paragraph{Parenthesis} This task (if it were to even ever appear in the exams) is simply applying precedences, as well as remembering associativity. The precedences are as follows: diff --git a/semester4/fmfp/parts/06_exercises/01_fp/03_type-inference.tex b/semester4/fmfp/parts/06_exercises/01_fp/03_type-inference.tex index dcbce15..887aceb 100644 --- a/semester4/fmfp/parts/06_exercises/01_fp/03_type-inference.tex +++ b/semester4/fmfp/parts/06_exercises/01_fp/03_type-inference.tex @@ -2,6 +2,7 @@ \begin{examdetails} There typically is one such task. They provide the inference rules \end{examdetails} + The proof trees are again drawn up bottom up, applying rules from the outside in. \begin{enumerate} \item Create a proof tree using the typing rules. 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 2b9292a..6de526f 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,4 +1,7 @@ \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. 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 2868d3a..37e6401 100644 --- a/semester4/fmfp/parts/06_exercises/02_fm/03_modelling.tex +++ b/semester4/fmfp/parts/06_exercises/02_fm/03_modelling.tex @@ -1,4 +1,7 @@ \subsubsection{Modelling} +\begin{examdetails} + Has appeared from time to time in exams +\end{examdetails} 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. 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 58199b8..14cbd38 100644 --- a/semester4/fmfp/parts/06_exercises/02_fm/04_ltl.tex +++ b/semester4/fmfp/parts/06_exercises/02_fm/04_ltl.tex @@ -1,5 +1,9 @@ \newpage \subsubsection{Linear Time Properties (LTL)} +\begin{examdetails} + Has appeared in most exams over the last 10 years. + Typically a task where you provide an LTL formula, one where you show correctness / counterexamples for one and one on Liveness/Safety Properties +\end{examdetails} We refer to Section~\ref{sec:ltl} for intuition, as these tend to mostly be intuition exercises. For doing verification of liveness / safety properties using \texttt{spin} and Promela,