The redundantly keyword can be used in a requires-clause
to state what should be a redundant
predicate that follows from the precondition.
(see section 6 Function Specifications, for the syntax).
Redundant requires clauses
should follow any non-redundant requires-clause
in a spec-case.
The main reason to use a redundant requires-clause is to highlight
for the reader some property, an assumption,
that is important, but which is implied
by the precondition (and any invariants in force).
As an example, consider the following specification of a function
that decrements the integer value of the object pointed to by p.
In this function, the assumption highlighted is that the argument p
cannot be a null pointer.
// @(#)$Id: decr_ptr.lh,v 1.2 1998/08/27 21:53:51 leavens Exp $
extern void decr_ptr(int *p);
//@ behavior {
//@ requires assigned(p, pre) /\ (*p)^ > 0;
//@ requires redundantly notNull(p);
//@ modifies *p;
//@ ensures returns /\ (*p)' = (*p)^ - 1;
//@ }
The semantics of a redundant requires-clause is that,
if the precondition holds, then the assumption in the redundant
requires-clause should also hold.
That is, what has to be proved is the following,
where PreCondition is the specified precondition,
and Assumption is the assumption from the redundant
requires-clause.
PreCondition => Assumption
As before, if there are relevant invariants, these can be instantiated for the relevant objects and used in the proof.
Go to the first, previous, next, last section, table of contents.