diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-10-17 14:07:59 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-10-17 14:07:59 -0700 |
| commit | 37bd956ddccbb0ccaa1f30a1283a2932178555d2 (patch) | |
| tree | 4e4071f436870ed590980c56fed75381cf3db81f /Test/dafny0/MultiSets.dfy | |
| parent | 6044f08dceb6c03e7b6e8924186a301dcc2e7e97 (diff) | |
Added some axioms to try to recover boxed data. In particular, any element 'x' of a set in the encoding satisfies Box(Unbox(x))==x. The soundness and performance of the axiomatization are dicey, so the axioms are made available only to method in-parameters.
Diffstat (limited to 'Test/dafny0/MultiSets.dfy')
| -rw-r--r-- | Test/dafny0/MultiSets.dfy | 64 |
1 files changed, 63 insertions, 1 deletions
diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy index e74873e3..22b93442 100644 --- a/Test/dafny0/MultiSets.dfy +++ b/Test/dafny0/MultiSets.dfy @@ -100,4 +100,66 @@ method test11(a: array<int>, n: int, c: int) ensures multiset(a[c..n-1]) == multiset(a[c..n]) - multiset{a[n-1]};
{
-}
\ No newline at end of file +}
+
+// ----------- the following tests mostly have to do with sets -------------
+
+class BoxTests<G> {
+ // ---------- sets ----------
+ ghost method LemmaSet0<T>(a: set<T>, b: set<T>)
+ requires forall x :: x in a ==> x in b;
+ ensures a <= b;
+ {
+ }
+
+ ghost method LemmaSet1(a: set<G>, b: set<G>)
+ requires forall x :: x in a ==> x in b;
+ ensures a <= b;
+ {
+ }
+
+ ghost method LemmaSet2(a: set<int>, b: set<int>)
+ requires forall x :: x in a ==> x in b;
+ ensures a <= b;
+ {
+ }
+
+ ghost method LemmaSet3(a: set<object>, b: set<object>)
+ requires forall x :: x in a ==> x in b;
+ ensures a <= b;
+ {
+ }
+
+ ghost method LemmaSet4(a: set<bool>, b: set<bool>)
+ requires forall x :: x in a ==> x in b;
+ ensures a <= b;
+ {
+ }
+
+ ghost method Lemma_NonEmpty(x : set<int>, y : set<int>)
+ requires x * y == {};
+ ensures x !! y;
+ {
+ assert forall k :: k !in (x*y);
+ }
+
+ // ---------- sequences (don't require any special tricks in the encoding) ----------
+ ghost method LemmaSeq(a: seq<int>, b: seq<int>)
+ requires |a| <= |b| && forall i :: 0 <= i < |a| ==> a[i] == b[i];
+ ensures a <= b;
+ {
+ }
+
+ // ---------- multisets ----------
+ ghost method LemmaMultiset0<T>(a: multiset<T>, b: multiset<T>)
+ requires forall x :: x in a ==> x in b;
+ ensures a <= b; // error: this property does not hold for multisets
+ {
+ }
+
+ ghost method LemmaMultiset1(a: multiset<int>, b: multiset<int>)
+ requires forall x :: x in a ==> x in b;
+ ensures a <= b; // error: this property does not hold for multisets
+ {
+ }
+}
|