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?

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.

Subtype predicates: Ada 2012 has generalized the subrange mechanism by allowing programmers to define object constraints (known as subtype predicates) that are not necessarily contiguous ranges. For example:

Subtype predicates may be specified through compile-time known values as shown above, in which case they are known as static predicates, or through run-time computed expressions (for 'dynamic predicates'). Dynamic predicates allow more flexibility in their definition than static predicates but are usable in fewer contexts. The following example illustrates a dynamic predicate:

Private types: A product contract may include a disclaimer that voids the warranty if the product is misused. This has a direct analogue in software: the integrity of a data object may be compromised unless the manipulation of the object is restricted. The following example illustrates this point, with a record type (similar to a struct in C or C++) that represents a date:

A major problem with this type definition is that it allows the programmer to construct nonsensical Date values:

Some_Day : Date_Pkg.Date := (Feb, 28, 2013); OK
Some_Day.D := 29; (Feb, 29, 2013), not OK

Such misuses can be prevented by declaring Date as a private type (Ada's terminology for an encapsulated type) and then declaring appropriate operations to construct and manipulate Date values. The full declaration of Date appears later in the package and is inaccessible outside the package implementation:

With a private type, data coherence cannot be violated by 'client' code that manipulates Date objects, since such code does not have access rights to the representation as a record type.

The private type facility in Ada is not new; it has been in the language since the earliest version of the standard.

Type invariants: In the skeletal example in the previous section, the private type declaration guarantees data coherence by limiting the processing of Date values to the invocation of operations that are defined in the same package as the type. In effect, data coherence is a postcondition for these operations.

That is all for the good, but the meaning of data coherence is implicit. It is preferable to have an explicit mechanism for specifying and enforcing the data coherence condition, and such a facility has been added in Ada 2012. A private type may be declared with a type invariant: a Boolean expression that serves as a postcondition for each operation that can be applied by 'consumer' code.

Here is the Date example with a type invariant, with operations to construct a date and to select and modify its components.

The invariant condition for Date (the Is_Legitimate function) is checked on return from To-Date and Set_Date, thus guaranteeing that malformed dates such as (Feb, 29, 2013) are prevented.

Increasing trust through contracts
Contracts are essential in real life to prevent misunderstandings of responsibilities, and they are equally important in software for the same reason: What does some operation expect, and what result will it deliver?; What is the constraint or 'steady state' condition for objects of a given type?

Ada 2012 provides standard syntax for expressing such requirements, integrated into the language's existing data type and subprogram framework, with checks performed either statically or dynamically. Similar contracts, with static enforcement, have been an essential part of the Ada-based SPARK language for many years, and the upcoming new version known as SPARK 2014 [3] will be integrating the Ada 2012 syntax.

With the ever-increasing role of software in critical fields, expressing contracts-in source code is an idea whose time has come. The new Ada 2012 language provides an effective solution and, unlike real life where contracts may require hiring legal experts, no language lawyers will be needed.

1. B. Meyer, Object-Oriented Software Construction (Second Edition). Prentice Hall PTR; 1997.
2. Ada 2012 Language Reference Manual.
3. SPARK 2014.

About the author
Dr. Benjamin Brosgol is a senior member of the technical staff of AdaCore. He has been involved with programming language design and implementation for more than 30 years, concentrating on languages and technologies for high-integrity systems. Dr. Brosgol was a member of the design team for Ada 95, and he has also served in the Expert Groups for several Java Specification Requests. He has presented papers and tutorials on safety and security certification on numerous occasions including ESC (Embedded Systems Conference), ICSE (IEEE/ACM International Conference on Software Engineering), SSTC (Systems & Software Technology Conference), ACM SIGAda, and Ada-Europe. Dr. Brosgol holds a BA in Mathematics from Amherst College, and MS and PhD degrees in Applied Mathematics from Harvard University.

To download the PDF version of this article, click here.

?First Page?Previous Page 1???2

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