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.