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

6 files changed, 188 insertions, 15 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index a89ded50..dd0a6671 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -25,7 +25,9 @@ axiom (forall<T> s: Set T :: { Set#Card(s) } 0 <= Set#Card(s));
 

 function Set#Empty<T>(): Set T;

 axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);

-axiom (forall<T> s: Set T :: { Set#Card(s) } Set#Card(s) == 0 <==> s == Set#Empty());

+axiom (forall<T> s: Set T :: { Set#Card(s) }

+  (Set#Card(s) == 0 <==> s == Set#Empty()) &&

+  (Set#Card(s) != 0 ==> (exists x: T :: s[x])));

 

 function Set#Singleton<T>(T): Set T;

 axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);

@@ -117,8 +119,8 @@ type MultiSet T = [T]int;
 function $IsGoodMultiSet<T>(ms: MultiSet T): bool;

 // ints are non-negative, used after havocing, and for conversion from sequences to multisets.

 axiom (forall<T> ms: MultiSet T :: { $IsGoodMultiSet(ms) } 

-     $IsGoodMultiSet(ms) <==> (forall o: T :: { ms[o] } 0 <= ms[o]));

-     

+  $IsGoodMultiSet(ms) <==> (forall bx: T :: { ms[bx] } 0 <= ms[bx]));

+

 function MultiSet#Card<T>(MultiSet T): int;

 axiom (forall<T> s: MultiSet T :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s));     

 axiom (forall<T> s: MultiSet T, x: T, n: int :: { MultiSet#Card(s[x := n]) }

@@ -126,7 +128,9 @@ axiom (forall<T> s: MultiSet T, x: T, n: int :: { MultiSet#Card(s[x := n]) }
 

 function MultiSet#Empty<T>(): MultiSet T;

 axiom (forall<T> o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0);

-axiom (forall<T> s: MultiSet T :: { MultiSet#Card(s) } MultiSet#Card(s) == 0 <==> s == MultiSet#Empty());

+axiom (forall<T> s: MultiSet T :: { MultiSet#Card(s) }

+  (MultiSet#Card(s) == 0 <==> s == MultiSet#Empty()) &&

+  (MultiSet#Card(s) != 0 ==> (exists x: T :: 0 < s[x])));

 

 function MultiSet#Singleton<T>(T): MultiSet T;

 axiom (forall<T> r: T, o: T :: { MultiSet#Singleton(r)[o] } (MultiSet#Singleton(r)[o] == 1 <==> r == o) &&

@@ -470,14 +474,18 @@ function $IsCanonicalBoolBox(BoxType): bool;
 axiom $IsCanonicalBoolBox($Box(false)) && $IsCanonicalBoolBox($Box(true));

 axiom (forall b: BoxType :: { $Unbox(b): bool } $IsCanonicalBoolBox(b) ==> $Box($Unbox(b): bool) == b);

 

-// The following function and axiom are used to obtain a $Box($Unbox(_)) wrapper around

-// certain expressions.  Note that it assumes any booleans contained in the set are canonical

-// (which is the case for any set that occurs in an execution of a Dafny program).

+// The following functions and axioms are used to obtain a $Box($Unbox(_)) wrapper around

+// certain expressions.  Note that it assumes any booleans (or, indeed, values of any type) contained

+// in the (multi)set are canonical (which is the case for any (multi)set that occurs in an execution of

+// a Dafny program).

 // The role of the parameter 'dummy' in the following is (an unfortunately clumsy construction

 // whose only purpose is) simply to tell Boogie how to instantiate the type parameter 'T'.

-function $IsGoodSet<T>(s: Set BoxType, dummy: T): bool;

-axiom (forall<T> ss: Set BoxType, dummy: T, bx: BoxType :: { $IsGoodSet(ss, dummy), ss[bx] }

-  $IsGoodSet(ss, dummy) ==> ss[bx] ==> bx == $Box($Unbox(bx):T));

+function $IsGoodSet_Extended<T>(s: Set BoxType, dummy: T): bool;

+axiom (forall<T> ss: Set BoxType, dummy: T, bx: BoxType :: { $IsGoodSet_Extended(ss, dummy), ss[bx] }

+  $IsGoodSet_Extended(ss, dummy) ==> ss[bx] ==> bx == $Box($Unbox(bx): T));

+function $IsGoodMultiSet_Extended<T>(ms: MultiSet BoxType, dummy: T): bool;

+axiom (forall<T> ms: MultiSet BoxType, dummy: T, bx: BoxType :: { $IsGoodMultiSet_Extended(ms, dummy), ms[bx] } 

+  $IsGoodMultiSet_Extended(ms, dummy) ==> 0 < ms[bx] ==> bx == $Box($Unbox(bx): T));

 

 // ---------------------------------------------------------------

 // -- Encoding of type names -------------------------------------

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 9628f14b..242d6589 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -6504,10 +6504,18 @@ namespace Microsoft.Dafny {
       type = type.Normalize();

       if (type is SetType) {

         var t = (SetType)type;

-        // $IsGoodSet(x, V), where V is a value whose type is the same as the element type of the set.

+        // $IsGoodSet_Extended(x, V), where V is a value whose type is the same as the element type of the set.

         var ex = ExemplaryBoxValue(t.Arg);

         if (ex != null) {

-          var p = FunctionCall(tok, "$IsGoodSet", Bpl.Type.Bool, x, ex);

+          var p = FunctionCall(tok, BuiltinFunction.IsGoodSet_Extended, null, x, ex);

+          r = r == null ? p : BplAnd(r, p);

+        }

+      } else  if (type is MultiSetType) {

+        var t = (MultiSetType)type;

+        // $IsGoodMultiSet_Extended(x, V), where V is a value whose type is the same as the element type of the set.

+        var ex = ExemplaryBoxValue(t.Arg);

+        if (ex != null) {

+          var p = FunctionCall(tok, BuiltinFunction.IsGoodMultiSet_Extended, null, x, ex);

           r = r == null ? p : BplAnd(r, p);

         }

       } else if (type.IsDatatype) {

@@ -8559,6 +8567,7 @@ namespace Microsoft.Dafny {
       SetEqual,

       SetSubset,

       SetDisjoint,

+      IsGoodSet_Extended,

 

       MultiSetCard,

       MultiSetEmpty,

@@ -8572,6 +8581,7 @@ namespace Microsoft.Dafny {
       MultiSetFromSet,

       MultiSetFromSeq,      

       IsGoodMultiSet,

+      IsGoodMultiSet_Extended,

 

       SeqLength,

       SeqEmpty,

@@ -8671,6 +8681,10 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 2);

           Contract.Assert(typeInstantiation == null);

           return FunctionCall(tok, "Set#Disjoint", Bpl.Type.Bool, args);

+        case BuiltinFunction.IsGoodSet_Extended:

+          Contract.Assert(args.Length == 2);

+          Contract.Assert(typeInstantiation == null);

+          return FunctionCall(tok, "$IsGoodSet_Extended", Bpl.Type.Bool, args);

 

         case BuiltinFunction.MultiSetCard:

           Contract.Assert(args.Length == 1);

@@ -8722,6 +8736,10 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation == null);

           return FunctionCall(tok, "$IsGoodMultiSet", Bpl.Type.Bool, args);

+        case BuiltinFunction.IsGoodMultiSet_Extended:

+          Contract.Assert(args.Length == 2);

+          Contract.Assert(typeInstantiation == null);

+          return FunctionCall(tok, "$IsGoodMultiSet_Extended", Bpl.Type.Bool, args);

 

         case BuiltinFunction.SeqLength:

           Contract.Assert(args.Length == 1);

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

 )