/[eiffelstudio]/branches/eth/eve/Src/Delivery/studio/tools/autoproof/base_theory.bpl
ViewVC logotype

Diff of /branches/eth/eve/Src/Delivery/studio/tools/autoproof/base_theory.bpl

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 93377 by julian, Wed Nov 13 17:15:59 2013 UTC revision 93378 by julian, Thu Nov 14 15:57:08 2013 UTC
# Line 152  function {:inline} is_open(h: HeapType, Line 152  function {:inline} is_open(h: HeapType,
152          !h[o, closed]          !h[o, closed]
153  }  }
154    
155    // Is o closed in h?
156    function {:inline} is_closed(h: HeapType, o: ref): bool {
157            h[o, closed]
158    }
159    
160  // Only allocated references can be in ghost sets  // Only allocated references can be in ghost sets
161  axiom (forall h: HeapType, o: ref, r: ref :: h[o, observers][r] ==> h[r, allocated]);  axiom (forall h: HeapType, o: ref, r: ref :: h[o, observers][r] ==> h[r, allocated]);
162  axiom (forall h: HeapType, o: ref, r: ref :: h[o, owns][r] ==> h[r, allocated]);  axiom (forall h: HeapType, o: ref, r: ref :: h[o, owns][r] ==> h[r, allocated]);

Legend:
Removed from v.93377  
changed lines
  Added in v.93378

  ViewVC Help
Powered by ViewVC 1.1.23