Formal specification -- contracts

Verification -- as a design methodology

Runtime consistency -- invariance

  • behavioral types specify test cases
  • invariants and assertions monitor consistency

slide: Formal specification and verification