Dafny: liberalized equality to work when the types could possibly be the same

(i.e. a != b is allowed when a: array<int> and b: array<T>)

4 files changed, 64 insertions, 4 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index be41fbf8..8866491e 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1574,6 +1574,11 @@ Execution trace:
 

 Dafny program verifier finished with 30 verified, 2 errors

 

+-------------------- LiberalEquality.dfy --------------------

+LiberalEquality.dfy(37,14): Error: arguments must have the same type (got Weird<T,int,V> and Weird<T,bool,V>)

+LiberalEquality.dfy(52,14): Error: arguments must have the same type (got array<int> and array<bool>)

+2 resolution/type errors detected in LiberalEquality.dfy

+

 -------------------- SmallTests.dfy --------------------

 SmallTests.dfy(30,11): Error: index out of range

 Execution trace:

diff --git a/Test/dafny0/LiberalEquality.dfy b/Test/dafny0/LiberalEquality.dfy
new file mode 100644
index 00000000..3dc52c80
--- /dev/null
+++ b/Test/dafny0/LiberalEquality.dfy
@@ -0,0 +1,55 @@
+

+class Array<T>

+{

+   var Length: nat;

+}

+

+class Test<T> {

+  var a: Array<int>;

+  var b: Array<T>;

+  predicate valid()

+      reads this, a, b;

+  {

+      a != null && b != null && a != b && a.Length == b.Length

+  }

+}

+

+method m1<T, U>(t: T, u: U)

+   requires t != u;

+{

+   

+}

+

+method m2<T>(t: array<T>, a: array<int>)

+   requires t != null && a != null && t != a && t.Length == a.Length;

+{

+

+}

+

+

+class Weird<T, U, V>

+{

+

+}

+

+

+method m3<T, V>(a: Weird<T, int, V>, b: Weird<T, bool, V>)

+   requires a == b; // Bad: second parameter can't be both bool and int.

+{

+

+}

+

+

+method m4<T, U, V>(a: Weird<T, U, V>, b: Weird<T, bool, V>)

+  requires a == b;

+{

+

+}

+

+

+// Just to make sure nothing went wrong.

+method m5(a: array<int>, b: array<bool>)

+   requires a == b; // Bad: never equal

+{

+

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index e4c134f6..0da7fe3e 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -22,7 +22,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             LoopModifies.dfy Refinement.dfy RefinementErrors.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy

-            Predicates.dfy Skeletons.dfy Maps.dfy) do (

+            Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy) do (

   echo.

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

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

diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy
index e56a8317..3e5a95ef 100644
--- a/Test/vacid0/LazyInitArray.dfy
+++ b/Test/vacid0/LazyInitArray.dfy
@@ -11,10 +11,10 @@ class LazyInitArray<T> {
     reads this, a, b, c;

   {

     a != null && b != null && c != null &&

-    a.Length == |Contents| + 1 &&  // TODO: remove the "+ 1" hack, which currently serves the purpose of distinguishing 'a' from 'b' and 'c'

+    a.Length == |Contents| &&

     b.Length == |Contents| &&

     c.Length == |Contents| &&

-    b != c &&

+    b != c && a != b && a != c &&

     0 <= n && n <= c.Length &&

     (forall i :: 0 <= i && i < |Contents| ==>

        Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else Zero)) &&

@@ -41,7 +41,7 @@ class LazyInitArray<T> {
     ensures |Contents| == N && Zero == zero;

     ensures (forall x :: x in Contents ==> x == zero);

   {

-    a := new T[N+1];

+    a := new T[N];

     b := new int[N];

     c := new int[N];

     n := 0;