Design by Contract in Dafny

9 Novembro 2022, 18:30 • Antónia Lopes

Writing classes with property-based specifications in Dafny.

Design by Contract II

9 Novembro 2022, 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

Writing methods with contracts in Dafny

2 Novembro 2022, 18:30 • Antónia Lopes

Writing methods over arrays in Dafny and equip them with contracts 

Design By

2 Novembro 2022, 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
  • Additional specification primitives: requires, ensures, quantifiers, read and write frames 
  • Additional types: arrays and sequences 

Writing simple programs and properties in Dafny

19 Outubro 2022, 18:30 • Antónia Lopes

Writing simple programs and properties in Dafny.