# Ada Programming/Contract Based Programming


## 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.[^1]

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`.

`  `` Sum (A, B : Number) `` Number`\
`  `\
`    Post => (`\
`               A <= 0.0 `` B >= 0.0`\
`             `\
`               Sum'Result = A + B);`

An alternative mode of expression emphasizes the pre-requisites,

`  `` Sum (A, B : Number) `` Number`\
`  `\
`    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  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
`Number`s 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.

`  `` Stack `` `\
`      `` Type_Invariant => Count(Stack) >= 0;`

As detailed in
, 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
 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
.
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`:

`  `` 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.

`  `` Assertion_Policy (Check);`

## References


[^1]: Ada Rationale, Contracts and
    Aspects
