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).

4 files changed, 150 insertions, 3 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 40725691..e78110b7 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -738,7 +738,7 @@ Basics.dfy(235,10): Error: when left-hand sides 0 and 1 refer to the same locati
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 37 verified, 11 errors

+Dafny program verifier finished with 51 verified, 11 errors

 

 -------------------- ControlStructures.dfy --------------------

 ControlStructures.dfy(5,3): Error: missing case in case statement: Purple

@@ -1475,7 +1475,7 @@ Execution trace:
     (0,0): anon4_Then

     (0,0): anon3

 

-Dafny program verifier finished with 39 verified, 3 errors

+Dafny program verifier finished with 53 verified, 3 errors

 

 -------------------- PredExpr.dfy --------------------

 PredExpr.dfy(4,12): Error: condition in assert expression might not hold

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;

+  {

+  }

+}

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;

+{

+}

diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat
index 3fffb577..ecccd929 100644
--- a/Test/vstte2012/runtest.bat
+++ b/Test/vstte2012/runtest.bat
@@ -13,5 +13,5 @@ for %%f in (
   ) do (

   echo.

   echo -------------------- %%f --------------------

-  %DAFNY_EXE% /compile:0 /vcsMaxKeepGoingSplits:2 /dprint:out.dfy.tmp %* %%f

+  %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

 )