Implemented resolution, verification, and (poorly performing) compilation of existential if guards.

Fixed bugs in ghost checks involving comprehensions and attributes.
Added SubstituteBoundedPool method.

8 files changed, 571 insertions, 22 deletions

diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index a2b96996..7f9169da 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny "%s" > "%t"

+// RUN: %dafny /compile:3 "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 // The tests in this file are designed to run through the compiler.  They contain

@@ -43,6 +43,8 @@ module CoRecursion {
   //   40

   //   41

   //   42

+  //   9

+  //   9

   method Main() {

     var m := 17;

     var cell := new Cell;

@@ -58,6 +60,37 @@ module CoRecursion {
       print l.car, "\n";

       l := l.cdr;

     }

+    var nio := OneLess(0, 10);

+    print nio, "\n";

+    nio := OneLess'(0, 10);

+    print nio, "\n";

+  }

+

+  method OneLess(lo: int, hi: int) returns (m: int)

+    requires lo < hi

+    // This method ensures m == hi - 1, but we don't care to prove it

+    decreases hi - lo

+  {

+    if y :| lo < y < hi {

+      m := OneLess(y, hi);

+    } else {

+      m := lo;

+    }

+  }

+

+  method OneLess'(lo: int, hi: int) returns (m: int)

+    requires lo < hi

+    // This method ensures m == hi - 1, but we don't care to prove it

+    decreases hi - lo

+  {

+    if {

+      case y :| lo < y < hi =>

+        m := OneLess'(y, hi);

+      case lo+1 < hi =>

+        m := OneLess'(lo+1, hi);

+      case lo + 1 == hi =>

+        m := lo;

+    }

   }

 }

 

diff --git a/Test/dafny0/Compilation.dfy.expect b/Test/dafny0/Compilation.dfy.expect
index 0a1938ae..2b76b107 100644
--- a/Test/dafny0/Compilation.dfy.expect
+++ b/Test/dafny0/Compilation.dfy.expect
@@ -1,3 +1,12 @@
 

-Dafny program verifier finished with 46 verified, 0 errors

-Compiled assembly into Compilation.exe

+Dafny program verifier finished with 50 verified, 0 errors

+Program compiled successfully

+Running...

+

+400
+320
+40
+41
+42
+9
+9
diff --git a/Test/dafny0/ExistentialGuards.dfy b/Test/dafny0/ExistentialGuards.dfy
index 001acb55..5afb3979 100644
--- a/Test/dafny0/ExistentialGuards.dfy
+++ b/Test/dafny0/ExistentialGuards.dfy
@@ -2,12 +2,19 @@
 // RUN: %diff "%s.expect" "%t"

 

 predicate P(n: int)

+{

+  n % 2 == 0

+}

 

 predicate R(r: real)

+{

+  0.0 <= r

+}

 

 method M0()

 {

   if x :| P(x) {

+    var y := x + 3;

   }

 }

 

@@ -19,13 +26,19 @@ method M1()
 

 method M2()

 {

-  if x, y :| P(x) && R(y) {

+  var x := true;

+  if x, y :| P(x) && R(y) {  // this declares a new 'x'

+    var z := x + 12;

   }

+  x := x && false;

 }

 

 method M3()

 {

+  var x := true;

   if x: int, y :| P(x) && R(y) {

+    var z := x + y.Trunc;

+    var w := real(x) + y;

   }

 }

 

@@ -53,37 +66,94 @@ method M6()
   }

 }

 

-method M7()

+ghost method M7() returns (z: real, w: real)

+  ensures -2.0 <= z

+  ensures z == w  // error: does not hold

 {

+  var k;

   if x :| P(x) {

+    k, z := 4, 18.0;

   } else if * {

+    z := z + -z;

   } else if y :| R(y) {

+    z := y;

   } else if y :| P(y) {

+    k := y;

+  } else {

+    z :| R(z);

+  }

+  if P(k) {

+    z := 18.0;

+  }

+}

+

+ghost method M8(m: int, n: int)

+  requires forall y :: m <= y < n ==> P(y)

