diff options
| author |  Rustan Leino <unknown> | 2013-06-20 18:44:27 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-06-20 18:44:27 -0700 |
| commit | 33be7e9826a9c6aaf72bcba82d349266d8f94d9c (patch) | |
| tree | 11904980cd966fe0e88a1267f18f90a941135224 /Test/dafny0/MultiSets.dfy | |
| parent | f75149436835b10ebba203a7a72ba52e723be03b (diff) | |
Beefed up axioms about cardinality and the empty (multi)set, which fixes Issue 17 on dafny.codeplex.com.
Added information that allows multiset members to be unboxed as needed (mimicking what was already done for sets).
Diffstat (limited to 'Test/dafny0/MultiSets.dfy')
| -rw-r--r-- | Test/dafny0/MultiSets.dfy | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy index a3a28222..ff03bb7a 100644 --- a/Test/dafny0/MultiSets.dfy +++ b/Test/dafny0/MultiSets.dfy @@ -176,3 +176,75 @@ method test12(a: nat, b: nat, c: int) m2 := m2[true := c]; // error: c might be negative
}
+
+// ---------- cardinality ----------
+method MultisetCardinalityA(s: multiset<int>)
+ requires s != multiset{};
+{
+ if {
+ case true => assert s != multiset{};
+ case true => assert |s| != 0;
+ case true => assert exists x :: x in s;
+ case true => var y :| y in s;
+ }
+}
+
+method MultisetCardinalityB(s: multiset<int>)
+ requires |s| != 0;
+{
+ if {
+ case true => assert s != multiset{};
+ case true => assert |s| != 0;
+ case true => assert exists x :: x in s;
+ case true => var y :| y in s;
+ }
+}
+
+method MultisetCardinalityC(s: multiset<int>)
+ requires exists x :: x in s;
+{
+ if {
+ case true => assert s != multiset{};
+ case true => assert |s| != 0;
+ case true => assert exists x :: x in s;
+ case true => var y :| y in s;
+ }
+}
+
+method MultisetCardinalityA'(s: multiset<int>)
+ requires s == multiset{};
+{
+ if {
+ case true => assert s == multiset{};
+ case true => assert |s| == 0;
+ case true => assert !exists x :: x in s;
+ case true => var y :| y !in s;
+ }
+}
+
+method MultisetCardinalityB'(s: multiset<int>)
+ requires |s| == 0;
+{
+ if {
+ case true => assert s == multiset{};
+ case true => assert |s| == 0;
+ case true => assert !exists x :: x in s;
+ case true => var y :| y !in s;
+ }
+}
+
+method MultisetCardinalityC'(s: multiset<int>)
+ requires forall x :: x !in s;
+{
+ if {
+ case true => assert s == multiset{};
+ case true => assert |s| == 0;
+ case true => assert !exists x :: x in s;
+ case true => var y :| y !in s;
+ }
+}
+
+method LetSuchThatExpression(s: multiset<int>)
+ ensures |s| != 0 ==> var x :| x in s; true;
+{
+}
|