Some simulation functions need a state, to access the values of
contained objects. Thus a simulation function is also allowed to
have the signature of
fs in the following trait.
See section 10.3 Specifying Protected and Private Interfaces for an example
of a simulation function that needs a state.
% @(#)$Id: SimulationFunState.lsl,v 1.3 1995/01/14 04:07:23 leavens Exp $ SimulationFunState(fs, Derived, Base): trait assumes State introduces fs: Derived, State -> Base
We can regard the definition of a simulation function of the first signature as sugar for the definition of a simulation function with the second signature, by use of the following trait.
% @(#)$Id: SimFunStateFromFun.lsl,v 1.2 1995/01/14 06:36:57 leavens Exp $ SimFunStateFromFun(f, fs, Derived, Base): trait includes SimulationFun, SimulationFunState(fs, Derived, Base) asserts \forall d: Derived, st: State fs(d, st) = f(d)
For example, in the specification of
the trait function
toMoney has the signature
MutableMoney -> Money.
Therefore, Larch/C++ implicitly uses the following trait, to overload
toMoney with the signature
MutableMoney, State -> Money.
SimFunStateFromFun(toMoney, toMoney, MutableMoney, Money)
The semantics of specification inheritance with such a simulation function
is given as a syntactic sugar, by rewriting the spec-cases
of the supertype using the simulation function,
and adding them to the explicitly written spec-cases.
The only trick is to get a sensible state passed,
although this does not matter for simulation functions like
which do not depend on a state.
The rewriting goes as follows.
g is a trait function
defined on the supertype,
fs is the simulation function of signature
Derived, State -> Base.
Then the term
g(self^) (and its equivalents)
Similarly the term
The same applies to trait functions that take more than one argument,
and to trait functions;
h(self', 2) rewrites to
h(fs(self', post), 2).
When the state-fcn is
the state used is
For example, the terms
h(self\any, 2) rewrites
h(fs(self\any, any), 2).
Note that values of sort
Obj[Derived] are passed to trait functions
For example, when inheriting a specification from
a term of the form
is rewritten to
See section 10.3 Specifying Protected and Private Interfaces for a full example
using such a simulation function.
Go to the first, previous, next, last section, table of contents.