% @(#)$Id: NoSideEffectsFun.lsl,v 1.3 1995/12/24 02:21:35 leavens Exp $
% Domain and input/output predicates for a side-effect free
% programming language "function" (which may be nondeterministic).
NoSideEffectsFun(S, T): trait
  introduces
    inDomain: S -> Bool
    isResultFor: S,T -> Bool
  asserts \forall s: S, t: T
    inDomain(s) => (\E t (isResultFor(s, t)));

[Index]

HTML generated using lcpp2html.