diff options
author | rustanleino <unknown> | 2010-06-18 17:37:41 +0000 |
---|---|---|
committer | rustanleino <unknown> | 2010-06-18 17:37:41 +0000 |
commit | b31c46ffa4d372fb9e51e667701f3b51e37afc73 (patch) | |
tree | f6189a05931138eebc6f663358afce333d6d0371 /Binaries/DafnyPrelude.bpl | |
parent | f15733e4485726ea79258d2b6938a33f54a3d36f (diff) |
Dafny:
* Added some more set axioms that go "inside out" for union and set differences (UnionOne already had such an axiom)
* Fixed bug to, once again, allow multiple .dfy files on the command line (with the effect of them being merged into one program)
* Fixed bug in translation of reads/modifies clauses that mention sequences
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
-rw-r--r-- | Binaries/DafnyPrelude.bpl | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 13314e29..520f9c77 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -32,10 +32,13 @@ axiom (forall<T> a: Set T, x: T :: { Set#UnionOne(a, x) } axiom (forall<T> a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] }
a[y] ==> Set#UnionOne(a, x)[y]);
-
function Set#Union<T>(Set T, Set T) returns (Set T);
axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] }
Set#Union(a,b)[o] <==> a[o] || b[o]);
+axiom (forall<T> a, b: Set T, y: T :: { Set#Union(a, b), a[y] }
+ a[y] ==> Set#Union(a, b)[y]);
+axiom (forall<T> a, b: Set T, y: T :: { Set#Union(a, b), b[y] }
+ b[y] ==> Set#Union(a, b)[y]);
function Set#Intersection<T>(Set T, Set T) returns (Set T);
axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] }
@@ -44,6 +47,8 @@ axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] } function Set#Difference<T>(Set T, Set T) returns (Set T);
axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Difference(a,b)[o] }
Set#Difference(a,b)[o] <==> a[o] && !b[o]);
+axiom (forall<T> a, b: Set T, y: T :: { Set#Difference(a, b), b[y] }
+ b[y] ==> !Set#Difference(a, b)[y] );
function Set#Subset<T>(Set T, Set T) returns (bool);
axiom(forall<T> a: Set T, b: Set T :: { Set#Subset(a,b) }
|