+{

+  var t := -1;

+  var u;

+  if y :| m <= y < n && P(y) {

+    u := y;

+    if * {

+      t := n - y;

+    } else if * {

+      t := y - m;

+    } else if P(y) {

+      t := 8;

+    } else {

+      t := -100;  // will never happen

+    }

+  }

+  if t < 0 && m < n {

+    assert P(m) && !P(m);

+    assert false;

   }

+  assert t < 0 ==> n <= m;

 }

 

 method P0(m: int, n: int)

   requires m < n

 {

+  ghost var even, alsoEven := 4, 8;

   if {

     case x :| P(x) =>

+      even := x;

     case x: int :| P(x) =>

+      even := x;

     case x, y :| P(x) && R(y) =>

+      even, alsoEven := x, y.Trunc;  // this assigns to 'alsoEven' a possibly odd number

     case x: int, y :| P(x) && R(y) =>

+      even := x;

     case m < n =>  // just to be different

     case x, y: real :| P(x) && R(y) =>

+      even := x;

     case x: int, y: real :| P(x) && R(y) =>

+      even := x;

   }

+  assert P(even);

+  assert P(alsoEven);  // error: may not hold

 }

 

 method P1(m: int, n: int)

-  requires m < n

 {

+  if {  // error: missing case

+    case x :| m <= x < n && P(x) =>

+  }

+}

+

+method P2(m: int, n: int)

+  requires forall y :: m <= y < n ==> P(y)

+{

+  if {  // error: missing case

+    case x :| m <= x < n && P(x) =>

+  }

+}

+

+method P3(m: int, n: int)

+  requires m < n && forall y :: m <= y < n ==> P(y)

+{

+  assert P(m);  // lemma that proves that the following 'if' covers all possibilities

   if {

-    case x {:myattribute x, "hello"} :| P(x) =>

-    case x, y {:myattribute y, "sveika"} :| P(x) && R(y) =>

-    case x: int {:myattribute x, "chello"} :| P(x) =>

-    case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) =>

-    case m < n =>

+    case x :| m <= x < n && P(x) =>

   }

 }

diff --git a/Test/dafny0/ExistentialGuards.dfy.expect b/Test/dafny0/ExistentialGuards.dfy.expect
index cf229553..21461067 100644
--- a/Test/dafny0/ExistentialGuards.dfy.expect
+++ b/Test/dafny0/ExistentialGuards.dfy.expect
@@ -3,12 +3,19 @@
 // ExistentialGuards.dfy

 

 predicate P(n: int)

+{

+  n % 2 == 0

+}

 

 predicate R(r: real)

+{

+  0.0 <= r

+}

 

 method M0()

 {

   if x :| P(x) {

+    var y := x + 3;

   }

 }

 

@@ -20,13 +27,19 @@ method M1()
 

 method M2()

 {

+  var x := true;

   if x, y :| P(x) && R(y) {

+    var z := x + 12;

   }

+  x := x && false;

 }

 

 method M3()

 {

+  var x := true;

   if x: int, y :| P(x) && R(y) {

+    var z := x + y.Trunc;

+    var w := real(x) + y;

   }

 }

 

@@ -54,41 +67,119 @@ method M6()
   }

 }

 

-method M7()

+ghost method M7() returns (z: real, w: real)

+  ensures -2.0 <= z

+  ensures z == w

 {

+  var k;

   if x :| P(x) {

+    k, z := 4, 18.0;

   } else if * {

+    z := z + -z;

   } else if y :| R(y) {

+    z := y;

   } else if y :| P(y) {

+    k := y;

+  } else {

+    z :| R(z);

+  }

+  if P(k) {

+    z := 18.0;

   }

 }

 

+ghost method M8(m: int, n: int)

+  requires forall y :: m <= y < n ==> P(y)

+{

+  var t := -1;

+  var u;

+  if y :| m <= y < n && P(y) {

+    u := y;

+    if * {

+      t := n - y;

+    } else if * {

+      t := y - m;

+    } else if P(y) {

+      t := 8;

+    } else {

+      t := -100;

+    }

+  }

+  if t < 0 && m < n {

+    assert P(m) && !P(m);

+    assert false;

+  }

+  assert t < 0 ==> n <= m;

+}

+

 method P0(m: int, n: int)

   requires m < n

 {

+  ghost var even, alsoEven := 4, 8;

   if {

     case x :| P(x) =>

+      even := x;

     case x: int :| P(x) =>

+      even := x;

     case x, y :| P(x) && R(y) =>

+      even, alsoEven := x, y.Trunc;

     case x: int, y :| P(x) && R(y) =>

+      even := x;

     case m < n =>

     case x, y: real :| P(x) && R(y) =>

+      even := x;

     case x: int, y: real :| P(x) && R(y) =>

+      even := x;

   }

+  assert P(even);

+  assert P(alsoEven);

 }

 

 method P1(m: int, n: int)

