Next: Pragma Convention_Identifier, Previous: Pragma Constant_After_Elaboration, Up: Implementation Defined Pragmas [Contents][Index]
Syntax:
pragma Contract_Cases ((CONTRACT_CASE {, CONTRACT_CASE)); CONTRACT_CASE ::= CASE_GUARD => CONSEQUENCE CASE_GUARD ::= boolean_EXPRESSION | others CONSEQUENCE ::= boolean_EXPRESSION
The Contract_Cases
pragma allows defining fine-grain specifications
that can complement or replace the contract given by a precondition and a
postcondition. Additionally, the Contract_Cases
pragma can be used
by testing and formal verification tools. The compiler checks its validity and,
depending on the assertion policy at the point of declaration of the pragma,
it may insert a check in the executable. For code generation, the contract
cases
pragma Contract_Cases ( Cond1 => Pred1, Cond2 => Pred2);
are equivalent to
C1 : constant Boolean := Cond1; -- evaluated at subprogram entry C2 : constant Boolean := Cond2; -- evaluated at subprogram entry pragma Precondition ((C1 and not C2) or (C2 and not C1)); pragma Postcondition (if C1 then Pred1); pragma Postcondition (if C2 then Pred2);
The precondition ensures that one and only one of the case guards is satisfied on entry to the subprogram. The postcondition ensures that for the case guard that was True on entry, the corresponding consequence is True on exit. Other consequence expressions are not evaluated.
A precondition P
and postcondition Q
can also be
expressed as contract cases:
pragma Contract_Cases (P => Q);
The placement and visibility rules for Contract_Cases
pragmas are
identical to those described for preconditions and postconditions.
The compiler checks that boolean expressions given in case guards and
consequences are valid, where the rules for case guards are the same as
the rule for an expression in Precondition
and the rules for
consequences are the same as the rule for an expression in
Postcondition
. In particular, attributes 'Old
and
'Result
can only be used within consequence expressions.
The case guard for the last contract case may be others
, to denote
any case not captured by the previous cases. The
following is an example of use within a package spec:
package Math_Functions is ... function Sqrt (Arg : Float) return Float; pragma Contract_Cases (((Arg in 0.0 .. 99.0) => Sqrt'Result < 10.0, Arg >= 100.0 => Sqrt'Result >= 10.0, others => Sqrt'Result = 0.0)); ... end Math_Functions;
The meaning of contract cases is that only one case should apply at each call, as determined by the corresponding case guard evaluating to True, and that the consequence for this case should hold when the subprogram returns.
Next: Pragma Convention_Identifier, Previous: Pragma Constant_After_Elaboration, Up: Implementation Defined Pragmas [Contents][Index]