In a Larch/C++ function specification, one can declare the global variables used in the specification of a function in the declaration-seq section of the specification's fun-spec-body. While this is not necessary if the variables were previously declared in a surrounding scope, declaring them makes clear to the reader of the specification what all the objects are that the function needs as "implicit arguments." (They are called "implicit arguments" because the function depends, in some way on each of these arguments. In the jargon of program verification, such variables are called "threatened.")
To mesh with C++ syntax, and to avoid confusing the reader
of the specification,
the declarations of such threatened variables
should start with the keyword extern.
In the specification below, the global variable current_token of type
Token is referenced in the function next_token;
to warn the reader, this variable is
explicitly declared in the declaration-seq clause.
// @(#)$Id: next_token.lh,v 1.6 1997/06/03 20:30:16 leavens Exp $
#include "istream.lh"
#include "Token.lh"
static Token current_token;
extern void next_token() throw();
//@ behavior {
//@ extern Token current_token; // global variable referenced
//@ extern istream cin; // another global variable
//@
//@ requires assigned(cin, pre);
//@ modifies current_token, cin;
//@ ensures current_token' = scan_token(cin^) /\ cin' = remove_token(cin^);
//@ }
A declaration of the form extern everything; means that
the function threatens all objects.
It might be used if one wants to warn the reader that
the function may access a large number of global variables.
However, all the global variables explicitly mentioned in the
specification must have been previously declared.
A C++ function that uses global variables can be modeled mathematically as a function with implicit (reference) arguments for each global variable the C++ function uses. Since the data members of an instance are not global variables, they are not listed as such.
Go to the first, previous, next, last section, table of contents.