Subprogram Contracts
Subprogram Contracts in Ada 2012 and SPARK 2014
Originate in Floyd-Hoare logic (1967-1969)
a Hoare triple {P}C{Q}
P is the precondition before executing command C
Q is the postcondition after executing command C
Executable version by Meyer in Eiffel (1988)
Called Design by Contract ™
Precondition is checked dynamically before a routine starts
Postcondition is checked dynamically when a routine returns
SPARK 2014 combines both views
SPARK 2005 version was only logic, Ada version is only executable
Dynamic Execution of Subprogram Contracts
Contract on subprogram declaration
Different from subprogram body in general (but not always)
Ada Reference Manual allows implementations choice
Contract can be checked in the caller or in the callee
GNAT's choice is to execute in the callee
GNAT introduces wrappers in some cases for contracts
For an imported subprogram (e.g. from C) with a contract
For cases where contracts on static call/dispatching are different
Contracts are not enabled by default
Switch
-gnata
enables dynamic checking of contracts in GNAT
Dynamic Behavior when Subprogram Contracts Fail
Violation of contract raises an exception
Standard exception
Assertion_Error
is raised (same as for pragmaAssert
and all other assertions)Exception cannot be caught by subprogram's own exception handler implementation choice caller/callee has no effect
Idiom allows to select another exception
Control over sequencing of checks
Typical pre/post is a conjunction of Boolean conditions
Use and when no possible RTE, and then otherwise (recommended for SPARK)
Precondition
Better alternative to defensive programming, compare
and
Preconditions can be activated alone
pragma Assertion_Policy (Pre => Check);
Postcondition
Single place to check all return paths from the subprogram
Avoids duplication of checks before each return statement
Much more robust during maintenance
Only applies to normal returns (not in exception, not on abort)
Can relate input and output values
Special attribute
X'Old
for referring to input value of variableX
Special attribute
Func'Result
for referring to result of functionFunc
Special attribute
Rec'Update
orArr'Update
for referring to modified value of recordRec
or arrayArr
replaced by delta aggregate syntax in Ada 202X: (
Rec with delta Comp => Value
)
Contract Cases
Convenient syntax to express a contract by cases
Cases must be disjoint and complete (forming a partition)
Introduced in SPARK, planned for inclusion in Ada 202X
Case is (guard => consequence) with
'Old
/'Result
in consequenceCan be used in combination with precondition/postcondition
Both a precondition and a postcondition
On subprogram entry, exactly one guard must hold
On subprogram exit, the corresponding consequence must hold
Attribute 'Old
X'Old
expresses the input value ofX
in postconditionsSame as
X
when variable not modified in the subprogramCompiler inserts a copy of
X
on subprogram entry ifX
is large, copy can be expensive in memory footprint!X
can be a variable, a function call, a qualification (but not limited!)
Expr'Old
is rejected in potentially unevaluated contextpragma Unevaluated_Use_Of_Old (Allow)
allows itIn Ada, user is responsible – in SPARK, user can rely on proof
Implication and Equivalence
If-expression can be used to express an implication
(if A then B)
expresses the logical implicationA → B
(if A then B else C)
expresses the formula(A → B) (¬A → C)
(if A then B else C)
can also be used with B, C not of Boolean type(A <= B)
should not be used for expressing implication (same dynamic semantics, but less readable, and harmful in SPARK)
Equality can be used to express an equivalence
(A = B)
expresses the logical equivalence(A ↔ B)
A double implication should not be used for expressing equivalence (same semantics, but less readable and maintainable)
Reasoning by Cases
Case-expression can be used to reason by cases
Case test only on values of expressions of discrete type
Can sometimes be an alternative to contract cases
Can sometimes be used at different levels in the expression
procedure Open (F : in out File; Success : out Boolean) with
Post =>
Success = (case F.Mode'Old is
when Open => True,
when Active => False,
when Closed => F.Mode = Open);
Universal and Existential Quantification
Quantified expressions can be used to express a property over a collection of values
(for all X in A .. B => C)
expresses the universally quantified property(∀ X . X ≥ A ⋀ X ≤ B → C)
(for some X in A .. B => C)
expresses the universally quantified property(∃ X . X ≥ A ⋀ X ≤ B ⋀ C)
Quantified expressions translated as loops at run time
Control exits the loop as soon as the condition becomes false (resp. true) for a universally (resp. existentially) quantified expression
Quantification forms over array and collection content
Syntax uses
(for all/some V of ... => C)
Expression Functions
Without abstraction, contracts can become unreadable
Also, use of quantifications can make them unprovable
Expression functions provide the means to abstract contracts
Expression function is a function consisting in an expression
Definition can complete a previous declaration
Definition is allowed in a package spec! (crucial for proof with SPARK)
function Valid_Configuration return Boolean is
(case Cur_State is
when Piece_Falling | Piece_Blocked =>
No_Overlap (Cur_Board, Cur_Piece),
when Board_Before_Clean => True,
when Board_After_Clean =>
No_Complete_Lines (Cur_Board));
Code Examples / Pitfalls
Example #1
This code is not correct. The exception from the recursive call is always
caught in the handler, but not the exception raised if caller of Fail
passes False
as value for Condition
.
Example #2
This code is correct. GNAT will create a wrapper for checking the
precondition and postcondition of Memset
, calling the imported
memset
from libc
.
Example #3
This code is not correct. Although GNAT inserts precondition checks in the
subprogram body instead of its caller, it is the value of Pre
assertion policy at the declaration of the subprogram that decides if
preconditions are activated.
Example #4
This code is not correct. Contract is allowed only on the spec of a subprogram. Hence it is not allowed on the body when a separate spec is available.
Example #5
This code is not correct. Postcondition is only relevant for normal returns.
Example #6
This code is correct. Procedure may raise an exception, but postcondition correctly describes normal returns.
Example #7
This code is correct. Precondition prevents exception inside Add
.
Postcondition is always satisfied.
Example #8
This code is not correct. 'Old
on expression including a quantified
variable is not allowed.
Example #9
This code is not correct. Expr'Old
on potentially unevaluated
expression is allowed only when Expr
is a variable.
Example #10
This code is correct. Expr'Old
does not appear anymore in a
potentially unevaluated expression. Another solution would have been to
apply 'Old
on B
or to use
pragma Unevaluated_Use_Of_Old (Allow)
.