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 components request) and replies with a suitable error message if not.
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 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:
A clear metaphor to guide the design process
The application to inheritance, in particular a formalism for redefinition and dynamic binding
The application to exception handling
The connection with automatic software documentation
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.
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.
We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u
The students will acquire a solid knowledge on the processes necessary to design, write and use scientific software. Software design techniques will be used to program a multi-usage particles code, ai
Ce cours approfondit les connaissances en programmation présentées dans le cours ICC du 1er semestre. L'accent est
mis sur l'approche «orientée objet» (en C++), la conception et la spécification de pr
In computer programming, specifically when using the imperative programming paradigm, an assertion is a predicate (a Boolean-valued function over the state space, usually expressed as a logical proposition using the variables of a program) connected to a point in the program, that always should evaluate to true at that point in code execution. Assertions can help a programmer read the code, help a compiler compile it, or help the program detect its own defects.
Rust is a multi-paradigm, general-purpose programming language that emphasizes performance, type safety, and concurrency. It enforces memory safety—ensuring that all references point to valid memory—without requiring the use of a garbage collector or reference counting present in other memory-safe languages. To simultaneously enforce memory safety and prevent data races, its "borrow checker" tracks the object lifetime of all references in a program during compilation.
Swift is a high-level general-purpose, multi-paradigm, compiled programming language developed by Apple Inc. and the open-source community. First released in June 2014, Swift was developed as a replacement for Apple's earlier programming language Objective-C, as Objective-C had been largely unchanged since the early 1980s and lacked modern language features. Swift works with Apple's Cocoa and Cocoa Touch frameworks, and a key aspect of Swift's design was the ability to interoperate with the huge body of existing Objective-C code developed for Apple products over the previous decades.
Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...
Writing correct software is hard, yet in systems that have a high failure cost or are not easily upgraded like blockchains, bugs and security problems cannot be tolerated. Therefore, these systems are perfect use cases for formal verification, the task of ...
Capabilities are widely used in the design of software systems to ensure security. A system of capabilities can become a mess in the presence of objects and functions: objects may leak capabilities and functions may capture capabilities. They make reasonin ...