Global Sources
EE Times-Asia
Stay in touch with EE Times Asia
EE Times-Asia > Embedded

Understanding contract-based programming

Posted: 11 Sep 2013 ?? ?Print Version ?Bookmark and Share

Keywords:contract-based programming? assertions? precondition? postcondition? Ada 2012?

The elements of 'contract-based programming'assertions of program properties that are part of the source texthave been available in some programming languages for many years. However, it moved into the mainstream of software development only recently. 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 realised in the latest version of the Ada language standard, Ada 2012 [2], 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:

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.

1???2?Next Page?Last Page

Article Comments - Understanding contract-based program...
*? You can enter [0] more charecters.
*Verify code:


Visit Asia Webinars to learn about the latest in technology and get practical design tips.

Back to Top