Merge pull request #6 from isaqb-org/dev

Merge dev branch

README.adoc

@@ -22,7 +22,8 @@ image:https://img.shields.io/github/issues-closed/isaqb-org/curriculum-fm.svg["I
 This is <<copyrighted,copyrighted work>>.
 
 == Content
-This repository contains the curriculum Formal Methods
+This repository contains the curriculum Formal Methods.  It is still
+in the early stages of development.
 
 toc::[]
 

docs/00b-basics/01-what-to-expect-of-this-module.adoc

@@ -8,13 +8,81 @@ Am Ende des Moduls kennen die Teilnehmerinnen und Teilnehmer … und können …
 // tag::EN[]
 === What does the module “{curriculum-short}” convey?
 
-The module presents {curriculum-short} to the participants …
-At the end of the module, the participants know … and are able to …
-// end::EN[]
+Among the responsibilities of a software architect is making sure that
+the architecture design is correctly refined and implemented, meaning
+that the implementation is architecturally compliant. On one hand, the
+implemented system should conform to the system’s software
+architecture, i.e. the interfaces, and the relationships defined in
+the software architecture. On the other hand, the models that describe
+the system functionality should be correct regarding the system
+requirements.
+
+Correctness seems self-evident as a requirement, but it rarely makes
+it into explicit design documents or design artifacts. Often,
+correctness is not directly applicable to the "messy" aspects of a
+software system which may have co-evolved with vaguely formulated
+requirements, where correctness is in the eye of the beholder. Yet
+some application domains require correctness of certain aspects of a
+system implementation with respect to its requirement
+specification. Examples include software applications that:
+
+* control mission-critical hardware,
+* secure highly sensitive pieces of information, or
+* make revenue-vital calculations.
+
+Traditional architecture focuses on producing a workable and
+maintainable system. Its functionality is assured through manual
+automated testing, which only operates on individual examples. These
+can, as the old adage goes, only show the presence, but not the
+absence of errors: Properties underlying the tests are not typically
+constructed systematically, and only a small part of the state space
+is covered.
+
+Thus, traditional software architecture and development methods are
+insufficient to ensure correctness as in the examples above. This
+curriculum intends to provide a collection of formal methods to
+supplement and replace the traditional architect's arsenal. These
+methods produce mathematical proofs of critical system
+properties. Note that such proof can not typically be produced as an
+afterthought to a system's architecture. Instead, the architecture
+needs to be designed from the start to be amenable to such
+proof. While designing and building systems that are amenable to
+various flavors of automated testing – such as unit, integration,
+acceptance, and property testing – is established practice and
+well-supported by common technology stacks, formal methods require a
+substantially higher effort to incorporate in a design. For instance,
+establishing a formal connection between specification and
+implementation requires a careful selection of specification and
+programming languages, respectively.
 
+To apply formal methods, architects need to formulate important
+properties of the software system mathematically, construct an
+architecture capable of ensuring these properties, and then proceed to
+verify them formally. Creating an architecture fit for verification
+requires careful consideration, and a high degree of architectural
+competency. In particular, architects need to:
+
+* choose appropriate properties to verify,
+* create verifiable models for the whole system under analysis as well
+  as for its components,
+* partition the system into verifiable components, and ensuring that
+  the component properties are composable into system properties,
+  which in turn are verified at system level
+* choose appropriate formal techniques and tools to verify the
+  properties
+* integrate verification into the software development process and
+  tool chain
+
+Software architects can employ these skills and techniques,
+particularly in early phases of the design of the system
+architecture. Formal verification methods are not only used to show
+correctness of architecture models regarding specific system
+requirements, their application can, in fact, be guided and directed
+by the functional system architecture itself. Relatedly, a strong
+focus on formal methods in system design may feed into better
+“traditional” testability, for example by the ability to automatically
+generate test cases, drastically increasing software quality while
+simultaneously increasing development.
+
+// end::EN[]
 
-[NOTE]
-====
-Hier bitte das Modul bzw. dessen Lerninhalte zusammenfassend in 5-8 Sätzen beschreiben. Dabei `{curriculum-name}`
-nicht entfernen, beim Zusammenbauen wird dieser Platzhalter mit dem Modulnamen ersetzt.
-====

docs/00b-basics/02-curriculum-structure-and-chronological-breakdown.adoc

@@ -24,24 +24,14 @@
 |===
 | Content
 | Recommended minimum duration (minutes)
-| 1. Introduction | 180
-| 2. xz | 150
-| 3. Lots of theory | 120
-| 4. xy and example | 180
-| 5. abc und d | 210
-| 6. Final example | 120
+| 1. <<Logic>> | 180
+| 2. <<Specification and Implementation>> | 300
+| 3. <<Formal Methods and the Development Process>> | 120
+| 4. <<Tools>> | 300
+| 5. <<{examples}>> | 180
 | |