-  requires m < n

 {

   if {

-    case x {:myattribute x, "hello"} :| P(x) =>

-    case x, y {:myattribute y, "sveika"} :| P(x) && R(y) =>

-    case x: int {:myattribute x, "chello"} :| P(x) =>

-    case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) =>

-    case m < n =>

+    case x :| m <= x < n && P(x) =>

+  }

+}

+

+method P2(m: int, n: int)

+  requires forall y :: m <= y < n ==> P(y)

+{

+  if {

+    case x :| m <= x < n && P(x) =>

+  }

+}

+

+method P3(m: int, n: int)

+  requires m < n && forall y :: m <= y < n ==> P(y)

+{

+  assert P(m);

+  if {

+    case x :| m <= x < n && P(x) =>

   }

 }

+ExistentialGuards.dfy(85,10): Error BP5003: A postcondition might not hold on this return path.

+ExistentialGuards.dfy(71,12): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon12_Then

+    (0,0): anon9

+    (0,0): anon16_Then

+ExistentialGuards.dfy(134,9): Error: assertion violation

+ExistentialGuards.dfy(6,8): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon20_Then

+    (0,0): anon21_Then

+    (0,0): anon5

+    (0,0): anon17

+ExistentialGuards.dfy(139,2): Error: alternative cases fail to cover all possibilties

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Else

+ExistentialGuards.dfy(147,2): Error: alternative cases fail to cover all possibilties

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Else

 

-Dafny program verifier finished with 22 verified, 0 errors

-Compilation error: Function _module._default.P has no body

-Compilation error: Function _module._default.R has no body

+Dafny program verifier finished with 24 verified, 4 errors

diff --git a/Test/dafny0/ExistentialGuardsResolution.dfy b/Test/dafny0/ExistentialGuardsResolution.dfy
new file mode 100644
index 00000000..8fce1de5
--- /dev/null
+++ b/Test/dafny0/ExistentialGuardsResolution.dfy
@@ -0,0 +1,154 @@
+// RUN: %dafny /dprint:- "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+predicate P(n: int)

+

+predicate R(r: real)

+

+method M0()

+{

+  if x :| P(x) {

+    var y := x + 3;

+    var x := true;  // error: 'x' is already declared in this scope

+  }

+}

+

+method M1()

+{

+  if x: int :| P(x) {

+    x := x + 1;  // error: 'x' is an immutable variable

+  }

+}

+

+method M2()

+{

+  var x := true;

+  if x, y :| P(x) && R(y) {  // this declares a new 'x'

+    var z := x + 12;

+  }

+  x := x && false;

+}

+

+method M3()

+{

+  var x := true;

+  if x: int, y :| P(x) && R(y) {

+    var z := x + int(y);

+    var w := real(x) + y;

+  }

+  var x := 0.0;  // error: 'x' is already declared in this scope

+}

+

+method M4()

+{

+  if x, y: real :| P(x) && R(y) {

+  }

+}

+

+method M5()

+{

+  if x: int, y: real :| P(x) && R(y) {

+  }

+}

+

+method M6()

+{

+  if x {:myattribute x, "hello"} :| P(x) {

+  }

+  if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {

+  }

+  if x: int {:myattribute x, "chello"} :| P(x) {

+  }

+  if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {

+  }

+}

+

+method M7()

+{

+  if x :| P(x) {

+  } else if * {

+  } else if y :| R(y) {

+  } else if y :| P(y) {

+  }

+}

+

+method P0(m: int, n: int)

+  requires m < n

+{

+  var x := true;

+  if {

+    case x :| P(x) =>

+      var t := 3 * x;

+    case x: int :| P(x) =>

+    case x, y :| P(x) && R(y) =>

+      y := y + 1.0;  // error: 'y' is an immutable variable

+    case x: int, y :| P(x) && R(y) =>

+    case m < n =>

+      x := x || m + 5 == n;

+    case x, y: real :| P(x) && R(y) =>

+    case x: int, y: real :| P(x) && R(y) =>

+  }

+  assert x;

+}

+

+method P1(m: int, n: int)

+  requires m < n

+{

+  if {

+    case x {:myattribute x, "hello"} :| P(x) =>

+    case x, y {:myattribute y, "sveika"} :| P(x) && R(y) =>

+    case x: int {:myattribute x, "chello"} :| P(x) =>

+    case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) =>

+    case m < n =>

+  }

+}

+

