Contract driven development

[Google Scholar] [Wikipedia]

Notes: test driven development, modular verification
Papers: logozzo:vmcai:2011, fahndrich:foveoos:2010

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


Modular verification, Spec# project