Another kind of redundancy in a function specification
is a redundant ensures clause or claim [Tan94].
These have the same syntax as normal ensures-clauses,
but use the keyword redundantly.
(See section 6 Function Specifications for the syntax.)
A redundant ensures-clause is the dual of an example; instead of stating some property that implies the specification, it states some property that follows from a function specification.
In Larch/C++, a sequence of redundant ensures-clauses can be placed at the end of a spec-case, following the required non-redundant ensures-clause. Each redundant post-cond in such a redundant ensures-clause should be implied by the rest of the spec-case.
Redundant ensures-clauses do not affect the meaning of a function specification. They are, however, useful in highlighting properties of a function specification, or in helping debug the specification.
Each redundant ensures-clause applies to the
spec-case of which it is a part.
By nesting multiple spec-cases in a pair of curly brackets
({ }), however, one can use redundant ensures-clauses
to talk about the entire function specification.
A redundant ensures-clause that uses the keyword liberally asserts
a property of executions of the function that terminate normally,
but does not require normal termination.
A redundant ensures-clause that does not use the keyword
liberally asserts
the existence of a post-state with the desired properties.
Hence ensures redundantly true;
asserts that every execution of the function
in which the precondition is satisfied always terminates.
As a simple example, consider the following function specification. The claimed postcondition (hereafter, simply "the claim") does not change the meaning of the specification from that given earlier (see section 6 Function Specifications) but it does highlight a property of the specification that is deducible using logic and facts about the integers.
// @(#)$Id: isqrt3.lh,v 1.11 1998/09/23 16:00:31 ruby Exp $
extern int isqrt(int x) throw();
//@ behavior {
//@ requires x >= 0;
//@ ensures (result-1)*(result-1) < x
//@ /\ x < (result+1)*(result+1);
//@ ensures redundantly ((((result - 1) * (result - 1)) < x)
//@ /\ (x <= (result * result)))
//@ \/ (((result * result) <= x)
//@ /\ (x < ((result + 1) * (result + 1))));
//@ example x = 28 /\ result = 5;
//@ example x = 28 /\ result = 6;
//@ }
The semantics of a redundant ensures-clause is that,
if the precondition and postcondition are true,
and the frame axioms given by the modifies-clause
and trashes-clause are satisfied,
then the claim (the redundant post-condition)
should follow (see Section 5.2 of [Tan94]).
That is, what has to be proved to verify a claim
is the following [Tan94],
where PreCondition is the (desugared) precondition
of the function specification (which combines all the spec-cases),
MP is the predicate that codes the modifies-clause
(see section 6.2.3 The Modifies Clause),
TP is the predicate that codes the trashes-clause
(see section 6.3.2 The Trashes Clause),
PostCondition is the (desugared) postcondition
of the function specification,
and Claim is the predicate from the redundant ensures-clause.
(PreCondition /\ MP /\ TP /\ PostCondition) => Claim
In cases where there are applicable invariants (see section 7.3 Class Invariants)
or history constraints (see section 7.4 History Constraints)
these can also be instantiated for the relevant objects
and used to help prove the above formula.
Thus, for example, in a class member function specification,
where there are no class instances other than self
involved, it will suffice to prove the following,
where
Invariant(pre) is the invariant
with the to the pre-state (pre) substituted for
the state any used to express the invariant,
Invariant(post) is the invariant applied to the post-state,
HistoryConstraint is the history constraint,
and the other symbols are as above.
(The history constraint is true if omitted.)
(PreCondition /\ Invariant(pre) /\ MP /\ TP /\ PostCondition /\ Invariant(post) /\ HistoryConstraint) => Claim
Such a proof should be carried out for each redundant ensures-clause in the ensures-clause-seq.
See [Tan94] for more examples. (Larch/C++ currently only supports what Tan calls "procedure claims".)
Go to the first, previous, next, last section, table of contents.