diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.tex b/semester4/fmfp/formal-methods-functional-programming-summary.tex index e895674..a82d822 100644 --- a/semester4/fmfp/formal-methods-functional-programming-summary.tex +++ b/semester4/fmfp/formal-methods-functional-programming-summary.tex @@ -75,6 +75,7 @@ \newsection \section{Induction Proofs} +\label{sec:induction-proofs} \input{parts/01_induction-proofs/00_intro.tex} \input{parts/01_induction-proofs/01_mathematical-induction.tex} \input{parts/01_induction-proofs/02_structural-induction.tex} @@ -161,5 +162,30 @@ % \input{parts/05_modelling/} +\newsection +\section{Exercises} +\subsection{Introduction} +\input{parts/06_exercises/00_intro.tex} + +\subsection{Functional Programming} +\input{parts/06_exercises/01_fp/00_eval-strats.tex} +\input{parts/06_exercises/01_fp/01_haskell.tex} +\input{parts/06_exercises/01_fp/02_natural-deduction.tex} +\input{parts/06_exercises/01_fp/03_type-inference.tex} +% \input{parts/06_exercises/01_fp/} + +\subsection{Induction} +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. + +\subsection{Formal Methods} +\input{parts/06_exercises/02_fm/00_imp.tex} +\input{parts/06_exercises/02_fm/01_operational-semantics.tex} +\input{parts/06_exercises/02_fm/02_axiomatic-semantics.tex} +\input{parts/06_exercises/02_fm/03_modelling.tex} +\input{parts/06_exercises/02_fm/04_ltl.tex} +% \input{parts/06_exercises/02_fm/} +% \input{parts/06_exercises/} + \end{document} diff --git a/semester4/fmfp/parts/06_exercises/00_intro.tex b/semester4/fmfp/parts/06_exercises/00_intro.tex new file mode 100644 index 0000000..5dad278 --- /dev/null +++ b/semester4/fmfp/parts/06_exercises/00_intro.tex @@ -0,0 +1,6 @@ +This section aims to give you an overview over how to solve different exercise types. +An understanding of the rest of the topics covered in the lecture is expected, as well as understanding of haskell. +There is a short section on haskell in this section, too. + +FMFP is known to feature an exam where time is at a premium, so the most important preparation likely is solving as many old exams as you can, +to really get fast at solving the exercises in there, as the exams have been following a similar format, with predictable exercise types, for a long time. 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 new file mode 100644 index 0000000..d91a43b --- /dev/null +++ b/semester4/fmfp/parts/06_exercises/01_fp/00_eval-strats.tex @@ -0,0 +1,10 @@ +\subsubsection{Evaluation strategies} +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} + +\paragraph{Lazy Evaluation} +In Lazy Evaluation, expressions are substituted until all possible values are substituted and the expression is then evaluated. + +At the exam, it is likely that one such task will appear. + +\paragraph{Eager 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 new file mode 100644 index 0000000..e69de29 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 new file mode 100644 index 0000000..e69de29 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 new file mode 100644 index 0000000..e69de29 diff --git a/semester4/fmfp/parts/06_exercises/02_fm/00_imp.tex b/semester4/fmfp/parts/06_exercises/02_fm/00_imp.tex new file mode 100644 index 0000000..e69de29 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 new file mode 100644 index 0000000..e69de29 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 new file mode 100644 index 0000000..e69de29 diff --git a/semester4/fmfp/parts/06_exercises/02_fm/03_modelling.tex b/semester4/fmfp/parts/06_exercises/02_fm/03_modelling.tex new file mode 100644 index 0000000..e69de29 diff --git a/semester4/fmfp/parts/06_exercises/02_fm/04_ltl.tex b/semester4/fmfp/parts/06_exercises/02_fm/04_ltl.tex new file mode 100644 index 0000000..e69de29