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/Basics.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/Basics.dfy')
| -rw-r--r-- | Test/dafny0/Basics.dfy | 75 |
1 files changed, 75 insertions, 0 deletions
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index 6b1b366d..3d2e35bd 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -262,3 +262,78 @@ predicate MSFE(s: seq<int>) copredicate CoPredTypeCheck(n: int)
requires n != 0;
+
+// -------------------- set cardinality ----------------------------------
+
+module SetCardinality {
+ method A(s: set<int>)
+ requires s != {};
+ {
+ if {
+ case true => assert s != {};
+ case true => assert |s| != 0;
+ case true => assert exists x :: x in s;
+ case true => var y :| y in s;
+ }
+ }
+
+ method B(s: set<int>)
+ requires |s| != 0;
+ {
+ if {
+ case true => assert s != {};
+ case true => assert |s| != 0;
+ case true => assert exists x :: x in s;
+ case true => var y :| y in s;
+ }
+ }
+
+ method C(s: set<int>)
+ requires exists x :: x in s;
+ {
+ if {
+ case true => assert s != {};
+ case true => assert |s| != 0;
+ case true => assert exists x :: x in s;
+ case true => var y :| y in s;
+ }
+ }
+
+ method A'(s: set<int>)
+ requires s == {};
+ {
+ if {
+ case true => assert s == {};
+ case true => assert |s| == 0;
+ case true => assert !exists x :: x in s;
+ case true => var y :| y !in s;
+ }
+ }
+
+ method B'(s: set<int>)
+ requires |s| == 0;
+ {
+ if {
+ case true => assert s == {};
+ case true => assert |s| == 0;
+ case true => assert !exists x :: x in s;
+ case true => var y :| y !in s;
+ }
+ }
+
+ method C'(s: set<int>)
+ requires forall x :: x !in s;
+ {
+ if {
+ case true => assert s == {};
+ case true => assert |s| == 0;
+ case true => assert !exists x :: x in s;
+ case true => var y :| y !in s;
+ }
+ }
+
+ method LetSuchThatExpression(s: set<int>)
+ ensures |s| != 0 ==> var x :| x in s; true;
+ {
+ }
+}
|