Design by contract
Encyclopedia
Design by contract also known as programming by contract and design-by-contract programming, is an approach to designing computer software
. It prescribes that software designers should define formal
, precise and verifiable interface specifications for software components, which extend the ordinary definition of abstract data type
s with precondition
s, postcondition
s and invariants
. These specifications are referred to as "contracts", in accordance with a conceptual metaphor
with the conditions and obligations of business contracts.
"Design by Contract" is a registered trademark
of Eiffel Software
in the United States. Microsoft calls their design-by-contract programming implementation "Code Contracts".
in connection with his design of the Eiffel programming language
and first described in various articles starting in 1986 and the two successive editions (1988, 1997) of his book Object-Oriented Software Construction
. Eiffel Software applied for trademark registration for Design by Contract in December 2003, and it was granted in December 2004. The current owner of this trademark is Eiffel Software.
'Design by contract has its roots in work on formal verification
, formal specification
and Hoare logic
. The original contributions include:
Similarly, if a routine from a class in object-oriented programming
provides a certain functionality, it may:
The contract is the formalization of these obligations and benefits. One could summarize design by contract by the "three questions" that the designer must repeatedly ask:
Many languages have facilities to make assertion
s like these. However, DbC considers these contracts to be so crucial to software correctness that they should be part of the design process. In effect, DbC advocates writing the assertions first.
The notion of a contract extends down to the method/procedure level; the contract for each method will normally contain the following pieces of information:
Subclasses in an inheritance hierarchy are allowed to weaken preconditions (but not strengthen them) and strengthen postconditions and invariants (but not weaken them). These rules approximate behavioral subtyping.
All class relationships are between Client classes and Supplier classes. A Client class is obliged to make calls to Supplier features where the resulting state of the Supplier is not violated by the Client call. Subsequently, the Supplier is obliged to provide a return state and data that does not violate the state requirements of the Client. For instance, a Supplier data buffer may require that data is present in the buffer when a delete feature is called. Subsequently, the Supplier guarantees to the client that when a delete feature finishes its work, the data item will, indeed, be deleted from the buffer. Other design contracts are concepts of "class invariant". The Class Invariant guarantees (for the local class) that the state of the class will be maintained within specified tolerances at the end of each feature execution.
When using contracts, a supplier should not try to verify that the contract conditions are satisfied; the general idea is that code should "fail hard", with contract verification being the safety net. DbC's "fail hard" property simplifies the debugging of contract behavior as the intended behaviour of each routine is clearly specified. This distinguishes it markedly from a related practice known as defensive programming
, where the supplier is responsible for figuring out what to do when a precondition is broken. More often than not, the supplier throws an exception to inform the client that the precondition has been broken, and in both cases—DbC and defensive programming—the client must figure out how to respond to that. DbC makes the supplier's job easier.
Design by contract also defines criteria for correctness for a software module:
Because the contract conditions should never be violated in program execution, they can be either left in as debugging code or removed from the production version of the code altogether for performance reasons.
Design by contract can also facilitate code reuse, since the contract for each piece of code is fully documented. The contracts for a module can be regarded as a form of software documentation
for the behavior of that module.
ing tests a module in isolation, to check that it meets its contract assuming its subcontractors meet theirs. Integration testing
checks whether the various modules are working properly together.
, D
, Eiffel
, Fortress, Lisaac
, Nice, Oxygene (formerly Chrome), Racket (including higher order contracts, and emphasizing that contract violations must blame the guilty party and must do so with an accurate explanation), Sather
, SPARK (via static analysis
of Ada
programs), Spec#
, Vala
, VDM, and languages that are built on top of the Microsoft .NET framework version 4.x (C#, VB.NET) through the use of the System.Diagnostics.Contract namespace.
Computer software
Computer software, or just software, is a collection of computer programs and related data that provide the instructions for telling a computer what to do and how to do it....
. It prescribes that software designers should define formal
Formal methods
In computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...
, precise and verifiable interface specifications for software components, which extend the ordinary definition of abstract data type
Abstract data type
In computing, an abstract data type is a mathematical model for a certain class of data structures that have similar behavior; or for certain data types of one or more programming languages that have similar semantics...
s with precondition
Precondition
In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification....
s, postcondition
Postcondition
In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions within the code itself...
s and invariants
Invariant (computer science)
In computer science, a predicate is called an invariant to a sequence of operations provided that: if the predicate is true before starting the sequence, then it is true at the end of the sequence.-Use:...
. These specifications are referred to as "contracts", in accordance with a conceptual metaphor
Conceptual metaphor
In cognitive linguistics, conceptual metaphor, or cognitive metaphor, refers to the understanding of one idea, or conceptual domain, in terms of another, for example, understanding quantity in terms of directionality . A conceptual domain can be any coherent organization of human experience...
with the conditions and obligations of business contracts.
"Design by Contract" is a registered trademark
Trademark
A trademark, trade mark, or trade-mark is a distinctive sign or indicator used by an individual, business organization, or other legal entity to identify that the products or services to consumers with which the trademark appears originate from a unique source, and to distinguish its products or...
of Eiffel Software
Eiffel Software
Eiffel Software is a software company specializing in object technology, especially tools, training and services for the Eiffel programming language and method, originally introduced by the company in 1985.The company's two flagship products are the EiffelStudio integrated development environment,...
in the United States. Microsoft calls their design-by-contract programming implementation "Code Contracts".
History
The term was coined by Bertrand MeyerBertrand Meyer
Bertrand Meyer is an academic, author, and consultant in the field of computer languages. He created the Eiffel programming language.-Education and academic career:...
in connection with his design of the Eiffel programming language
Eiffel (programming language)
Eiffel is an ISO-standardized, object-oriented programming language designed by Bertrand Meyer and Eiffel Software. The design of the language is closely connected with the Eiffel programming method...
and first described in various articles starting in 1986 and the two successive editions (1988, 1997) of his book Object-Oriented Software Construction
Object-Oriented Software Construction
Object-Oriented Software Construction is a book by Bertrand Meyer, widely considered a foundational text of object-oriented programming. The first edition was published in 1988; the second, extensively revised and expanded edition , in 1997...
. Eiffel Software applied for trademark registration for Design by Contract in December 2003, and it was granted in December 2004. The current owner of this trademark is Eiffel Software.
'Design by contract has its roots in work on formal verification
Formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...
, formal specification
Formal specification
In computer science, a formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not how the system should do it...
and Hoare logic
Hoare logic
Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...
. The original contributions include:
- A clear metaphor to guide the design process
- The application to inheritanceInheritance (computer science)In object-oriented programming , inheritance is a way to reuse code of existing objects, establish a subtype from an existing object, or both, depending upon programming language support...
, in particular a formalism for redefinition and dynamic binding - The application to exception handling
- The connection with automatic software documentationSoftware documentationSoftware documentation or source code documentation is written text that accompanies computer software. It either explains how it operates or how to use it, and may mean different things to people in different roles....
Description
The central idea of DbC is a metaphor on how elements of a software system collaborate with each other, on the basis of mutual obligations and benefits. The metaphor comes from business life, where a "client" and a "supplier" agree on a "contract" which defines for example that:- The supplier must provide a certain product (obligation) and is entitled to expect that the client has paid its fee (benefit).
- The client must pay the fee (obligation) and is entitled to get the product (benefit).
- Both parties must satisfy certain obligations, such as laws and regulations, applying to all contracts.
Similarly, if a routine from a class in object-oriented programming
Object-oriented programming
Object-oriented programming is a programming paradigm using "objects" – data structures consisting of data fields and methods together with their interactions – to design applications and computer programs. Programming techniques may include features such as data abstraction,...
provides a certain functionality, it may:
- Expect a certain condition to be guaranteed on entry by any client module that calls it: the routine's preconditionPreconditionIn computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification....
—an obligation for the client, and a benefit for the supplier (the routine itself), as it frees it from having to handle cases outside of the precondition. - Guarantee a certain property on exit: the routine's postconditionPostconditionIn computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions within the code itself...
—an obligation for the supplier, and obviously a benefit (the main benefit of calling the routine) for the client. - Maintain a certain property, assumed on entry and guaranteed on exit: the class invariantClass invariantIn computer programming, specifically object-oriented programming, a class invariant is an invariant used to constrain objects of a class. Methods of the class should preserve the invariant. The class invariant constrains the state stored in the object....
.
The contract is the formalization of these obligations and benefits. One could summarize design by contract by the "three questions" that the designer must repeatedly ask:
- What does it expect?
- What does it guarantee?
- What does it maintain?
Many languages have facilities to make assertion
Assertion (computing)
In computer programming, an assertion is a predicate placed in a program to indicate that the developer thinks that the predicate is always true at that place.For example, the following code contains two assertions:...
s like these. However, DbC considers these contracts to be so crucial to software correctness that they should be part of the design process. In effect, DbC advocates writing the assertions first.
The notion of a contract extends down to the method/procedure level; the contract for each method will normally contain the following pieces of information:
- Acceptable and unacceptable input values or types, and their meanings
- Return values or types, and their meanings
- ErrorErrorThe word error entails different meanings and usages relative to how it is conceptually applied. The concrete meaning of the Latin word "error" is "wandering" or "straying". Unlike an illusion, an error or a mistake can sometimes be dispelled through knowledge...
and exceptionException handlingException handling is a programming language construct or computer hardware mechanism designed to handle the occurrence of exceptions, special conditions that change the normal flow of program execution....
conditions values or types, that can occur, and their meanings - Side effectsSide effect (computer science)In computer science, a function or expression is said to have a side effect if, in addition to returning a value, it also modifies some state or has an observable interaction with calling functions or the outside world...
- PreconditionPreconditionIn computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification....
s - PostconditionPostconditionIn computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions within the code itself...
s - InvariantInvariant (computer science)In computer science, a predicate is called an invariant to a sequence of operations provided that: if the predicate is true before starting the sequence, then it is true at the end of the sequence.-Use:...
s - (more rarely) Performance guarantees, e.g. for time or space used
Subclasses in an inheritance hierarchy are allowed to weaken preconditions (but not strengthen them) and strengthen postconditions and invariants (but not weaken them). These rules approximate behavioral subtyping.
All class relationships are between Client classes and Supplier classes. A Client class is obliged to make calls to Supplier features where the resulting state of the Supplier is not violated by the Client call. Subsequently, the Supplier is obliged to provide a return state and data that does not violate the state requirements of the Client. For instance, a Supplier data buffer may require that data is present in the buffer when a delete feature is called. Subsequently, the Supplier guarantees to the client that when a delete feature finishes its work, the data item will, indeed, be deleted from the buffer. Other design contracts are concepts of "class invariant". The Class Invariant guarantees (for the local class) that the state of the class will be maintained within specified tolerances at the end of each feature execution.
When using contracts, a supplier should not try to verify that the contract conditions are satisfied; the general idea is that code should "fail hard", with contract verification being the safety net. DbC's "fail hard" property simplifies the debugging of contract behavior as the intended behaviour of each routine is clearly specified. This distinguishes it markedly from a related practice known as defensive programming
Defensive programming
Defensive programming is a form of defensive design intended to ensure the continuing function of a piece of software in spite of unforeseeable usage of said software. The idea can be viewed as reducing or eliminating the prospect of Murphy's Law having effect...
, where the supplier is responsible for figuring out what to do when a precondition is broken. More often than not, the supplier throws an exception to inform the client that the precondition has been broken, and in both cases—DbC and defensive programming—the client must figure out how to respond to that. DbC makes the supplier's job easier.
Design by contract also defines criteria for correctness for a software module:
- If the class invariant AND precondition are true before a supplier is called by a client, then the invariant AND the postcondition will be true after the service has been completed.
- When making calls to a Supplier, a software module should not violate the Supplier's preconditions.
Because the contract conditions should never be violated in program execution, they can be either left in as debugging code or removed from the production version of the code altogether for performance reasons.
Design by contract can also facilitate code reuse, since the contract for each piece of code is fully documented. The contracts for a module can be regarded as a form of software documentation
Software documentation
Software documentation or source code documentation is written text that accompanies computer software. It either explains how it operates or how to use it, and may mean different things to people in different roles....
for the behavior of that module.
Relationship with software testing
Unit testUnit test
In computer programming, unit testing is a method by which individual units of source code are tested to determine if they are fit for use.A unit is the smallest testable part of an application. In procedural programming a unit could be an entire module but is more commonly an individual function...
ing tests a module in isolation, to check that it meets its contract assuming its subcontractors meet theirs. Integration testing
Integration testing
Integration testing is the phase in software testing in which individual software modules are combined and tested as a group. It occurs after unit testing and before validation testing...
checks whether the various modules are working properly together.
Languages with native support
Languages that implement most DbC features natively include CobraCobra (programming language from Cobra Language LLC)
Cobra is an object-oriented programming language produced by Cobra Language LLC. Cobra is designed by Chuck Esterbrook, and runs on the Microsoft .NET and Mono platforms. It is strongly influenced by Python, C#, Eiffel, Objective-C, and other programming languages. It supports both static and...
, D
D (programming language)
The D programming language is an object-oriented, imperative, multi-paradigm, system programming language created by Walter Bright of Digital Mars. It originated as a re-engineering of C++, but even though it is mainly influenced by that language, it is not a variant of C++...
, Eiffel
Eiffel (programming language)
Eiffel is an ISO-standardized, object-oriented programming language designed by Bertrand Meyer and Eiffel Software. The design of the language is closely connected with the Eiffel programming method...
, Fortress, Lisaac
Lisaac
Lisaac is a compiled object-oriented programming language based on prototype concepts, with system programming facilities and design by contract....
, Nice, Oxygene (formerly Chrome), Racket (including higher order contracts, and emphasizing that contract violations must blame the guilty party and must do so with an accurate explanation), Sather
Sather
Sather is an object-oriented programming language. It originated circa 1990 at the International Computer Science Institute at the University of California, Berkeley, developed by an international team led by Steve Omohundro...
, SPARK (via static analysis
Static code analysis
Static program analysis is the analysis of computer software that is performed without actually executing programs built from that software In most cases the analysis is performed on some version of the source code and in the other cases some form of the object code...
of Ada
Ada (programming language)
Ada is a structured, statically typed, imperative, wide-spectrum, and object-oriented high-level computer programming language, extended from Pascal and other languages...
programs), Spec#
Spec sharp
Spec# is a programming language with specification language features that extends the capabilities of the C# programming language with Eiffel-like contracts, including object invariants, preconditions and postconditions. Like ESC/Java, it includes a static checking tool based on a theorem prover...
, Vala
Vala (programming language)
Vala is a programming language created with the goal of bringing modern language features to C, with no added runtime needs and with little overhead, by targeting the GObject object system. It is being developed by Jürg Billeter and Raffaele Sandrini. The syntax borrows heavily from C#...
, VDM, and languages that are built on top of the Microsoft .NET framework version 4.x (C#, VB.NET) through the use of the System.Diagnostics.Contract namespace.
Languages with third-party support
Various libraries, preprocessors and other tools have been developed for existing programming languages without native Design by Contract support:- AdaAda (programming language)Ada is a structured, statically typed, imperative, wide-spectrum, and object-oriented high-level computer programming language, extended from Pascal and other languages...
, via GNATGNATGNAT is a free-software compiler for the Ada programming language which forms part of the GNU Compiler Collection. It supports all versions of the language, i.e. Ada 2005, Ada 95 and Ada 83; it allows already some constructs of Ada 2012...
pragmas for preconditions and postconditions. The Ada Rapporteur Group is preparing the inclusion of subprogram contracts (AI05-0145) and type invariants (AI05-0146) in the future version of Ada, Ada 201X. - CC (programming language)C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....
and C++C++C++ is a statically typed, free-form, multi-paradigm, compiled, general-purpose programming language. It is regarded as an intermediate-level language, as it comprises a combination of both high-level and low-level language features. It was developed by Bjarne Stroustrup starting in 1979 at Bell...
, via the DBC for C preprocessorPreprocessorIn computer science, a preprocessor is a program that processes its input data to produce output that is used as input to another program. The output is said to be a preprocessed form of the input data, which is often used by some subsequent programs like compilers...
, GNU Nana, eCv static analysisStatic analysisStatic analysis, static projection, and static scoring are terms for simplified analysis wherein the effect of an immediate change to a system is calculated without respect to the longer term response of the system to that change...
tool, or the Digital MarsDigital MarsDigital Mars is a small American software company owned by Walter Bright that makes C and C++ compilers for Windows and DOS. They also distribute the compilers for free on their web site....
C++ compiler, via CTESK extension of C. Loki LibraryLoki (C++)Loki is the name of a C++ software library written by Andrei Alexandrescu as part of his book Modern C++ Design.The library makes extensive use of C++ template metaprogramming and implements several commonly used tools: typelist, functor, singleton, smart pointer, object factory, visitor and...
provides a mechanism named ContractChecker which verifies a class follows design by contract. - C# (and other .NET languages), via Code Contracts (a Microsoft ResearchMicrosoft ResearchMicrosoft Research is the research division of Microsoft created in 1991 for developing various computer science ideas and integrating them into Microsoft products. It currently employs Turing Award winners C.A.R. Hoare, Butler Lampson, and Charles P...
project integrated into the .NET Framework.NET FrameworkThe .NET Framework is a software framework that runs primarily on Microsoft Windows. It includes a large library and supports several programming languages which allows language interoperability...
4.0) - Groovy via GContracts GContracts
- JavaJava (programming language)Java is a programming language originally developed by James Gosling at Sun Microsystems and released in 1995 as a core component of Sun Microsystems' Java platform. The language derives much of its syntax from C and C++ but has a simpler object model and fewer low-level facilities...
, via iContract2, Contract4J, jContractor, Jcontract, C4J, Google CodePro Analytix, STclass, Jass preprocessor, OVal with AspectJAspectJAspectJ is an aspect-oriented extension created at PARC for the Java programming language. It is available in Eclipse Foundation open-source projects, both stand-alone and integrated into Eclipse. AspectJ has become the widely-used de-facto standard for AOP by emphasizing simplicity and usability...
, Java Modeling LanguageJava Modeling LanguageThe Java Modeling Language is a specification language for Java programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm...
(JML), SpringContracts for the Spring framework, Modern Jass, Custos using AspectJ,JavaDbC using AspectJ, JavaTESK using extension of Java, chex4j using javassist, or Contracts for Java, and the highly customizable java-on-contracts. - JavaScriptJavaScriptJavaScript is a prototype-based scripting language that is dynamic, weakly typed and has first-class functions. It is a multi-paradigm language, supporting object-oriented, imperative, and functional programming styles....
, via Cerny.js or ecmaDebug. - Common LispCommon LispCommon Lisp, commonly abbreviated CL, is a dialect of the Lisp programming language, published in ANSI standard document ANSI INCITS 226-1994 , . From the ANSI Common Lisp standard the Common Lisp HyperSpec has been derived for use with web browsers...
, via the macro facility or the CLOS metaobject protocolMetaobjectIn computer science, a metaobject or meta-object is any entity that manipulates, creates, describes, or implements other objects. The object that the metaobject is about is called the base object...
. - Nemerle, via macros.
- PerlPerlPerl is a high-level, general-purpose, interpreted, dynamic programming language. Perl was originally developed by Larry Wall in 1987 as a general-purpose Unix scripting language to make report processing easier. Since then, it has undergone many changes and revisions and become widely popular...
, via the CPANCPANCPAN, the Comprehensive Perl Archive Network, is an archive of nearly 100,000 modules of software written in Perl, as well as documentation for it. It has a presence on the World Wide Web at and is mirrored worldwide at more than 200 locations...
modules Class::Contract (by Damian ConwayDamian ConwayDamian Conway is a prominent member of the Perl community, a proponent of object-oriented programming, and the author of several books. He is also an Adjunct Associate Professor in the Faculty of Information Technology at Monash University....
) or Carp::Datum (by Raphael ManfrediRaphael ManfrediRaphaël Manfredi has been the author of many open-source programs since 1990.He is currently the main software architect of gtk-gnutella but has also made numerous contributions to Perl.- External links :*- References :...
). - PythonPython (programming language)Python is a general-purpose, high-level programming language whose design philosophy emphasizes code readability. Python claims to "[combine] remarkable power with very clear syntax", and its standard library is large and comprehensive...
, using packages like zope.interface, PyDBC or Contracts for Python. - RubyRuby (programming language)Ruby is a dynamic, reflective, general-purpose object-oriented programming language that combines syntax inspired by Perl with Smalltalk-like features. Ruby originated in Japan during the mid-1990s and was first developed and designed by Yukihiro "Matz" Matsumoto...
, via Brian McCallister's DesignByContract, Ruby DBC or ruby-contract. - TclTclTcl is a scripting language created by John Ousterhout. Originally "born out of frustration", according to the author, with programmers devising their own languages intended to be embedded into applications, Tcl gained acceptance on its own...
, via the XOTclXOTclXOTcl is an object-oriented extension for the Tool Command Language created by Gustaf Neumann and Uwe Zdun. It is an extension of the MIT OTcl. XOTcl supports metaclasses. Class and method definitions are completely dynamic...
object-oriented extension.
Generic tools
- Perfect DeveloperPerfect DeveloperPerfect Developer is a tool for developing computer programs in a rigorous manner. It is used to develop applications in areas including IT systems and airborne critical systems. The principle is to develop a formal specification and refine the specification to code...
, via the Perfect specification language, can verify contracts with static code analysisStatic code analysisStatic program analysis is the analysis of computer software that is performed without actually executing programs built from that software In most cases the analysis is performed on some version of the source code and in the other cases some form of the object code...
and generate programs in languages such as C++ and Java.
See also
- Component-based software engineeringComponent-based software engineeringComponent-based software engineering is a branch of software engineering that emphasizes the separation of concerns in respect of the wide-ranging functionality available throughout a given software system...
- Defensive programmingDefensive programmingDefensive programming is a form of defensive design intended to ensure the continuing function of a piece of software in spite of unforeseeable usage of said software. The idea can be viewed as reducing or eliminating the prospect of Murphy's Law having effect...
- Formal methodsFormal methodsIn computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...
- Hoare logicHoare logicHoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...
- Modular programmingModular programmingModular programming is a software design technique that increases the extent to which software is composed of separate, interchangeable components called modules by breaking down program functions into modules, each of which accomplishes one function and contains everything necessary to accomplish...
- Program refinement
- Test-driven developmentTest-driven developmentTest-driven development is a software development process that relies on the repetition of a very short development cycle: first the developer writes a failing automated test case that defines a desired improvement or new function, then produces code to pass that test and finally refactors the new...
External links
- An introduction to Design by Contract(TM)
- Original IEEE Computer article
- Isaac / Lisaac Project home
- dlib C++ Library
- Java Programming by Contract Class Utility
- GContracts - Programming by Contract with Groovy
- C2 Wiki: Design by Contract
- Damian Conway's Class::Contract Perl module from CPAN
- Raphael Manfredi's Carp::Datum Perl module from CPAN
- GNU Nana
- Digital Mars Contract Programming (DBC)
- Class Contracts in Delphi Prism
- Contract language and tools for .NET
- Using Code Contracts for Safer Code