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