7.6 The Depends Clause

A depends-clause is used to specify that some object depends on other objects [Leino95]. The syntax is as follows.

depends-clause ::= depends store-ref on store-ref-list ;

The first store-ref must name a single object, which will be referred to as the abstract object below. The store-ref-list names the concrete objects that the abstract object depends on.

The effect of a depends-clause is to allow the concrete objects to be modified when the abstract object is mentioned in a modifies-clause, and to be trashed when the abstract object is mentioned in a trashes-clause. (See section 6.2.3 The Modifies Clause for details on the modifies-clause. (See section 6.3.2 The Trashes Clause for details on the trashes-clause.)

See section 7.9.1 Inheritance of Specifications with Specification Variables for an example of the use of the depends-clause in specifying a derived class.

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