+module TypesNotFullyDetermined {

+  method T0()

+  {

+    if x :| true {  // error: type not entirely resolved

+    }

+  }

+  method T1()

+  {

+    if x :| true {

+      var y := x + 3;

+    }

+  }

+}

+

+module Ghost {

+  predicate P(x: int)  // note, P is ghost

+  predicate method R(x: int)

+  method M7() returns (z: int, b: bool)

+  {

+    if * {

+      z := z + -z;

+    } else if y :| 1000 <= y < 2000 && R(y) {

+      z := y;

+    } else if y :| 0 <= y < 100 && P(y) {

+      z := y;  // error: not allowed, because the P in the guard makes this a ghost context

+    } else if y :| 0 <= y < 100 && R(y) {

+      z := y;  // error: this is also in a ghost context, because it depends on the P above

+    }

+

+    if * {

+      z := z + -z;

+    } else if exists y :: 1000 <= y < 2000 && R(y) {

+      z := 0;

+    } else if exists y :: 0 <= y < 100 && P(y) {

+      z := 0;  // error: not allowed, because the P in the guard makes this a ghost context

+    } else if exists y :: 0 <= y < 100 && R(y) {

+      z := 0;  // error: this is also in a ghost context, because it depends on the P above

+    }

+

+    if P(z) {

+      z := 20;  // error: blatant ghost context

+    }

+

+    b := exists y :: 0 <= y < 100 && P(y);  // error: assignment to non-ghost of something that depends on ghost

+    ghost var c;

+    c := exists y :: 0 <= y < 100 && P(y);

+    b := exists y {:myattribute P(y)} :: 0 <= y < 100;

+  }

+}

diff --git a/Test/dafny0/ExistentialGuardsResolution.dfy.expect b/Test/dafny0/ExistentialGuardsResolution.dfy.expect
new file mode 100644
index 00000000..681bb13d
--- /dev/null
+++ b/Test/dafny0/ExistentialGuardsResolution.dfy.expect
@@ -0,0 +1,167 @@
+// Dafny program verifier version 1.9.5.20511, Copyright (c) 2003-2015, Microsoft.

+// Command Line Options: -nologo -countVerificationErrors:0 -useBaseNameForFileName /dprint:- C:\dafny\Test\dafny0\ExistentialGuardsResolution.dfy

+// ExistentialGuardsResolution.dfy

+

+

+module TypesNotFullyDetermined {

+  method T0()

+  {

+    if x :| true {

+    }

+  }

+

+  method T1()

+  {

+    if x :| true {

+      var y := x + 3;

+    }

+  }

+}

+

+module Ghost {

+  predicate P(x: int)

+

+  predicate method R(x: int)

+

+  method M7() returns (z: int, b: bool)

+  {

+    if * {

+      z := z + -z;

+    } else if y :| 1000 <= y < 2000 && R(y) {

+      z := y;

+    } else if y :| 0 <= y < 100 && P(y) {

+      z := y;

+    } else if y :| 0 <= y < 100 && R(y) {

+      z := y;

+    }

+    if * {

+      z := z + -z;

+    } else if exists y :: 1000 <= y < 2000 && R(y) {

+      z := 0;

+    } else if exists y :: 0 <= y < 100 && P(y) {

+      z := 0;

+    } else if exists y :: 0 <= y < 100 && R(y) {

+      z := 0;

+    }

+    if P(z) {

+      z := 20;

+    }

+    b := exists y :: 0 <= y < 100 && P(y);

+    ghost var c;

+    c := exists y :: 0 <= y < 100 && P(y);

+    b := exists y {:myattribute P(y)} :: 0 <= y < 100;

+  }

+}

+predicate P(n: int)

+

+predicate R(r: real)

+

+method M0()

+{

+  if x :| P(x) {

+    var y := x + 3;

+    var x := true;

+  }

+}

+

+method M1()

+{

+  if x: int :| P(x) {

+    x := x + 1;

+  }

+}

+

+method M2()

+{

+  var x := true;

+  if x, y :| P(x) && R(y) {

+    var z := x + 12;

+  }

+  x := x && false;

+}

+

+method M3()

+{

+  var x := true;

+  if x: int, y :| P(x) && R(y) {

+    var z := x + int(y);

+    var w := real(x) + y;

+  }

+  var x := 0.0;

+}

+

+method M4()

+{

+  if x, y: real :| P(x) && R(y) {

+  }

+}

+

+method M5()

+{

+  if x: int, y: real :| P(x) && R(y) {

+  }

+}

