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 MutableMoney above,
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 toMoney,
which do not depend on a state.
The rewriting goes as follows.
Suppose g is a trait function g
defined on the supertype, Base.
Suppose fs is the simulation function of signature
Derived, State -> Base.
Then the term g(self^) (and its equivalents)
rewrites to g(fs(self^, pre)).
Similarly the term g(self')
rewrites to g(fs(self', post)).
The same applies to trait functions that take more than one argument,
and to trait functions;
for example, h(self', 2) rewrites to h(fs(self', post), 2).
When the state-fcn is \any,
the state used is any.
For example, the terms h(self\any, 2) rewrites
to h(fs(self\any, any), 2).
Note that values of sort Obj[Derived] are passed to trait functions
unchanged.
For example, when inheriting a specification from Money,
a term of the form self'
is rewritten to toMoney(self', post).
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.