Dafny Concepts and Preconditions
Preconditions are required; postconditions are ensured.
Methods do not change given parameters unless a modifies clause is present.
Old(E) has the value of E at the start of the method.
Fresh(E) as a postcondition shows that E was created by M.
With if statements, Dafny works normally. With if-case statements, you introduce nondeterminism (hard; you need to prove all options).
Classes have instance variables and methods, which need clear contracts.
A trait is an abstract class, from which classes inherit (like a template in Java). Example: trait A; class B extends A
Class invariants must hold before and after any method. Use ghost predicate Valid().
Behavioral Subtyping: When a class A inherits from another class/trait,... Continue reading "Dafny Verification and Formal Methods Exam Review" »