Ada Programming/Contract Based Programming

Computing » Computer Science » Computer Programming » Ada Programming

---

This language feature has been introduced in Ada 2012.

Contract Based Programming in Ada 2012

Among the additions to Ada 2012, a number of aspects follow the common theme of ‘formal’ contracts on types and subprograms. The formality here is referring to symbolic logic integrated with existing features of Ada. Contracts endow the language with expressive features similar to those of Eiffel's Design by Contract™, SPARK, or those connected with LSP.

Since specifying contracts involves several parts of the Ada language, also since obeying contracts on the part of the compiler does so, too, the topic of contracts is addressed in several parts of the language reference. A comprehensive, more focused view, is a subject of the latest edition of the Ada Rationale.

Parts of the contracts can be about statically known properties of the program, while others would be checked only at run-time. In the first case, the formal parts of the contract may be analyzed not just by the Ada compiler, but also by proof tools. The assurance resulting from the analysis can be that certain undesirable properties will be absent from the program. For example, the program might then be known to not raise exceptions.

This overview will only outline syntax and variants by example while referring to existing wikibook entries and other resources for explanations of contracts in general.

Preconditions and Postconditions of Subprograms

Considering functions, for example, their specification gives the type of the return value as part of the parameter profile. One way of informing about the specifics of the return value of the function is to give a mathematical (in style) expression of the result, which is thus guaranteed by this clause of the contract. A contract may also specify conditions that say what must be true of objects entering the computation in order for the function to produce its result. In contracts, the return value is named function_name'Result.

  function Sum (A, B : Number) return Number
  with
    Post => (if
               A <= 0.0 and B >= 0.0
             then
               Sum'Result = A + B);

An alternative mode of expression emphasizes the pre-requisites,

  function Sum (A, B : Number) return Number
  with
    Pre  => A <= 0.0 and B >= 0.0,
    Post => Sum'Result = A + B;

The first example leaves unsaid what happens when the condition evaluates to False. By default, when an assertion fails, and if the current Assertion_Policy is Check, Assertion_Error is raised. (The current amendment process of Ada is considering “raise expressions” (8652/0117): should the condition not be True, these permit raising a specific exception as an else part, with a corresponding specific message instead of defaulting as just outlined.) The second example expressly obliges, in Pre, the caller to ensure that both A and B will have the specified properties of being Numbers and of being no greater than 0.0 and no less than 0.0, respectively. This way the Pre aspect is stating that in case the condition is False, the function cannot fulfill its contractual obligation as given in Post.

Assertions About Types And Subtypes

Ada types may be declared to have a type invariant. This kind of predicate applies to private types. Hence, its expression may only refer to other publicly visible features of the type. The type's name here denotes the current instance of the type.

  type Stack is private
      with Type_Invariant => Count(Stack) >= 0;

As detailed in 3.2.4: Type Invariants ^[Annotated], invariants may also be given for a derivation class of types, using aspect name Type_Invariant'Class, to apply to all types in a hierarchy.

A predicate may also be given when declaring a subtype. In this case, the expression (of a boolean type) states properties of the subtype (see 3.2.4: Subtype Predicates ^[Annotated] for details) and its truth would be checked at certain points. When a predicate should be tested by the compiler, its aspect is named Static_Predicate, and Dynamic_Predicate otherwise. Roughly, then, checks are performed when a type conversion takes place, or when a parameter is passed, or when an object is created.

When deriving subtypes, the predicate that applies is the conjunction of the predicates on the subtypes involved.

Assertion Policies

The language reference manual extends the Assert pragma and its associated Assertion_Policy to also cover aspects of contract based programming in 11.4.2: Pragmas Assert and Assertion_Policy ^[Annotated]. Each ‘section’ of a contract, such as Pre, can be turned on and off for checking. This is done by specifying the desired Assertion_Policy, as locally or as globally as is desired. The following line turns checks on for aspect mark Pre:

  pragma Assertion_Policy (Pre => Check);

Implementations of Ada are free to provide more policy identifiers than the two defined by the language, Check and Ignore.

A setting that affects all possible assertion aspects at the same time omits giving aspect marks.

  pragma Assertion_Policy (Check);