diff options
| author |  rustanleino <unknown> | 2010-07-09 03:10:43 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-07-09 03:10:43 +0000 |
| commit | 442dceca5acb9ab93978d0173e850125288db6d5 (patch) | |
| tree | cd499b781719736bbec692b2339623e6a5c46eb0 /Binaries | |
| parent | a751d6ada517ee4edeeee476e319c52e4d3388da (diff) | |
Dafny: Axiom about inverting a set union operation, similar to the recent ones added for sequence concatenation. The new SeparationLogicList example profits from this axiom.
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index eeb4f103..8d89715f 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -39,6 +39,10 @@ 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]);
+axiom (forall<T> a, b: Set T :: { Set#Union(a, b) }
+ Set#Disjoint(a, b) ==>
+ Set#Difference(Set#Union(a, b), a) == b &&
+ Set#Difference(Set#Union(a, b), b) == a);
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] }
|