% @(#)$Id: SideEffectsFun.lsl,v 1.1 1995/12/24 22:09:32 leavens Exp $
% Domain and state relation predicates for a
% programming language procedure (which may be nondeterministic).
SideEffectsFun(T): trait
  includes State_Basics
  introduces
    inDomain: T, State -> Bool
    isStateFor: T, State, State -> Bool
  asserts \forall e: T, pre, post: State
    inDomain(e, pre) => (\E post (isStateFor(e, pre, post)));

[Index]

HTML generated using lcpp2html.