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

9.1 Ghost Variables

A spec-decl consists of a declaration preceded by the keyword spec.

spec-decl ::= spec declaration

Such declarations declare things which are may be useful for specification purposes, but which do not have to be implemented. In the literature, variables declared in this way are called ghost variables or specification variables. (The syntax for this feature is borrowed from LCL [Tan 94].)

An example of an interface that uses a spec-decl is the following. The spec-decl is used to declare the system_clock as a volatile variable. (It is declared volatile because it changes state in ways not controlled by a program.) This is declared using a spec-decl because, while in a real system there would be a clock, it might not be directly accessible as a volatile variable named system_clock. Thus a spec-decl is used for the global declaration of system_clock, not a extern decl. If the global declaration was marked extern, a corresponding declaration would have to appear in the implementation, and this would, in effect, require the implementation to have a variable named system_clock. Furthermore, without this spec-decl, the function time would be a constant function, as it takes no input arguments. (The argument pointer tloc is part of the standard C library.)

// @(#)$Id: time.lh,v 1.11 1997/07/31 04:02:27 leavens Exp $

// the following defines time_t
#include "types.lh"

//@ spec volatile time_t system_clock;

extern time_t time(time_t * tloc) throw();
//@ behavior {
//@   requires allocated(tloc, pre);
//@   modifies *tloc;
//@   ensures result = system_clock^ /\ tloc' = system_clock^;
//@ also
//@   requires isNull(tloc);
//@   ensures result = system_clock^;
//@ }

See section 7 Class Specifications for several examples that use specification variables to specify the abstract models of classes.

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