% @(#)$Id: WithUnassigned.lsl,v 1.1 1995/11/06 05:12:17 leavens Exp $

WithUnassigned(T): trait
  introduces 
    injectTVal: T -> WithUnassigned[T]
    extractTVal: WithUnassigned[T] -> T
    unassigned: -> WithUnassigned[T]
    isUnassigned: WithUnassigned[T] -> Bool

  asserts
    sort WithUnassigned[T] generated by injectTVal, unassigned
    sort WithUnassigned[T] partitioned by isUnassigned, extractTVal
    \forall tval: T
      extractTVal(injectTVal(tval)) == tval;
      ~isUnassigned(injectTVal(tval));
      isUnassigned(unassigned);

  implies
    \forall tval: T
      injectTVal(extractTVal(injectTVal(tval))) == injectTVal(tval);
    converts
      isUnassigned, extractTVal
        exempting extractTVal(unassigned)

[Index]

HTML generated using lcpp2html.