Contract-based programming: making software more reliable - Embedded.com

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 [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:

  type Float_Array is array (Integer range <>) of Float;
  — Different objects may have different lengths
 
  function Max( A : Float_Array ) return Float
  with
    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
  begin
    … — Algorithm to compute max value
  end Max;

  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.

Augusta Ada King, Countess of Lovelace, who programmed the first mechanical computer in the 1800's, and for whom the Ada programming language was named.Design by contract is a main feature of Ada 2012.

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 subrangemechanism by allowing programmers to define object constraints (known assubtype predicates) that are not necessarily contiguous ranges. Forexample:

  type Month is (Jan, Feb, Mar, Apr, May, Jun, Jul, Aug, Sep, Oct, Nov, Dec);
  subtype Month_30 is Month
  with Static_Predicate =>
    Month_30 in Apr | Jun | Sep | Nov;

  M1 : Month_30; — Constrained to Apr, Jun, Sep, or Nov
  M2 : Month := Dec;
  …
  M1 := Sep; — OK
  M1 := M2; — Run-time check, raises exception if M2 not in Month_30

Subtypepredicates may be specified through compile-time known values as shownabove, in which case they are known as static predicates, or throughrun-time computed expressions (for ‘dynamic predicates’). Dynamicpredicates allow more flexibility in their definition than staticpredicates but are usable in fewer contexts. The following exampleillustrates a dynamic predicate:

  type Hemisphere is (Northern, Southern);
  Local_Hemisphere : Hemisphere := …; — Initialize based on locale

  subtype Summer_Month is Month
  with Dynamic_Predicate =>
    (case Local_Hemisphere is
      when Northern =>
        Summer_Month in Jun .. Aug,
      when Southern =>
        Summer_Month in Dec | Jan | Feb);

  S : Summer_Month := Jun; — Raises exception if Local_Hemisphere = Southern

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

  package Date_Pkg is
    type Month is (Jan, Feb, Mar, Apr, May, Jun,
                   Jul, Aug, Sep, Oct, Nov, Dec);
    subtype Day is Integer range 1..31;
    subtype Year is Integer range 1801..2100;

  type Date is
    record
      M : Month;
      D : Day;
      Y : Year;
    end record;
  end Date_Pkg;

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

Suchmisuses can be prevented by declaring Date as a private type (Ada’sterminology for an encapsulated type) and then declaring appropriateoperations to construct and manipulate Date values. The full declarationof Date appears later in the package and is inaccessible outside thepackage implementation:

  package Date_Pkg is
    type Month is (Jan, Feb, Mar, Apr, May, Jun,
                   Jul, Aug, Sep, Oct, Nov, Dec);
    subtype Day is Integer range 1..31;
    subtype Year is Integer range 1801..2100;

    type Date is private;

    … — Operations for Date

  private
    type Date is
      record
        M : Month;
        D : Day;
        Y : Year;
      end record;
  end Date_Pkg;

Witha private type, data coherence cannot be violated by ‘client’ code thatmanipulates Date objects, since such code does not have access rightsto 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 typedeclaration guarantees data coherence by limiting the processing of Datevalues to the invocation of operations that are defined in the samepackage as the type. In effect, data coherence is a postcondition forthese operations.

That is all for the good, but the meaning ofdata coherence is implicit. It is preferable to have an explicitmechanism for specifying and enforcing the data coherence condition, andsuch a facility has been added in Ada 2012. A private type may bedeclared with a type invariant: a Boolean expression that serves as apostcondition 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.

  package Date_Pkg is
  type Month is (Jan, Feb, Mar, Apr, May, Jun,
                 Jul, Aug, Sep, Oct, Nov, Dec);
  subtype Day is Integer range 1..31;
  subtype Year is Integer range 1801..2100;

  type Date is private;
  with Invariant => Is_Legitimate(Date);

  function M(X : Date) return Month;
  function D(X : Date) return Day;
  function Y(X : Date) return Year;
  function Is_Leap_Year(Y : Year) return Boolean;

  function Is_Legitimate(X : Date) return Boolean is
    (if M(X) in Month_30 then
      D(X) <= 30
    elsif M(X) = Feb and Is_Leap_Year(Y(X)) then
      D(X) <= 29
    elsif M(X) = Feb and not Is_Leap_Year(Y(X)) then
      D(X) <= 28);   function To_Date(M : Month; D : Day; Y : Year) return Date;   procedure Set_Date(X : out Date; M : in Month; D : in Day; Y : in Year);   private
    type Date is
      record
        M : Month;
        D : Day;
        Y : Year;
      end record;
  end Date_Pkg;

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
Contractsare essential in real life to prevent misunderstandings ofresponsibilities, and they are equally important in software for thesame 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?

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

Withthe ever-increasing role of software in critical fields, expressingcontracts-in source code is an idea whose time has come. The new Ada2012 language provides an effective solution and, unlike real life wherecontracts may require hiring legal experts, no language lawyers will beneeded.

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

Dr. Benjamin Brosgol is a senior member of the technical staff of AdaCore. He has beeninvolved with programming language design and implementation for morethan 30 years, concentrating on languages and technologies forhigh-integrity systems. Dr. Brosgol was a member of the design team forAda 95, and he has also served in the Expert Groups for several JavaSpecification Requests. He has presented papers and tutorials on safetyand security certification on numerous occasions including ESC (EmbeddedSystems Conference), ICSE (IEEE/ACM International Conference onSoftware Engineering), SSTC (Systems & Software TechnologyConference), ACM SIGAda, and Ada-Europe. Dr. Brosgol holds a BA inMathematics from Amherst College, and MS and PhD degrees in AppliedMathematics from Harvard University.

4 thoughts on “Contract-based programming: making software more reliable

  1. I do enjoy reading this article very much. Thank you for providing it.

    The object declaration “T : Test_Score;” seems to violate the Ada syntax rules. Was it a typo?

    Anh Vo

    Log in to Reply
  2. The analogies you used to clarify the purpose and application of each contract element are very helpful in understanding and appreciating the Ada-2012 contract model. I especially like the analogy of private types as a way of enforcing the warranty on a p

    Log in to Reply
  3. This was a very interesting article but of little practical use beingst that so few of us use Ada (which obviously helps enforce the pre/post-conditions). How about another version of the article translated to C or C++?

    Log in to Reply

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.