% @(#) $Id: PureValue.lsl,v 1.1 1997/07/31 01:31:46 leavens Exp $

PureValue(V) : trait
  assumes State
  introduces
    eval: V, State -> V
    allocated, assigned: V, State -> Bool
  asserts
    \forall v: V, st: State
    eval(v, st) == v;
    allocated(v, st);
    assigned(v, st);

[Index]

HTML generated using lcpp2html.