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


7.9.3.2 Simulation Functions that Need a State

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.