Formal specification -- contracts
- type specification -- local properties
- relational specification -- structural properties, type relations
- functional specification -- requirements
Verification -- as a design methodology
- reasoning about program specification/code
Runtime consistency -- invariance
- behavioral types specify test cases
- invariants and assertions monitor consistency
slide: Formal specification and verification