Sumários

Exercises about Design by Contract in Dafny

20 Outubro 2021, 18:30 • Antónia Lopes

Exercises3 (Dafny&DbC): 1,2,5,6,7

Design by contract:Contracts for Data Abstractions

20 Outubro 2021, 16:30 • Antónia Lopes

Classes in Dafny
Design by contract:Contracts for Data Abstractions

  • Invariants and representation invariants
  • Property-based specifications
  • Model-based specifications
Brief overview of design by contract in Java with JML

Exercises about Design by Contract in Dafny

20 Outubro 2021, 15:00 • Antónia Lopes

Exercises3 (Dafny&DbC): 1,2,5,6,7

Exercises about procedures and functions in Dafny

13 Outubro 2021, 18:30 • Antónia Lopes

Exercises2 (Dafny&Hoare): 4,5,6,8

Design by Contract: Procedural Abstraction

13 Outubro 2021, 16:30 • Antónia Lopes

Design by contract: Contracts for Procedural Abstraction

    • Compositional reasonig
    • DbC in Dafny
    • Additional specification primitives: quantifiers, read and write frames 
Hoare Logic versus Design by Contract