operations

NEW: Heaps_Data ==> ADDRESS
NEW(data) ==
(   def newAddress = Heaps_UnallocatedAddress(heap) in
       def newLoc = mk_Heaps_Location(data,true) in
    (   heap := Heaps_ModifyLoc(heap, newAddress, newLoc);
        return newAddress
    )
)
pre Heaps_Available(heap);

DISPOSE: ADDRESS ==> ()
DISPOSE(address) ==
   heap := Heaps_ModifyLoc(heap, address, mk_Heaps_Location(nil, false))
pre pre_Heaps_ModifyLoc(heap, address, mk_Heaps_Location(nil, false))