% @(#)$Id: PointerDeref.lsl,v 1.1 1999/02/03 20:29:30 leavens Exp $
% Dereferencing of pointers
% AUTHOR: Clyde Ruby

PointerDeref(T): trait
  includes MutableObj(T), 
	   MutableObj(Ptr[Obj[T]]), 
	   MutableObj(Ptr[ConstObj[T]])
  includes ConstObj(T), 
	   ConstObj(Ptr[Obj[T]]), 
	   ConstObj(Ptr[ConstObj[T]])
  includes Pointer(Obj, T),
	   Pointer(ConstObj, T)
  introduces
    deref: Obj[Ptr[Obj[T]]], State -> T
    deref: Obj[Ptr[ConstObj[T]]], State -> T
    deref: ConstObj[Ptr[Obj[T]]], State -> T
    deref: ConstObj[Ptr[ConstObj[T]]], State -> T
  asserts
    \forall p1:Obj[Ptr[Obj[T]]], 
	    p2:Obj[Ptr[ConstObj[T]]], 
	    p3:ConstObj[Ptr[Obj[T]]], 
	    p4:ConstObj[Ptr[ConstObj[T]]], 
	    st:State
        deref(p1, st) == eval(*(eval(p1, st)), st);
        deref(p2, st) == eval(*(eval(p2, st)), st);
        deref(p3, st) == eval(*(eval(p3, st)), st);
        deref(p4, st) == eval(*(eval(p4, st)), st);

[Index]

HTML generated using lcpp2html.