Hubbry Logo
Design by contractDesign by contractMain
Open search
Design by contract
Community hub
Design by contract
logo
8 pages, 0 posts
0 subscribers
Be the first to start a discussion here.
Be the first to start a discussion here.
Design by contract
Design by contract
Design by contract
View on Wikipedia
from Wikipedia
A design by contract scheme

Design by contract (DbC), also known as contract programming, programming by contract and design-by-contract programming, is an approach for designing 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 types with preconditions, postconditions and invariants. These specifications are referred to as "contracts", in accordance with a conceptual metaphor with the conditions and obligations of business contracts.

The DbC approach assumes all client components that invoke an operation on a server component will meet the preconditions specified as required for that operation.

Where this assumption is considered too risky (as in multi-channel or distributed computing), the inverse approach is taken, meaning that the server component tests that all relevant preconditions hold true (before, or while, processing the client component's request) and replies with a suitable error message if not.

History

[edit]

The term was coined by Bertrand Meyer in connection with his design of the Eiffel programming language and first described in various articles starting in 1986[1][2][3] 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.[4][5] The current owner of this trademark is Eiffel Software.[6][7]

Design by contract has its roots in work on formal verification, formal specification and Hoare logic. The original contributions include:

Description

[edit]

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" that 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 the method of a class in object-oriented programming provides a certain functionality, it may:

  • Expect a certain condition to be guaranteed on entry by any client module that calls it: the method's precondition—an obligation for the client, and a benefit for the supplier (the method itself), as it frees it from having to handle cases outside of the precondition.
  • Guarantee a certain property on exit: the method's postcondition—an obligation for the supplier, and obviously a benefit (the main benefit of calling the method) for the client.
  • Maintain a certain property, assumed on entry and guaranteed on exit: the class invariant.

The contract is semantically equivalent to a Hoare triple which formalises the obligations. This can be summarised by the "three questions" that the designer must repeatedly answer in the contract:

  • What does the contract expect?
  • What does the contract guarantee?
  • What does the contract maintain?

Many programming languages have facilities to make assertions 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.[citation needed] Contracts can be written by code comments, enforced by a test suite, or both, even if there is no special language support for contracts.

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:[citation needed]

  • Acceptable and unacceptable input values or types, and their meanings
  • Return values or types, and their meanings
  • Error and exception condition values or types that can occur, and their meanings
  • Side effects
  • Preconditions
  • Postconditions
  • Invariants
  • (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 behavioural 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—a practice known as offensive programming—the general idea being 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 method is clearly specified.

This approach differs substantially from that of 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 alike—the client must figure out how to respond to that. In such cases, 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.

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.

Design by contract may look something like this:[8][9] 

int f(const int x)
    pre(x != 1) // a precondition assertion
    post(r : r == x && r != 2) // a postcondition assertion; r names the result object of f
{
    contract_assert(x != 3); // an assertion statement
    return x;
}

Performance implications

[edit]

Contract conditions should never be violated during execution of a bug-free program. Contracts are therefore typically only checked in debug mode during software development. Later at release, the contract checks are disabled to maximize performance.

In many programming languages, contracts are implemented with assert. Asserts are by default compiled away in release mode in C/C++, and similarly deactivated in C#[10] and Java.

Launching the Python interpreter with "-O" (for "optimize") as an argument will likewise cause the Python code generator to not emit any bytecode for asserts.[11]

This effectively eliminates the run-time costs of asserts in production code—irrespective of the number and computational expense of asserts used in development—as no such instructions will be included in production by the compiler.

Relationship to software testing

[edit]

Design by contract does not replace regular testing strategies, such as unit testing, integration testing and system testing. Rather, it complements external testing with internal self-tests that can be activated both for isolated tests and in production code during a test-phase.

The advantage of internal self-tests is that they can detect errors before they manifest themselves as invalid results observed by the client. This leads to earlier and more specific error detection.

The use of assertions can be considered to be a form of test oracle, a way of testing the design by contract implementation.

Language support

[edit]

Languages with native support

[edit]

Languages that implement most DbC features natively include:

Additionally, the standard method combination in the Common Lisp Object System has the method qualifiers :before, :after and :around that allow writing contracts as auxiliary methods, among other uses.

See also

[edit]

Notes

[edit]

Bibliography

[edit]
[edit]
Revisions and contributorsEdit on WikipediaRead on Wikipedia

Design by contract

View on Grokipedia
from Grokipedia
Design by Contract (DbC), also known as contract programming, is a software engineering methodology that treats the construction of software components as a series of formal agreements, or "contracts," between clients (callers) and suppliers (routines or modules), specifying mutual obligations through preconditions, postconditions, and class invariants to ensure reliability and correctness. Introduced by Bertrand Meyer in the context of the Eiffel programming language, DbC views software development as a contractual process where violations of these specifications trigger exceptions, promoting systematic debugging and quality assurance. The core principles of DbC revolve around three main assertion types: preconditions, which define conditions that must hold true before a routine is executed (responsibility of the client); postconditions, which guarantee outcomes after execution (responsibility of the supplier); and class invariants, which maintain consistent properties across all instances of a class throughout their lifecycle. These elements are expressed as expressions in the code, often using language-specific syntax, and are checked at runtime to detect errors early, while also serving as for interfaces. In inheritance hierarchies, DbC enforces rules such as weakening preconditions and strengthening postconditions in subclasses to preserve integrity, enabling safe polymorphism and reuse. Historically, emerged from research in the 1980s, building on ideas from program verification pioneers like Hoare and Dijkstra, and was first formalized in Meyer's 1988 book as a practical approach for object-oriented design. It gained prominence through the Eiffel language, where it is natively supported, and has influenced and testing practices by emphasizing partial correctness over total avoidance of errors. Key benefits include improved software reliability, clearer module interfaces, and reduced debugging time, as demonstrated in mission-critical applications like the rocket software analysis, where could have prevented failures by enforcing interface . While DbC is most fully integrated in Eiffel, implementations appear in other languages such as Ada 2012, which supports preconditions, postconditions, type invariants, and predicates via aspect specifications to align with Meyer's contractual model. Partial support exists in languages like Java through libraries (e.g., Contracts for Java) or annotations, and in C++ via assertion frameworks, though runtime enforcement varies and is not as seamless as in dedicated systems. Despite its proven effectiveness in enhancing software quality, DbC adoption remains limited in mainstream languages due to performance overhead from runtime checks and the need for precise specification writing.

Core Concepts

Preconditions

In Design by Contract (DbC), preconditions are boolean conditions that must evaluate to true immediately before a subroutine (such as a method or function) is invoked, verifying that the inputs and context satisfy the necessary criteria for the routine to operate correctly. These conditions form part of the explicit contract between the caller (client) and the callee (supplier), outlining the assumptions under which the routine is valid. Preconditions delineate the responsibilities of the caller, requiring them to ensure these conditions hold; if violated, the supplier bears no obligation to produce correct results or avoid failure, thereby shifting and preventing the supplier from needing to handle invalid scenarios defensively. This delineation promotes a clear division of labor in , where the supplier can focus on specified behaviors without redundant validation. For instance, in an array access routine, a might stipulate that the provided index is non-negative and within the array's bounds to ensure safe retrieval. Similarly, for inserting an element into a bounded collection like a stack or table, the could require that the collection is not already at full capacity. These can be expressed in as assertions checked at entry:

precondition array_access(index): require index >= 0 and index < array.length // Routine body proceeds only if true

precondition array_access(index): require index >= 0 and index < array.length // Routine body proceeds only if true

precondition insert(element): require collection.size < collection.capacity // Routine body proceeds only if true

precondition insert(element): require collection.size < collection.capacity // Routine body proceeds only if true

Such examples illustrate how preconditions enforce caller obligations through simple, verifiable checks. The unique advantages of preconditions include facilitating early detection of errors at the call site, where violations can be identified and addressed before deeper execution, and enabling modular reasoning by allowing developers to assume these conditions hold without re-verifying them internally. This supports more reliable software construction by clarifying interfaces and reducing the scope of potential faults. Postconditions complement preconditions by specifying guarantees upon routine exit.

Postconditions

Postconditions in Design by Contract represent the obligations of a subroutine to its caller, consisting of boolean expressions that must evaluate to true upon the subroutine's completion, assuming the preconditions have been satisfied. These expressions define the expected outcomes, including return values, modified states, and any side effects, thereby establishing clear guarantees about what the subroutine achieves. In practice, postconditions are often expressed using language-specific syntax, such as the ensure clause in Eiffel, where multiple assertions can be combined to specify various properties of the resulting state. For instance, in a routine that inserts an element into a table, postconditions might ensure that the table's size increases by one, the inserted element is retrievable via its key, and no other elements have been altered. If a postcondition fails during runtime checking, an exception is raised to signal the contract violation, allowing the caller to handle the failure appropriately and attributing responsibility to the subroutine's implementation. Some formulations explicitly include exception handling by stating that the postcondition holds or an exception has been raised, accommodating cases where the subroutine cannot fulfill its guarantees due to unforeseen errors. A representative example is a sorting subroutine, where the postcondition guarantees that the output array is sorted in non-decreasing order and contains exactly the same elements as the input, preserving the multiset of values. This can be illustrated in pseudocode as follows:

procedure sort(input: array of comparable elements) returns sorted_array require: input is non-null and elements are comparable // Implementation of sorting algorithm (e.g., quicksort) ensure: forall i from 0 to length(sorted_array)-2: sorted_array[i] <= sorted_array[i+1] ensure: multiset(sorted_array) == multiset(input)

procedure sort(input: array of comparable elements) returns sorted_array require: input is non-null and elements are comparable // Implementation of sorting algorithm (e.g., quicksort) ensure: forall i from 0 to length(sorted_array)-2: sorted_array[i] <= sorted_array[i+1] ensure: multiset(sorted_array) == multiset(input)

To verify compliance, the runtime system would evaluate these ensures after execution; for the sorting case, checks might confirm sequential ordering via pairwise comparisons and element permutation via counting or hashing. Such postconditions aid debugging by pinpointing failures immediately after the subroutine. Postconditions can be weak or strong, where a weak postcondition offers minimal guarantees (e.g., "the array contains the original elements in some order"), while a strong one provides tighter specifications (e.g., "the array is sorted in ascending order"). Stronger postconditions deliver more precise contracts and better reusability in verification but impose greater implementation constraints; in inheritance hierarchies, redefined subroutines may strengthen postconditions, as the new version must satisfy both the original (weaker) postcondition and any additional ones, ensuring compatibility with callers expecting the parent's guarantees. Mathematically, postconditions form part of Hoare logic triples of the form {P} S {Q}, where P is the precondition, S is the subroutine, and Q is the postcondition, asserting that if P holds before executing S, then Q will hold afterward (assuming termination). This framework underpins formal proofs of correctness in Design by Contract.

Class Invariants

Class invariants in Design by Contract represent boolean properties that must hold true for every instance of a class at all times when the object is in a stable state, ensuring the consistency and reliability of the object's internal representation. These invariants encapsulate the essential constraints on the class's data, promoting encapsulation by hiding implementation details while guaranteeing that the object's state remains valid throughout its lifecycle. The scope of class invariants extends to key points in an object's lifecycle: they must be established upon object creation, preserved between calls to public (exported) routines, and verified after the execution of such routines, as well as upon object destruction if applicable. Private routines inherit the invariant as an implicit obligation but do not explicitly check or enforce it at their boundaries, allowing internal operations flexibility while relying on the enclosing public routines to maintain overall consistency. This selective enforcement applies specifically to public operations, where the invariant is conjoined with the routine's precondition before entry and with its postcondition after exit. A representative example is a bank account class, where the invariant ensures the balance never falls below the negative of the credit limit, preventing invalid financial states. In pseudocode inspired by Eiffel's syntax, the invariant might be declared as follows:

class ACCOUNT attribute balance: INTEGER credit_limit: INTEGER invariant credit_limit >= 0 balance >= -credit_limit create make (initial_balance: INTEGER; limit: INTEGER) -- Establish initial state satisfying invariant do balance := initial_balance credit_limit := limit ensure balance = initial_balance credit_limit = limit end routine withdraw (amount: INTEGER) -- Reduce balance by amount, preserving invariant require amount > 0 balance - amount >= -credit_limit -- Temporary precondition check do balance := balance - amount ensure balance = old balance - amount end end

class ACCOUNT attribute balance: INTEGER credit_limit: INTEGER invariant credit_limit >= 0 balance >= -credit_limit create make (initial_balance: INTEGER; limit: INTEGER) -- Establish initial state satisfying invariant do balance := initial_balance credit_limit := limit ensure balance = initial_balance credit_limit = limit end routine withdraw (amount: INTEGER) -- Reduce balance by amount, preserving invariant require amount > 0 balance - amount >= -credit_limit -- Temporary precondition check do balance := balance - amount ensure balance = old balance - amount end end

Here, the invariant is implicitly checked after creation and at the end of the withdraw routine, confirming balance >= -credit_limit holds. In object-oriented , class invariants propagate from to child classes through , requiring subclasses to satisfy both their own invariants and those of their ancestors. Subclasses may strengthen the inherited invariant by adding more restrictive conditions but cannot weaken it, ensuring behavioral compatibility and preventing violations of the 's in derived types. For instance, a base TREE class might invariant that a child's references the tree , which a subclass BINARY_TREE inherits and potentially augments with constraints on left and right children. Class invariants subsume and contextualize preconditions and postconditions by providing a persistent framework for the entire class state, where routine-specific assertions operate within the bounds of the invariant to maintain long-term object integrity across multiple operations.

Historical Development

Origins with Bertrand Meyer

Bertrand Meyer, a French computer scientist and software engineer, originated the Design by Contract (DbC) methodology as a foundational principle for reliable software construction, deeply influenced by advancements in formal methods and software engineering during the late 20th century. His approach emphasized specifying clear obligations for software components through assertions, drawing inspiration from the systematic program verification techniques pioneered by Edsger W. Dijkstra and C.A.R. Hoare. Dijkstra's work on structured programming and disciplined development, as outlined in his 1976 book A Discipline of Programming, provided a framework for rigorous program design that Meyer extended to object-oriented contexts. Similarly, Hoare's axiomatic semantics, introduced in his 1969 paper "An Axiomatic Basis for Computer Programming," supplied the theoretical basis for preconditions, postconditions, and invariants, which Meyer adapted to enforce contractual guarantees in software modules. Meyer first formally described Design by Contract in 1986, in the technical report Design by Contract (TR-EI-12/CO), published by Interactive Software Engineering Inc. as part of the design specifications for the Eiffel programming language. This introduction coincided with the development of Eiffel, which Meyer conceived in 1985 to promote object-oriented programming with built-in support for reliability mechanisms. The methodology emerged amid growing concerns over software reliability in the 1980s, a period marked by high-profile failures in complex systems that highlighted the limitations of ad-hoc debugging and testing practices. By integrating DbC into Eiffel's syntax and semantics, Meyer aimed to shift software development toward a more verifiable and maintainable paradigm, where errors could be anticipated and localized through explicit specifications rather than discovered post-deployment. Central to Meyer's innovation was the business metaphor, which analogized software interactions to legal agreements between parties, imposing mutual responsibilities on callers and callees in a subroutine or method. In this model, a client (the calling code) must satisfy preconditions to invoke a supplier (the routine), while the supplier guarantees postconditions upon successful execution, fostering and reducing in component interfaces. This not only clarified the division of labor in but also aligned with principles, enabling developers to treat assertions as enforceable clauses that could detect violations at runtime. In recognition of its significance, "Design by Contract" was registered as a trademark by Eiffel Software in December 2004, following an application in December 2003, underscoring its proprietary role in the Eiffel ecosystem.

Evolution and Standardization

Following its introduction in the Eiffel programming language in the 1980s, Design by Contract (DbC) saw significant adoption in other languages during the 1990s, particularly through academic research and extensions that integrated it with object-oriented paradigms. Researchers explored DbC's application beyond Eiffel, influencing languages like Java, where assertions were added in Java 1.4 (2002) to support lightweight contract checking, though full DbC required libraries such as JML (Java Modeling Language). In parallel, DbC principles began shaping broader methodologies; by the late 1990s, it contributed to formal methods by providing a practical bridge between rigorous specification and implementation, as seen in extensions to Hoare logic for runtime verification. Its influence extended to agile practices in the 2000s, where DbC was combined with test-driven development (TDD) to form specification-driven development, enabling iterative refinement of contracts alongside code. Standardization efforts solidified DbC's role in the 2000s and 2010s. The Eiffel language, central to DbC, was formalized as ISO/IEC 25436:2006, which explicitly incorporates contract mechanisms like preconditions, postconditions, and invariants as core elements of the language standard. Similarly, Ada's 2012 ISO standard (ISO/IEC 8652:2012) introduced native support for preconditions and postconditions, marking a milestone in embedding DbC into a widely used language for safety-critical applications. Proposals for C++ followed, with contracts initially targeted for but deferred; by 2025, the P2900 proposal for a minimal viable product of contracts—covering preconditions, postconditions, and assertions—was advanced into the C++26 working draft at the February 2025 ISO C++ committee meeting, with ratification expected in 2026. Key milestones in the reflect growing library and native integrations. In Python, libraries like deal emerged around 2020 to provide DbC decorators for runtime checks, while a March 2025 Python Enhancement Proposal discussion advocated for native class invariants to enhance built-in support. Scala, building on its functional-object hybrid nature, incorporated contract features through libraries like ScalaCheck in the early . These developments underscore DbC's evolution from a niche Eiffel feature to a cross-language , influencing both tools and agile workflows without native implementations dominating .

Language Implementation

Native Language Support

Eiffel was the first programming language to provide full native support for design by contract, with its initial implementation available since early 1986. The language includes dedicated keywords for specifying preconditions (require), postconditions (ensure), and class invariants (invariant), enabling runtime assertion checking by default, though compile-time verification is also possible via tools like AutoProof. For example, a routine might be defined as:

feature divide (numerator, denominator: REAL): REAL require denominator_not_zero: denominator /= 0.0 do Result := numerator / denominator ensure correct_result: Result = numerator / old denominator end

feature divide (numerator, denominator: REAL): REAL require denominator_not_zero: denominator /= 0.0 do Result := numerator / denominator ensure correct_result: Result = numerator / old denominator end

This syntax enforces contracts at runtime during development and can be disabled in production for performance. Ada 2012 introduced native support for design by contract through aspect specifications, including preconditions (Pre), postconditions (Post), type invariants, and subtype predicates. These are specified in subprogram declarations using aspect clauses, with runtime checks enabled via compiler options such as GNAT's -gnata switch. For example:

function Square (A : Positive) return Positive with Post => Square'Result > A;

function Square (A : Positive) return Positive with Post => Square'Result > A;

This ensures the result of Square exceeds the input A. Ada's contracts align closely with the DbC model and are particularly used in safety-critical systems. The D programming language offers built-in contract programming through language constructs for preconditions, postconditions, and invariants, integrated since its initial design. These are specified using attributes like in for preconditions and out for postconditions, with runtime evaluation enabled via compiler flags (-checkaction=context for halting on violation). Compile-time checks occur where feasible, such as for constant expressions. An example function contract appears as:

int divide(int numerator, int denominator) in { assert(denominator != 0); } out(result; // can use 'result' to refer to return value { assert(result * denominator == numerator); } do { return numerator / denominator; }

int divide(int numerator, int denominator) in { assert(denominator != 0); } out(result; // can use 'result' to refer to return value { assert(result * denominator == numerator); } do { return numerator / denominator; }

This module enhances reliability without requiring external libraries. Oxygene, formerly known as Delphi Prism and developed for .NET platforms, provides native support for design by contract constructs including class contracts for preconditions, postconditions, and invariants. Introduced as a language innovation inspired by Eiffel, these features allow self-testing classes with runtime enforcement. Syntax uses sections like require and ensure within methods, as in:

method Divide(numerator, denominator: [Single): Single](/page/Single_&_Single); require DenominatorNotZero = denominator <> 0; ensure CorrectResult = result = numerator / denominator; begin result := numerator / denominator; end;

method Divide(numerator, denominator: [Single): Single](/page/Single_&_Single); require DenominatorNotZero = denominator <> 0; ensure CorrectResult = result = numerator / denominator; begin result := numerator / denominator; end;

Invariants are declared at the class level for ongoing validation. C++26 introduces native contract assertions as a recent standardization effort, with features included in the working draft as of November 2025 and expected in the full standard by 2026. These include attributes like [[expects]] for preconditions and [[ensures]] for postconditions, supporting runtime checking via compiler options while allowing future compile-time analysis. For instance:

int divide(int numerator, int denominator) [[expects: denominator != 0]] [[ensures: result * denominator == numerator]] { return numerator / denominator; }

int divide(int numerator, int denominator) [[expects: denominator != 0]] [[ensures: result * denominator == numerator]] { return numerator / denominator; }

This addition addresses long-standing requests for built-in contracts in C++, promoting safer code without altering existing syntax.

Library and Framework Support

In languages without native support for design by contract (DbC), third-party and frameworks provide mechanisms to implement preconditions, postconditions, and invariants through annotations, decorators, or instrumentation, enabling DbC without requiring changes to the compiler or runtime environment. These tools facilitate adoption in legacy codebases and promote practices by integrating contract checks at runtime or compile time. For C++, the Boost.Contract library offers comprehensive DbC support, including subcontracting, class invariants (including static and volatile variants), and postconditions that access old values and return results. It uses macros and lambda expressions to define s, allowing customizable failure handling such as throwing exceptions or terminating execution. A simple example demonstrates and postcondition checks for an increment function:

cpp

#include <boost/contract.hpp> #include <limits> void inc(int& x) { boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x); boost::contract::check c = boost::contract::function() .precondition([&] { BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max()); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(x == *old_x + 1); }); ++x; }

#include <boost/contract.hpp> #include <limits> void inc(int& x) { boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x); boost::contract::check c = boost::contract::function() .precondition([&] { BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max()); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(x == *old_x + 1); }); ++x; }

This checks that x is not at its maximum before incrementing and verifies it increased by 1 afterward. In , historical libraries like jContractor (introduced in 2005) and Contract4J5 (last updated 2009, now dormant) enabled via reflective bytecode instrumentation and annotations, respectively, supporting contract inheritance where subclasses can weaken preconditions and strengthen postconditions. jContractor uses standard Java methods following a (e.g., pre_myMethod()) for contracts, which are instrumented at class loading to enforce runtime checks without modifying . Contract4J5 leverages Java 5 annotations and for weaving contract logic, marking classes with @Contract and methods with @Pre, @Post, or @Invar. An example from Contract4J5 illustrates invariant and enforcement:

java

import com.contract4j5.Contract; import com.contract4j5.Pre; import com.contract4j5.[Invar](/page/Invar); @Contract public class MyClass { @[Invar](/page/Invar)("name != null") private String name; @Pre("n != null") public void setName(String n) { name = n; } @Post("$return != null") public String getName() { return name; } }

import com.contract4j5.Contract; import com.contract4j5.Pre; import com.contract4j5.[Invar](/page/Invar); @Contract public class MyClass { @[Invar](/page/Invar)("name != null") private String name; @Pre("n != null") public void setName(String n) { name = n; } @Post("$return != null") public String getName() { return name; } }

This ensures the name field remains non-null as an invariant and rejects null inputs to setName. More recent efforts include projects like C4J, but adoption remains limited. For Python, PyContracts (last updated around 2020) provides decorator-based DbC with a domain-specific language for constraints, supporting type checking, arithmetic conditions, and variable binding in function annotations or docstrings. It allows disabling checks in production for zero overhead and includes specialized support for libraries like NumPy. Contracts are specified using the @contract decorator, as in this matrix multiplication example:

python

import numpy from contracts import contract @contract def matrix_multiply(a, b): '''Multiplies two matrices together. :param a: The first matrix. Must be a 2D [array](/page/Array). :type a: array[MxN],M>0,N>0 :param b: The second matrix. Must be of compatible dimensions. :type b: array[NxP],P>0 :rtype: array[MxP] ''' return numpy.dot(a, b)

import numpy from contracts import contract @contract def matrix_multiply(a, b): '''Multiplies two matrices together. :param a: The first matrix. Must be a 2D [array](/page/Array). :type a: array[MxN],M>0,N>0 :param b: The second matrix. Must be of compatible dimensions. :type b: array[NxP],P>0 :rtype: array[MxP] ''' return numpy.dot(a, b)

Here, it verifies a and b are compatible 2D arrays with positive dimensions and ensures the result is a valid MxP array. As of 2025, proposals for native DbC support in Python, such as class invariants, are under discussion. Microsoft's Code Contracts framework for .NET languages like C# extends support to interoperable scenarios, such as wrappers, by specifying contracts via attributes and static analysis tools that rewrite code for runtime verification. This allows .NET assemblies to enforce preconditions and invariants across managed and native boundaries without full recompilation. For and , the Decorator Contracts library by Michael Haufe, published in mid-2025, provides a comprehensive implementation of Design by Contract support using decorators, serving as a superior and actively maintained alternative to earlier tools. It targets web applications where native support is absent, enforcing preconditions via @demands, postconditions via @ensures, and class invariants via @invariant, while supporting principles such as the Liskov substitution principle through subcontracting and a Contracted base class with Proxy-based enforcement. The library includes a checked mode for runtime toggling of contract verification, ensuring low overhead in production. At version 1.0.0 as of 2026, it remains current and feature-rich. An example demonstrates contract enforcement for a simple Stack class:

javascript

import { demands, ensures, invariant } from '@final-hill/decorator-contracts'; class Stack { @invariant('this.items.length >= 0') constructor() { this.items = []; } @demands('item !== undefined') @ensures('this.items.length === __old__.items.length + 1') push(item) { this.items.push(item); } }

import { demands, ensures, invariant } from '@final-hill/decorator-contracts'; class Stack { @invariant('this.items.length >= 0') constructor() { this.items = []; } @demands('item !== undefined') @ensures('this.items.length === __old__.items.length + 1') push(item) { this.items.push(item); } }

These libraries bridge the gap to native DbC support by retrofitting contracts into existing ecosystems, improving code reliability in widely used languages, though many are historical or require evaluation for current maintenance.

Practical Implications

Performance and Optimization

Design by contract (DbC) implementations introduce runtime overhead due to the evaluation of preconditions, postconditions, and invariants during program execution, particularly in debug modes where checks are enabled. This overhead varies widely depending on the application and assertion complexity, as observed in benchmarks for runtime assertion checking tools like RTC on C programs. Additionally, code generation for assertions increases binary size, though this space overhead is typically modest and can be mitigated in optimized builds. To address performance concerns in production environments, DbC languages and libraries support disabling contract checks in release configurations. In C++, the NDEBUG macro, defined via compiler flags, eliminates assertion code entirely, preventing any runtime or space overhead. Similarly, Eiffel's compiler options allow turning off assertion monitoring globally or per class, such as disabling postconditions and invariants while retaining preconditions, ensuring negligible impact when checks are inactive. Modern compilers incorporate optimizations to reduce DbC costs even when checks are active. Compile-time evaluation of constant conditions in assertions avoids unnecessary runtime computations, a feature supported in languages like Eiffel and enhanced in C++ through static analysis. The proposed C++26 contracts (P2900) enable partial evaluation and constant propagation for contract assertions during compilation, further minimizing overhead by simplifying or eliding provably true checks. These strategies highlight key trade-offs in : enhanced reliability through rigorous verification versus potential speed degradation in unoptimized modes. Benchmarks in Eiffel-based systems demonstrate that disabling assertions in production yields nearly identical to non-DbC , preserving speed without sacrificing debug-time benefits. Recent advancements in the , such as static analysis-driven simplification of assertions in tools like Prusti for , further reduce overhead by proving subsets of contracts at . In production, complements dynamic testing by providing lightweight, configurable checks that can be tuned for minimal intrusion.

Integration with

Design by contract (DbC) integrates seamlessly with software testing by embedding specifications directly into the code, functioning as runtime assertions that serve as automated test oracles. These contracts—preconditions, postconditions, and class invariants—continuously validate the software's behavior during execution, detecting violations immediately without requiring separate test suites. This approach transforms the program into a self-testing , where any contract failure indicates a deviation from expected behavior, thereby catching bugs early in the development process. Unlike traditional testing methods, which rely on reactive, external harnesses like unit tests or integration suites to verify outputs after execution, DbC is proactive and built-in, enforcing specifications at key points such as routine entry and exit. Traditional tests often require explicit test cases to cover scenarios, including edge cases, whereas contracts implicitly address these by defining valid states and outcomes, reducing the need for exhaustive manual design. This distinction allows DbC to complement rather than replace conventional testing, providing continuous validation during normal operation. Synergies between DbC and testing are evident in tools that leverage contracts for automated test generation. For instance, Eiffel's AutoTest tool uses to systematically generate valid inputs through random and adaptive techniques, such as precondition satisfaction and stateful exploration, while postconditions and invariants act as the to verify results. This enables fully automated testing of object-oriented code, uncovering faults in production libraries by exercising features that manual tests might overlook. The benefits of this integration include reduced test maintenance, as changes to specifications automatically update the testing behavior without modifying separate test code, and enhanced coverage in object-oriented designs by ensuring interactions between components adhere to contracts. In empirical studies, has been shown to decrease the required number of unit tests by providing verifiable assertions that serve as oracles, allowing developers to focus on fewer, higher-level tests while maintaining reliability. Overall, this leads to more efficient testing processes, particularly in large-scale systems where manual test proliferation becomes burdensome. A practical example illustrates the diagnostic power of contracts: a postcondition failure in a routine signals a bug within the callee itself, as the inputs satisfied the precondition but the output violated the expected result. Conversely, a precondition failure points to an issue in the caller, which provided invalid arguments, thus localizing the fault to the appropriate subsystem without additional debugging overhead.

Advanced Applications and Criticisms

Relation to Formal Verification

Design by Contract (DbC) is fundamentally rooted in axiomatic semantics and Hoare logic, which provide a mathematical framework for reasoning about program correctness through preconditions, postconditions, and invariants. In Hoare logic, a program's behavior is captured by triples of the form {P} S {Q}, where P is the precondition, S the statement or routine, and Q the postcondition, enabling deductive proofs of correctness. DbC adapts this by treating these assertions as enforceable contracts that suppliers must satisfy if clients meet their obligations, serving as lightweight formal specifications that bridge informal development practices with rigorous verification. This connection allows DbC annotations to function as partial specifications input to theorem provers, facilitating proofs of properties like loop invariants without full axiomatic overhaul. Integration with formal verification tools elevates DbC from runtime assertion checking to static proof generation. For Eiffel programs, the AutoProof environment translates DbC contracts into logical formulas verified by backends like Why3, Boogie, and Z3, enabling compile-time confirmation that routines satisfy their specifications without execution. Similarly, for C code, Frama-C employs the ANSI/ISO C Specification Language (ACSL), inspired by DbC principles, where annotations are discharged via the Weakest Precondition (WP) plugin using SMT solvers for deductive verification. These tools treat contracts as axioms in a proof system, automatically generating verification conditions to establish properties such as absence of runtime errors or adherence to functional requirements. Unlike traditional DbC runtime checks, which detect violations dynamically, this static approach provides exhaustive guarantees by exploring all possible execution paths mathematically. Recent advancements include the use of generative AI to automate the creation of contracts. As of 2024, methods leveraging large language models can infer pre- and postconditions for methods, facilitating broader adoption of by reducing the manual effort required for specification writing. These AI-assisted approaches integrate with pipelines, enhancing scalability for large codebases. In advanced applications, contracts enhance for concurrent or state-based systems, where bounded model checking tools encode pre- and postconditions to explore finite state spaces for property violations. For instance, Java Modeling Language (JML) contracts—directly based on —have been verified using bounded model checkers like CPAChecker to prove modular correctness in object-oriented designs. This is particularly valuable in safety-critical domains like , where Frama-C has certified C components in flight software by proving ACSL contracts against standards such as , ensuring no specification breaches under all inputs. To illustrate, verifying a sorting routine might involve a that the input is a valid and a postcondition that the output is sorted while preserving elements; AutoProof then discharges obligations like loop invariants (e.g., partial sortedness after each iteration) using theorem proving, confirming correctness exhaustively. These methods differ from empirical by offering mathematical certainty, though they complement it as a more rigorous layer for critical components.

Limitations and Adoption Challenges

One significant challenge in applying Design by Contract (DbC) is the generation of for assertions, which can increase software complexity and potentially reduce overall reliability by introducing redundant error-checking mechanisms. Additionally, specifying contracts for non-deterministic behaviors, such as those involving dynamic binding in object-oriented systems, poses difficulties, as redefined routines may violate class invariants and lead to inconsistent states. Adoption of faces barriers including a steep , where developers must grasp and assertion semantics to implement it effectively. It is particularly limited in procedural or paradigms, which lack the object-oriented structures central to DbC's mutual obligations and constraints. In performance-critical domains, resistance arises from runtime overhead associated with assertion monitoring, often ranging from 25% to 100%, making it less viable for real-time or resource-constrained applications. Critics argue that over-reliance on contracts can mask underlying poor design choices, as the focus on specifications may divert attention from architectural flaws. Furthermore, evolving software specifications introduce maintenance overhead, with redundant checks and complex complicating updates and integrations. In modern contexts, encounters gaps in scalability for architectures, where distributed interactions amplify contract enforcement challenges in event-sourced systems. Overall, DbC's adoption is limited outside languages like Eiffel, as extensions for others often become discontinued owing to high maintenance costs and lack of native support. To mitigate these issues, hybrid approaches combining with (TDD) have been proposed, leveraging TDD's iterative testing to complement contract specifications and reduce upfront rigidity. Evolving tools, such as annotation-based utilities for auto-generating contracts in domain-driven designs, aim to alleviate boilerplate and integration burdens, promoting more sustainable use.

References

  1. https://se.inf.ethz.ch/~meyer/publications/old/dbc_chapter.pdf
  2. https://archive.eiffel.com/doc/manuals/technology/contract/
  3. https://www.researchgate.net/publication/220475937_Design_by_Contract_The_Lessons_of_Ariane
  4. https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html
  5. https://blog.frankel.ch/programming-by-contract-jvm/
  6. https://se.inf.ethz.ch/~meyer/publications/computer/contract.pdf
  7. https://dl.acm.org/doi/10.1145/3626201
  8. https://se.inf.ethz.ch/research/autoproof/tutorial/downloads/tutorial.pdf
  9. https://archive.eiffel.com/general/people/meyer/publications/publications.html
  10. https://www.eiffel.com/values/design-by-contract/
  11. https://people.eecs.ku.edu/~saiedian/Teaching/811/Papers/Agile-Development/formal-agile-fittest.pdf
  12. https://github.com/life4/deal
  13. https://discuss.python.org/t/design-by-contract-in-python-proposal-for-native-class-invariants/85434
  14. https://se.inf.ethz.ch/~meyer/publications/eiffel/eiffel_jss.pdf
  15. https://www.eiffel.org/doc/eiffel/ET-_Design_by_Contract_%2528tm%2529%252C_Assertions_and_Exceptions
  16. https://dlang.org/spec/contracts.html
  17. https://www.remobjects.com/page.aspx?id=%257BE10F7F5C-AE94-4833-9E4B-2EDD5ED69768%257D
  18. https://www.remobjects.com/elements/oxygene/evolution
  19. https://docs.elementscompiler.com/Concepts/ClassContracts/
  20. https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2025/p2899r1.pdf
  21. https://en.cppreference.com/w/cpp/language/contracts.html
  22. https://www.modernescpp.com/index.php/contracts-in-c26/
  23. https://softwareengineering.stackexchange.com/questions/147520/options-for-programming-by-contract-in-java
  24. https://www.boost.org/libs/contract/doc/html/index.html
  25. https://link.springer.com/article/10.1007/s10703-005-3400-1
  26. https://github.com/C4J-Team/C4J
  27. https://github.com/AndreaCensi/contracts
  28. https://andreacensi.github.io/contracts/tour.html
  29. https://learn.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts
  30. https://www.npmjs.com/package/@final-hill/decorator-contracts
  31. https://www.osti.gov/pages/servlets/purl/1477830
  32. https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2025/p2900r13.pdf
  33. https://www.prusti.dev/
  34. https://www.eiffel.org/doc/eiffelstudio/Testing-_Background_and_basics
  35. https://www.sciencedirect.com/topics/computer-science/design-by-contract
  36. https://se.inf.ethz.ch/research/autotest/
  37. https://dl.acm.org/doi/10.1145/2023607.2023635
  38. https://se.inf.ethz.ch/~meyer/publications/theory/09-axiom.pdf
  39. https://se.inf.ethz.ch/~meyer/down/touch/TOUCH.pdf
  40. https://arxiv.org/pdf/1704.04189
  41. https://frama-c.com/download/acsl.pdf
  42. https://dl.acm.org/doi/10.1145/3689484.3690738
  43. https://formal.kastel.kit.edu/biblio/researcher/ulbrich/pdf/BeckertKirstenEA20.pdf
  44. https://cacm.acm.org/research/the-dogged-pursuit-of-bug-free-c-programs/
  45. https://www.jot.fm/issues/issue_2005_09/article2.pdf
  46. https://www.mdpi.com/2079-9292/14/21/4205
  47. https://www.researchgate.net/publication/221610881_Combining_Contract-Based_Development_and_Test-Driven_Development
Add your contribution
Related Hubs
User Avatar
No comments yet.