Sumários

SAT and SMT

28 Outubro 2016, 16:30 Antónia Lopes

  • SAT solvers
  • SMT solvers


Specifying properties in JML

21 Outubro 2016, 18:30 Antónia Lopes

Exercises about specification of properties in JML from Problem Set 3.


Type Specifications I

21 Outubro 2016, 16:30 Antónia Lopes

  • Property-based specifications in JML
  • Representation-exposing specifications in JML


Dafny

14 Outubro 2016, 18:30 Antónia Lopes

Exercises about Dafny from Problem Set 2.


Design by Contract

14 Outubro 2016, 16:30 Antónia Lopes

  • Approaches to DBC (Design by Contract)
    • Preconditions and postconditions
    • Blame assignment
  • DBC with Dafny
    • Procedural abstraction
    • Additional specification features
  • DBC with JML
    • Procedural abstraction and JML assertions
    • Runtime verification
  • Hoare Logic versus Design by Contract