Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Comparing design by contract to type systems

Tags:

I recently read a paper that compared Design-by-Contract to Test-Driven-Development. There seems to be lot of overlap, some redundancy, and a little bit of synergy between the DbC and TDD. For example, there are systems for automatically generating tests based on contracts.

In what way does DbC overlap with modern type system (such as in haskell, or one of those dependently typed languages) and are there points where using both is better than either?

like image 223
aleator Avatar asked May 11 '11 13:05

aleator


People also ask

Why is design by contract useful?

The benefits of Design by Contract include the following: A better understanding of the object-oriented method and, more generally, of software construction. A systematic approach to building bug-free object-oriented systems. An effective framework for debugging, testing and, more generally, quality assurance.

What is Contract based design?

Contract-based design is an approach where the design process is seen as a successive assembly of components where a component is represented in terms of assumptions about its environment and guarantees about its behavior.

What does design by contract mean in an OO program?

“Design by Contract” is an object-oriented technique which defines contracts for the main program elements – methods and classes [1]. The client code must adhere to the contract otherwise the result is undefined. The contract consists of three main elements – preconditions, postconditions and invariants.


2 Answers

The paper Typed Contracts for Functional Programming by Ralf Hinze, Johan Jeuring, and Andres Löh had this handy table that illustrates whereabouts contracts sit in the design spectrum of "checking":

                   |   static checking    |   dynamic checking ------------------------------------------------------------------- simple properties  | static type checking | dynamic type checking complex properties | theorem proving      | contract checking 
like image 113
stephen tetley Avatar answered Oct 10 '22 23:10

stephen tetley


It seems most answers assume that contracts are checked dynamically. Note that in some systems contracts are checked statically. In such systems you can think of contracts as a restricted form of dependent types which can be checked automatically. Contrast this with richer dependent types, which are checked interactively, such as in Coq.

See the "Specification Checking" section on Dana Xu's page for papers on static and hybrid checking (static followed by dynamic) of contracts for Haskell and OCaml. The contract system of Xu includes refinement types and dependent arrows, both of which are dependent types. Early languages with restricted dependent types that are automatically checked include the DML and ATS of Pfenning and Xi. In DML, unlike in Xu's work, the dependent types are restricted so that automatic checking is complete.

like image 28
ntc2 Avatar answered Oct 10 '22 23:10

ntc2