Contract driven development is a development methodology where you write a contract for a function/method/class before implementing it.

The name comes from Bertrand Meyer’s paper [meyer:fase:2007].

In a formal verification context, this is often synonymous with modular verification.

The approach of defining the desired behaviour before implementing the behaviour bears some resemblance to test driven development.

Formal verification papers: logozzo:vmcai:2011, fahndrich:foveoos:2010

[meyer:fase:2007]: https://doi.org/10.1007/978-3-540-71289-3_2

Notes related to Contract driven development

Modular verification, Spec# project

Papers related to Contract driven development

• Specification and verification: The Spec# experience [barnett:cacm:2011]
• Boogie: A modular reusable verifier for object-oriented programs [barnett:fmco:2005]
• Enforcing high-level protocols in low-level software [deline:pldi:2001]
• Static contract checking with abstract interpretation [fahndrich:foveoos:2010]
• Behavioral interface specification languages [hatcliff:compsurv:2012]
• Verification of concurrent programs with Chalice [leino:fosad:2007]
• No panic! Verification of Rust programs by symbolic execution [lindner:indin:2018]
• Practical verification for the working programmer with CodeContracts and abstract interpretation [logozzo:vmcai:2011]
• Verifying security invariants in ExpressOS [mai:asplos:2013]