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/test21/EmptySetBug.bpl |
Initial set of files.
Diffstat (limited to 'Test/test21/EmptySetBug.bpl')
-rw-r--r-- | Test/test21/EmptySetBug.bpl | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/Test/test21/EmptySetBug.bpl b/Test/test21/EmptySetBug.bpl new file mode 100644 index 00000000..424d998c --- /dev/null +++ b/Test/test21/EmptySetBug.bpl @@ -0,0 +1,30 @@ +type ref;
+
+const null: ref;
+
+type Set T = [T]bool;
+
+function Set#Empty<T>() returns (Set T);
+
+axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);
+
+function Set#Singleton<T>(T) returns (Set T);
+
+axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);
+
+axiom (forall<T> r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o);
+
+function Set#UnionOne<T>(Set T, T) returns (Set T);
+
+axiom (forall<T> a: Set T, x: T, o: T :: { Set#UnionOne(a, x)[o] } Set#UnionOne(a, x)[o] <==> o == x || a[o]);
+
+procedure Test(this: ref)
+{
+ var s: Set ref;
+
+ s := Set#UnionOne(Set#Empty(), this);
+ assert s[this];
+ assert !Set#Empty()[this];
+
+ assert Set#Singleton(this)[null]; // should not be provable
+}
|