Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adjust LG headings to new format #14

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
+44 −56
Open

Adjust LG headings to new format #14

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2e27bf7
Adjust LG headings to new format
mikesperber Jan 17, 2025
0b77fc3
Merge branch 'main' into learning-goal-headings
larsrh Jan 18, 2025
5b2fbf0
Apply Ben's suggestion from review
mikesperber Jan 24, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 5 additions & 15 deletions docs/01-module-block-1/02-learning-goals.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,7 @@ wie wichtig einzelne Aspekte des Lernziels sind. Es kann hier bereits auf Litera

// tag::EN[]
[[LG-1-1]]
==== LG 1-1: Propositional Logic
Know the basic structure of propositional logic:
==== LG 1-1: Know the basic structure of propositional logic
mikesperber marked this conversation as resolved.
Show resolved Hide resolved

* (atomic) propositions and their syntax
* logical connectives such as conjunction
Expand All @@ -27,9 +26,7 @@ Know the basic structure of propositional logic:
* Decidability of propositional logic

[[LG-1-2]]
==== LG 1-2: Predicate Logic

Know the basic structure of predicate/first-order logic:
==== LG 1-2: Know the basic structure of predicate/first-order logic

* terms and their syntactic structure (variables, functions)
* formulas and their syntactic structure (predicates, quantifiers)
Expand All @@ -45,18 +42,14 @@ Know the basic structure of predicate/first-order logic:
* semi-decidability of predicate logic

[[LG-1-3]]
==== LG 1-3: Temporal Logic

Know the basic structure of temporal operators:
==== LG 1-3: 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:
==== LG 1-4: 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
Expand All @@ -66,10 +59,7 @@ Understand the basic concepts of a logical calculus:
* Resolution

[[LG-1-5]]
==== LG 1-5: Intuitionistic vs. Classical Logic

Understand the difference between intuitionistic and
classical logic:
==== LG 1-5: 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)
Expand Down
54 changes: 26 additions & 28 deletions docs/02-module-block-2/02-learning-goals.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,33 +19,31 @@ tbd.

// tag::EN[]
[[LG-2-1]]
==== LG 2-1: Notions of specification
==== LG 2-1: Differentiate notions of specification

* Know different notions of specification, specifically:
* examples
* properties
* formal
* mechanized

** examples
** properties
** formal
** mechanized

* Understand that specification may pertain to different kinds of
components, such as:
[[LG-2-2]]
==== LG 2-2: Understand that specification may pertain to different kinds of components

** functions
** data types
** algorithms
** systems
* functions
* data types
* algorithms
* systems

* Understand that specifications may pertain to different
qualities, such as:
[[LG-2-3]]
==== LG 2-3: Understand that specifications may pertain to different qualities

** functionality
** performance effiicency
** security
** safety
* functionality
* performance effiicency
* security
* safety

[[LG-2-2]]
==== LG 2-2: Formal Specifications
[[LG-2-4]]
==== LG 2-4: Differentiate between formal specifications and other kinds of specifications

* Understand that applying formal methods requires formal
specifications.
Expand All @@ -57,19 +55,19 @@ tbd.
that admit only one output per input, and relational properties that
admit multiple outputs per input.

[[LG-2-3]]
==== LG 2-3: Specification Languages
[[LG-2-5]]
==== LG 2-5: Know the distinguishing properties at least three different 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.
* Examples for specification languages are Isabelle/HOL
<<nipkow2014>>, ACL2 <<kaufmann2000-approach>>, TLA+
<<lamport2022>>, and Alloy <<jackson2006>>.

[[LG-2-4]]
==== LG 2-4: Refinement

* Understand the notion of refinement.
[[LG-2-6]]
==== LG 2-6: Understand the notion of refinement

* Understand that it may be helpful to develop a separate model
between specification and implementation, which satisfies the
Expand Down
14 changes: 7 additions & 7 deletions docs/03-module-block-3/02-learning-goals.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ tbd.