-| Total | 960 (16h)
+| Total | 1080 (18h)
 
 |===
 
 // end::EN[]
-
-[NOTE]
-====
-Bitte die oben angegebene Tabelle entsprechend anpassen.
-
-= = =
-
-Please adjust the table above according to your curriculum.
-====

docs/00b-basics/03-timing-didactics-and-more.adoc

@@ -1,14 +1,8 @@
 
-[NOTE]
-====
-Bitte in dieser Datei nur die "**?**"-Platzhalter durch die Anzahl der Tage sowie die erreichbaren Punkte ersetzen. Ansonsten keine Änderungen vornehmen!
-====
-
-
-:recommended-duration-in-days: **?**
-:methodical-credits: **?**
-:technical-credits: **?**
-:communicative-credits: **?**
+:recommended-duration-in-days: **3**
+:methodical-credits: **10**
+:technical-credits: **10**
+:communicative-credits: **10**
 
 // tag::DE[]
 === Dauer, Didaktik und weitere Details

docs/00b-basics/04-prerequisites-for-this-training.adoc

@@ -21,20 +21,13 @@ Teilnehmerinnen und Teilnehmer **sollten** folgende Kenntnisse und/oder Erfahrun
 
 Participants **should** have the following prerequisite knowledge:
 
-- Prerequisite 1
-- Prerequisite 2, etc.
+- basic knowledge of algebra
+- basic knowledge of logic
 
 Knowledge in the following areas may be **helpful** for understanding some concepts:
 
-- Area 1:
-  * Knowledge 1
-  * Experience 2
-  * Knowledge 3
-  * Experience 4
-  * Understanding 5
-// end::EN[]
+- functional programming
+- equational reasoning over programs
+- programming-language semantics
 
-[NOTE]
-====
-Kenntnisgruppen sowie Voraussetzungen bitte entsprechend ausformulieren!
-====
+// end::EN[]

docs/01-module-block-1/00-structure.adoc

@@ -8,7 +8,7 @@
 // end::DE[]
 
 // tag::EN[]
-== This is the First Module's Title
+== Logic
 // end::EN[]
 
 

docs/01-module-block-1/01-duration-terms.adoc

@@ -10,20 +10,9 @@ Begriff 1, Begriff 2, Begriff 3
 
 // tag::EN[]
 |===
-| Duration: XXX min | Practice time: XXX min
+| Duration: 120 min | Practice time: 60 min
 |===
 
 === Terms and Principles
-Term 1, Term 2, Term 3
+formal system, logic, propositional logic, predicate logic, temporal logic, intuitionistic logic, classical logic, syntax, semantics, conjunction, disjunction, implication, quantifier, logical calculus, natural calculus, sequent calculus, deduction, inference, resolution
 // end::EN[]
-
-
-[NOTE]
-====
-Überschrift in 00-structure.adoc ersetzen
-====
-
-[NOTE]
-====
-Sinnvolle Zeiten für Dauer und Übungszeit eintragen, vernünftige Begriffe aufzählen.
-====

docs/01-module-block-1/02-learning-goals.adoc

@@ -16,11 +16,62 @@ wie wichtig einzelne Aspekte des Lernziels sind. Es kann hier bereits auf Litera
 
 // tag::EN[]
 [[LG-1-1]]
-==== LG 1-1: The is the first learning goal, in category xy
-tbd.
+==== LG 1-1: Propositional Logic
+Know the basic structure of propositional logic:
+
+* (atomic) propositions and their syntax
+* logical connectives such as conjunction
+* Conjunctive and disjunctive normal forms
+* Semantics of propositions
+* Meta-logical concepts of models, validity, satisfiability, and equivalence
+* Decidability of propositional logic
+
+[[LG-1-2]]
+==== LG 1-2: Predicate Logic
+
+Know the basic structure of predicate/first-order logic:
+
+* terms and their syntactic structure (variables, functions)
+* formulas and their syntactic structure (predicates, quantifiers)
+* predicate logic as an extension of propositional logic
+* Non-trivial syntactic operations on formulas
+** renaming and substitution, avoiding variable capture
+** skolemization and equisatisfiability
+** quantifier elimination
+* Semantics of first-order formulas
+** structures comprising universes and interpretations
+** coincidence of structures
+** extension with equality
+* semi-decidability of predicate logic
+
+[[LG-1-3]]
+==== LG 1-3: Temporal Logic
+
+Know the basic structure of temporal operators:
+
+* eventually and forever
+* Different logics and interpretations, for example LTL vs. CTL
+* Connection to automata
+
+[[LG-1-4]]
+==== LG 1-4: Logical Calculi
+
+Understand the basic concepts of a logical calculus:
+
+* Inference rules operating on syntactic structure of a formula
+* Different characteristics regarding supported fragments and runtime complexity
+* Completeness vs. refutation completeness
+* Natural deduction
+* Sequent calculus
+* Resolution
 // end::EN[]
 
