diff options
| author |  rustanleino <unknown> | 2010-07-09 03:10:43 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-07-09 03:10:43 +0000 |
| commit | 51eeaab85a7c42cfa5c98052481ad4e037f4e8b6 (patch) | |
| tree | d4eae129bbefe8449b576d5019a61012b9106990 /Binaries | |
| parent | a2c1e84dbcb6aa059971797d70f39c137b78072d (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] }
|