7.7 The Represents Clause

A represents-clause is used to how some object represents on other objects that depend on it [Leino95]. The syntax is as follows.

represents-clause ::= represents store-ref by predicate ;

The first store-ref must name a single object, which will be referred to as the abstract object below. The predicate specifies the relationship that holds between the abstract object and some concrete objects that it depends on.

The represents-clause describes relationships that hold in all visible states. Unlike an invariant, which gives a proof obligation, the represents clause gives something that aids a proof. When used in a class, it can be thought of as conjoined to every public member function's pre- and post-condition.

[[[Detailed semantics to be written.]]]

See section 7.9.1 Inheritance of Specifications with Specification Variables for an example of the use of the represents-clause in specifying a derived class. See section 10.2 Class Refinement for other examples.

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