Não houve aula (dia investigação)

22 Outubro 2025, 16:30 • Antónia Lopes

Não houve aula (dia investigação)

---

Exercises Dafny

15 Outubro 2025, 18:30 • Antónia Lopes

Exercises2 (Dafny&Hoare): 8
Exercises3 (Dafny&DbC): 5, 6, 7, 9

---

Design by contract: Contracts for Procedural Abstractions

15 Outubro 2025, 16:30 • Antónia Lopes

• Design by contract: Contracts for Procedural Abstractions (cont'd)
  • Additional types: matrices and sequences 
  • Additional specification primitives: old, fresh predicate
    • Examples: linear search in an array, grow array, copy array
• 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

---

Exercises Dafny-Hoare

8 Outubro 2025, 18:30 • Antónia Lopes

Exercises2 (Dafny-Hoare): 1,2,3,4 (8 left as homework!)

---

Design by contract

8 Outubro 2025, 16:30 • Antónia Lopes

• 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
  • Additional types: arrays, matrices and sequences 
  • Additional specification primitives: quantifiers, read and write frames, old

---