From b31c46ffa4d372fb9e51e667701f3b51e37afc73 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Fri, 18 Jun 2010 17:37:41 +0000 Subject: 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 --- Binaries/DafnyPrelude.bpl | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'Binaries') 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 a: Set T, x: T :: { Set#UnionOne(a, x) } axiom (forall a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] } a[y] ==> Set#UnionOne(a, x)[y]); - function Set#Union(Set T, Set T) returns (Set T); axiom (forall a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] } Set#Union(a,b)[o] <==> a[o] || b[o]); +axiom (forall a, b: Set T, y: T :: { Set#Union(a, b), a[y] } + a[y] ==> Set#Union(a, b)[y]); +axiom (forall a, b: Set T, y: T :: { Set#Union(a, b), b[y] } + b[y] ==> Set#Union(a, b)[y]); function Set#Intersection(Set T, Set T) returns (Set T); axiom (forall a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] } @@ -44,6 +47,8 @@ axiom (forall a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] } function Set#Difference(Set T, Set T) returns (Set T); axiom (forall a: Set T, b: Set T, o: T :: { Set#Difference(a,b)[o] } Set#Difference(a,b)[o] <==> a[o] && !b[o]); +axiom (forall a, b: Set T, y: T :: { Set#Difference(a, b), b[y] } + b[y] ==> !Set#Difference(a, b)[y] ); function Set#Subset(Set T, Set T) returns (bool); axiom(forall a: Set T, b: Set T :: { Set#Subset(a,b) } -- cgit v1.2.3