Contract-based programming: making software more reliable
The elements of 'contract-based programming' – assertions of program properties that are part of the source text – have been available in some programming languages for many years but have only recently moved into the mainstream of software development. The latest version of the Ada language standard, Ada 2012, has added contract-based programming features that can be verified either dynamically with run-time checks, or statically through formal analysis tools. Both approaches help make programs more reliable by preventing errors from getting into production code.
Contracts for business
In everyday life a service or a product typically comes with a contract or warranty: an agreement in which one party promises to supply the service or product for the benefit of some other party. An effective contract for a service specifies two kinds of requirements:
- A precondition that the consumer must meet in order for the service to be performed; i.e., the minimum requirements on the consumer (for example cleaning the walls before they can be painted), and
- A postcondition that the server must meet in order for the service to be acceptable; i.e., the minimum requirements on the server (for example guaranteeing that the painted surfaces will not peel for some specified amount of time).
From a different perspective, the precondition is the maximum that the server should expect from the consumer before performing the service, and the postcondition is the maximum that the consumer should expect from the server as a result.
A contract or warranty for a product is somewhat analogous. Viewed abstractly, a product is an object that is accessed or manipulated through services (operations) that the consumer requests/performs. A product’s contract thus includes the pre- and postconditions for the services that it provides.
But typically a product’s contract also includes disclaimers that void the warranty if the consumer misuses the product, for example by dismantling an appliance. And a contract may also specify the product’s 'steady state' condition: an invariant that must be met after any of the operations is performed.
The invariant is effectively a postcondition for each operation, to ensure that the product is in an internally consistent state, although the condition might be violated while the operation is in progress. As an example, an invariant for a toaster might be that the bread holder is either completely up or completely down. This condition is satisfied after each operation (lowering the bread, raising the bread, etc.) but is not met while the lowering or raising is in progress.
Contracts for software
As explained by Meyer in the context of the Eiffel language [1, pp. 337ff], the contract concept can be applied to software. We can look at a system’s architecture as a collection of interrelated modules, where program execution entails creating objects of various types (products) and interacting with them through operations (services). In the case of contract-based programming, the 'consumer' is a module that manipulates objects and invokes operations; a 'server' is a module that defines an object’s type or operations. The same module can play different roles at different times.
These concepts are realized in the latest version of the Ada language standard, Ada 2012 , which provides explicit contract syntax for both operations and types.
Software service contracts
Operations in Ada are parameterizable subprograms (procedures or functions), and preconditions and postconditions are manifested through Boolean expressions that are associated with the subprogram’s declaration. Here is an example of a simple function that computes the maximum in an array of Float values, with pre- and postconditions establishing the function’s contract:
type Float_Array is array (Integer range <>) of Float;
-- Different objects may have different lengths
function Max( A : Float_Array ) return Float
Pre => A'Length > 0,
Post => (for all F of A => F <= Max'Result) and
(for some F of A => F = Max'Result);
function Max( A : Float_Array ) return Float is
… -- Algorithm to compute max value
A1 : Float_Array(1..5) := (-10.0, 20.34, -123.45, 0.0, 0.0);
F1 : Float := Max(A1); -- 20.34
A2 : Float_Array(1..0); -- No elements in A2
F2 : Float := Max(A2): -- Precondition violation, since A2'Length=0
The syntax should be self-explanatory, with the precondition requiring that the Float_Array parameter have at least one element, and the postcondition reflecting the intent that the returned value be the maximum value found in the array.
One of the major benefits of pre- and postcondition contracts is that they define the semantics of the operation: what the operation expects from its parameters and what it computes as a result. In most languages this intent would need to be conveyed through comments. With a standard syntax for expressing such semantics, Ada 2012 allows the intent to be verified in several ways:
- at run time, with assertion checks ensuring that the precondition is satisfied on entry and that the postcondition is satisfied on return. Violation of either of these conditions will raise an exception;
- through formal static analysis by a tool that checks that the precondition is met at each call, and that the postcondition is met based on the implementation of the operation;
- through manual code review, if the run-time assertion checks are not enabled. Even in this case, the standard syntax, with support for quantification, can assist the verification process.
Software product contracts
Products correspond to instances of data types. Ada supports type-based contracts in several ways.
Scalar subranges One simple form of contract, borrowed from Pascal, has been part of Ada since the earliest version of the language standard: the ability to specify scalar subranges, with run-time checks guaranteeing that the range constraint is obeyed on assignment and similar operations. For example:
Test_Score : Integer range 0..100;
T : Test_Score;
T := some_expr; -- Run-time check that some_expr is in 0..100
The ability to explicitly define the constraints on scalar data makes code easier to understand and more amenable to static analysis, and the run-time enforcement of the constraints helps prevent vulnerabilities such as buffer overflow.