-[NOTE]
-====
-Die einzelnen Lernziele müssen nicht als einfache Aufzählungen mit Unterpunkten aufgeführt werden, sondern können auch gerne in ganzen Sätzen formuliert werden, welche die einzelnen Punkte (sofern möglich) integrieren.
-====
+[[LG-1-5]]
+==== LG 1-5: Intuitionistic vs. Classical Logic
+
+Understand the difference between intuitionistic and
+classical logic:
+
+* Constructive vs. non-constructive proofs
+* Axioms and inferences only admissible in classical logic (LEM, double negation elimination)
+* Correspondence of intuitionistic logic to programmign and type systems

docs/01-module-block-1/references.adoc

@@ -1,14 +1,3 @@
 === {references}
 
-<<bass>>, <<bachmann>>, <<kruchten>>, <<starke>>
-
-
-
-[NOTE]
-====
-Eine Quelle wird über `\<<label>>` referenziert. Dieses muss in `99-references/00-references.adoc` definiert sein.
-
-= = =
-
-A reference source is referenced via `\<<label>>`. The label has to be defined in `99-references/00-references.adoc`.
-====
+<<schoening2008>>, <<troelstra2012>>, <<harrison2009>>, <<fitting1996>>, <<enderton2001>>, <<ebbinghaus2021>>, <<gallier2015>>

docs/02-module-block-2/00-structure.adoc

@@ -7,7 +7,7 @@
 // end::DE[]
 
 // tag::EN[]
-== Here's the Title of the Second Lesson
+== Specification and Implementation
 // end::EN[]
 
 include::01-duration-terms.adoc[{include_configuration}]

docs/02-module-block-2/01-duration-terms.adoc

@@ -11,20 +11,12 @@ Begriff 1, Begriff 2, Begriff 3
 
 // tag::EN[]
 |===
-| Duration: XXX min | Practice time: XXX min
+| Duration: 200 min | Practice time: 100 min
 |===
 
 === Terms and Principles
-Term 1, Term 2, Term 3
 
-// end::EN[]
-
-[NOTE]
-====
-Überschrift in 00-structure.adoc ersetzen
-====
+specification, property, formal specification, mechanized
+specification, specification language, refinement, model
 
-[NOTE]
-====
-Sinnvolle Zeiten für Dauer und Übungszeit eintragen, vernünftige Begriffe aufzählen.
-====
+// end::EN[]

docs/02-module-block-2/02-learning-goals.adoc

@@ -19,16 +19,61 @@ tbd.
 
 // tag::EN[]
 [[LG-2-1]]
-==== LG 2-1: TBD
-tbd.
+==== LG 2-1: Notions of specification
+
+* Know different notions of specification, specifically:
+
+** examples
+** properties
+** formal
+** mechanized
+
+* Understand that specification may pertain to different kinds of
+  components, such as:
+
+** functions
+** data types
+** algorithms
+** systems
+
+* Understand that specifications may pertain to different
+  qualities, such as:
+
+** functionality
+** performance effiicency
+** security
+** safety
 
 [[LG-2-2]]
-==== LG 2-2: TBD
-tbd.
-// end::EN[]
+==== LG 2-2: Formal Specifications
+
+* Understand that applying formal methods requires formal
+  specifications.
 
-[NOTE]
-====
-Die einzelnen Lernziele müssen nicht als einfache Aufzählungen mit Unterpunkten aufgeführt werden, sondern können auch gerne in ganzen Sätzen formuliert werden, welche die einzelnen Punkte (sofern möglich) integrieren.
-====
+* Understand that formal specifications involve universal
+  quantifiers rather than just examples for desired behavior.
+
+* Understand the difference between functional properties
+  that admit only one output per input, and relational properties that
+  admit multiple outputs per input.
+
+[[LG-2-3]]
+==== LG 2-3: Specification Languages
+
+* Know that many different specification languages exist,
+  among them some with tool support.
+
+* Know that at least three such languages, and
+  their distinguishing properties.
+
+[[LG-2-4]]
+==== LG 2-4: Refinement
+
+* Understand the notion of refinement.
+
+* Understand that it may be helpful to develop a separate model
+  between specification and implementation, which satisfies the
+  specification and is equivalent to the implementation.
+
+// end::EN[]