[FMFP] Final remarks and fixes

2026-09-10 13:05:24 +02:00 · 2026-08-06 15:10:54 +02:00
parent dad7286f10
commit 7cdba7dca9
10 changed files with 18 additions and 4 deletions
@@ -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)
@@ -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}.
@@ -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}
@@ -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}
@@ -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:
@@ -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.
@@ -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.
@@ -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.

@@ -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,