diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Test/test2/NullaryMaps.bpl | |
Initial set of files.
Diffstat (limited to 'Test/test2/NullaryMaps.bpl')
| -rw-r--r-- | Test/test2/NullaryMaps.bpl | 57 |
1 files changed, 57 insertions, 0 deletions
diff --git a/Test/test2/NullaryMaps.bpl b/Test/test2/NullaryMaps.bpl new file mode 100644 index 00000000..1bc18c41 --- /dev/null +++ b/Test/test2/NullaryMaps.bpl @@ -0,0 +1,57 @@ +// aren't these cool!
+
+var m: []int;
+var p: <a>[]a;
+
+type ref;
+const null: ref;
+
+procedure P()
+ requires m[] == 5;
+ modifies m;
+ modifies p;
+ ensures m[] == 30;
+ ensures p[] == null;
+{
+ m[] := 12;
+ p[] := 12;
+ p[] := true;
+ assert p[] == m[];
+ assert p[];
+ m := m[:= 30];
+ p := p[:=null];
+}
+
+procedure Q()
+ modifies m;
+{
+ assert m[] == 5; // error
+ m[] := 30;
+ assert m[] == 5; // error
+}
+
+procedure R()
+ modifies p;
+{
+ assert p[] < 3; // error
+}
+
+// ----
+
+type Field a;
+type HeapType = <a>[ref, Field a]a;
+const F0: Field int;
+const F1: Field bool;
+const alloc: Field bool;
+var Heap: HeapType;
+procedure FrameCondition(this: ref)
+ modifies Heap;
+ ensures (forall<a> o: ref, f: Field a ::
+ Heap[o,f] == old(Heap)[o,f] ||
+ !old(Heap)[o,alloc] ||
+ (o == this && f == F0) ||
+ (o == this && f == F1)
+ );
+{
+}
+
|