Sumários
Design by contract
18 Outubro 2023, 16:30 • Antónia Lopes
- Mechanising Deductive Verification (cont'd)
- Generation of verification conditions for bounded programs with WLP calculus
- Checking verification conditions with a SMT solver
- Introduction to design by contract (DbC)
- Contracts for procedural abstractions
- pre- and postconditions
- blame assignment
- Hoare triples vs contracts
- Compositional reasonig
- DbC for procedural abstractions in Dafny
- More about methods and functions
Exercises Hoare Calculus III
11 Outubro 2023, 18:30 • Antónia Lopes
- Exercises1 (Hoare): 1 (o), 5, 7, 8
Mechanising Software deductive verification
11 Outubro 2023, 16:30 • Antónia Lopes
- Introduction to Dafny
- simple methods, functions and lemmas
- specification primitives: assume and assert
- write Hoare triples in Dafny
- Weakest precondition calculus
- Dafny architecture
- Verification conditions
- Bounded programs
Deductive Verification II
4 Outubro 2023, 16:30 • Antónia Lopes
- Proof System (cont'd):
- Soundness and Completeness
- Formal theory
- Consistency (syntactically soundness)
- Syntatic Completeness
- Examples of first-order theories
- Theory of equality
- Theory of Presburger arithmetic
- Theory of Peano arithmetic
- The syntatic incompleteness of arithmetic
- Hoare logic (cont'd):
- Proving termination
- Soundness and completeness
- Pros & Cons