// tag::EN[]
[[LG-3-1]]
==== LG 3-1: Applicability
==== LG 3-1: Identify where formal methods are applicable

* Know that not all parts of a typical software system are
susceptible to formal methods.
Expand All @@ -31,20 +31,20 @@ tbd.
methods.

[[LG-3-2]]
==== LG 3-2: Relevant Qualities
==== LG 3-2: Know relevant qualities that indicate the use of formal methods

* Know the qualities that typically indicate the use of formal
methods, such as reliability, safety, and security.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are these qualities of ISO25010? Then you should mention it here.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

They are, but I disagree - ISO 25010 has no special status in Foundation, either, and mentioning ISO 25010 would add no useful information.


[[LG-3-3]]
==== LG 3-3: Relevance Specification
==== LG 3-3: Understand the relevance of precise specification

* Know that the successful application of formal methods
depends on the precise specification of the properties they require
the software system to exhibit.

[[LG-3-4]]
==== LG 3-4: Tradeoffs
==== LG 3-4: Know tradeoffs between formal methods

Know the tradeoffs inherent in the choice of a particular formal
method, in particular with respect to:
Expand All @@ -55,14 +55,14 @@ method, in particular with respect to:
* the qualificiations required of those who apply the method.

[[LG-3-5]]
==== LG 3-5: Gradual Introduction
==== LG 3-5: Introduce formal methods gradually

* Know techniques for gradually introducing formal methods into a
software project such as adding static typing or property-based
testing.

[[LG-3-6]]
==== LG 3-6: Appropriate Selection of Methods
==== LG 3-6: Select appropriate formal methods

Be able to choose an appropriate formal method depending on the
form of the specification such as:
Expand All @@ -77,7 +77,7 @@ form of the specification such as:
(See section <<Tools>>.)

[[LG-3-7]]
==== LG 3-7: Architecture Evaluation
==== LG 3-7: Evaluate architecture with formal methods

Understand that formal methods can support architecture evaluation:

Expand Down
12 changes: 6 additions & 6 deletions docs/04-module-block-4/02-learning-goals.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,15 +20,15 @@ tbd.

// tag::EN[]
[[LG-4-1]]
==== LG 4-1: Property-Based Testing
==== LG 4-1: Apply property-based testing

* Understand the concept of property-based testing, can
identify for which properties it is amenable, and guide the
implementation of property-based testing in a software project.


[[LG-4-2]]
==== LG 4-2: Type Systems
==== LG 4-2: Understand the role of type systems

* Understand that type systems can express and ensure properties of
software system.
Expand All @@ -41,7 +41,7 @@ tbd.
a software system.

[[LG-4-3]]
==== LG 4-3: Model Checking
==== LG 4-3: Apply model checking to verify properties of automata

* Understand that Model Checking describes methods to check whether a
logic formula is satisfied by a given model.
Expand All @@ -61,7 +61,7 @@ tbd.
** limitations

[[LG-4-4]]
==== LG 4-4: Proof Assistants
==== LG 4-4: Apply proof assistants to verify properties of arbitrary software systems

* Understand the mode of operation of proof assistants.

Expand All @@ -74,7 +74,7 @@ tbd.
projects into proof obligations for a proof assistant.

[[LG-4-5]]
==== LG 4-5: SMT Solvers
==== LG 4-5: Apply SMT Solvers to verify constraints of arbitrary software systems

* Understand the concept of satisfiability modulo theories (SMT) and
its application and constraints as a tool for checking properties of
Expand All @@ -88,7 +88,7 @@ tbd.


[[LG-4-6]]
==== LG 4-6: Abstract Interpretation
==== LG 4-6: Apply Abstract Interpretation to predict dynamic behavior statically

* Understand that the possible dynamic behavior of programs can be
soundly predicted using static analysis.
Expand Down
Loading