Sumários
Design by contract: Contracts for Data Abstractions
30 Outubro 2024, 16:30 • Antónia Lopes
- Design by contract: Contracts for Data Abstractions
- Classes in Dafny
- Invariants and representation invariants
- Dynamic frames and idioms for expressing representation frames
- Property-based specifications
- Observers, Producers and Mutators
- Overview of Model-based specifications for Object Types
Exercises in Dafny; DbC for procedures and functions
23 Outubro 2024, 18:30 • Antónia Lopes
- Exercises2 (Dafny&Hoare): 1, 8
- Exercises3 (Dafny-DbC): 7, 9
Design by contract: Contracts for Procedural Abstractions
23 Outubro 2024, 16:30 • Antónia Lopes
- Design by contract: Contracts for Procedural Abstractions (cont'd)
- Additional types: arrays, matrices and sequences
- Additional specification primitives: quantifiers, read and write frames, old, fresh predicate
- Examples: linear search in an array, grow array, copy array
Mechanising Deductive Verification (cont'd)
16 Outubro 2024, 16:30 • Antónia Lopes
- Mechanising Deductive Verification (cont'd)
- Dafny architecture
- Verification conditions
- Bounded programs
- Weakest precondition calculus
- 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