+

+method M6()

+{

+  if x {:myattribute x, "hello"} :| P(x) {

+  }

+  if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {

+  }

+  if x: int {:myattribute x, "chello"} :| P(x) {

+  }

+  if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {

+  }

+}

+

+method M7()

+{

+  if x :| P(x) {

+  } else if * {

+  } else if y :| R(y) {

+  } else if y :| P(y) {

+  }

+}

+

+method P0(m: int, n: int)

+  requires m < n

+{

+  var x := true;

+  if {

+    case x :| P(x) =>

+      var t := 3 * x;

+    case x: int :| P(x) =>

+    case x, y :| P(x) && R(y) =>

+      y := y + 1.0;

+    case x: int, y :| P(x) && R(y) =>

+    case m < n =>

+      x := x || m + 5 == n;

+    case x, y: real :| P(x) && R(y) =>

+    case x: int, y: real :| P(x) && R(y) =>

+  }

+  assert x;

+}

+

+method P1(m: int, n: int)

+  requires m < n

+{

+  if {

+    case x {:myattribute x, "hello"} :| P(x) =>

+    case x, y {:myattribute y, "sveika"} :| P(x) && R(y) =>

+    case x: int {:myattribute x, "chello"} :| P(x) =>

+    case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) =>

+    case m < n =>

+  }

+}

+ExistentialGuardsResolution.dfy(109,7): Error: type of bound variable 'x' could not be determined; please specify the type explicitly

+ExistentialGuardsResolution.dfy(130,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+ExistentialGuardsResolution.dfy(132,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+ExistentialGuardsResolution.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+ExistentialGuardsResolution.dfy(142,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+ExistentialGuardsResolution.dfy(146,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+ExistentialGuardsResolution.dfy(149,37): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

+ExistentialGuardsResolution.dfy(12,8): Error: Duplicate local-variable name: x

+ExistentialGuardsResolution.dfy(19,4): Error: LHS of assignment must denote a mutable variable

+ExistentialGuardsResolution.dfy(39,6): Error: Duplicate local-variable name: x

+ExistentialGuardsResolution.dfy(84,6): Error: LHS of assignment must denote a mutable variable

+11 resolution/type errors detected in ExistentialGuardsResolution.dfy

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index e935c83d..58ba6701 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1692,3 +1692,23 @@ module LoopResolutionTests {
     }

   }

 }

+

+module UnderspecifiedTypesInAttributes {

+  function method P<T>(x: T): int

+  method M() {

+    var {:myattr var u :| true; 6} v: int;  // error: type of u is underspecified

+    var j {:myattr var u :| true; 6} :| 0 <= j < 100;  // error: type of u is underspecified

+

+    var a := new int[100];

+    forall lp {:myattr var u :| true; 6} | 0 <= lp < 100 {  // error: type of u is underspecified

+      a[lp] := 0;

+    }

+

+    modify {:myattr P(10)} {:myattr var u :| true; 6} a;  // error: type of u is underspecified

+

+    calc {:myattr P(10)} {:myattr var u :| true; 6} // error: type of u is underspecified

+    {

+      5;

+    }

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index be19eeac..b055184f 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -161,6 +161,11 @@ ResolutionErrors.dfy(1673,4): Error: 'decreases *' is not allowed on ghost loops
 ResolutionErrors.dfy(1677,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

 ResolutionErrors.dfy(1687,4): Error: 'decreases *' is not allowed on ghost loops

 ResolutionErrors.dfy(1691,29): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+ResolutionErrors.dfy(1699,17): Error: the type of the bound variable 'u' could not be determined

+ResolutionErrors.dfy(1700,19): Error: the type of the bound variable 'u' could not be determined

+ResolutionErrors.dfy(1703,23): Error: the type of the bound variable 'u' could not be determined

+ResolutionErrors.dfy(1707,36): Error: the type of the bound variable 'u' could not be determined

+ResolutionErrors.dfy(1709,34): Error: the type of the bound variable 'u' could not be determined

 ResolutionErrors.dfy(469,2): Error: More than one anonymous constructor

 ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')

@@ -224,4 +229,4 @@ ResolutionErrors.dfy(1123,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1144,13): Error: first argument to / must be of numeric type (instead got set<bool>)

 ResolutionErrors.dfy(1151,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

 ResolutionErrors.dfy(1166,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-226 resolution/type errors detected in ResolutionErrors.dfy

+231 resolution/type errors detected in ResolutionErrors.dfy