Go to the first, previous, next, last section, table of contents.

6.9.2 Redundant Requires Clauses

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.