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

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) }