% @(#)$Id: NoSideEffectsDetFun.lsl,v 1.1 1995/12/24 02:23:32 leavens Exp $
% Domain, I/O relation, and result map for
% a side-effect free, deterministic programming language "function".
NoSideEffectsDetFun(S, T): trait
  includes NoSideEffectsFun(S, T)
  introduces
    resultFor: S -> T
  asserts \forall e: S, r1,r2: T
    (inDomain(e) /\ isResultFor(e, r1) /\ isResultFor(e, r2))
      => r1 = r2;
    inDomain(e) => (isResultFor(e, resultFor(e)));

[Index]

HTML generated using lcpp2html.