Merge my autoTriggers work into the master branch

This contains trigger related things under the autoTriggers flag (disabled by default), and some bug-fixes and cleanups that are already enabled.
author: Clément Pit--Claudel <clement.pitclaudel@live.com> 2015-07-17 17:25:10 -0700
committer: Clément Pit--Claudel <clement.pitclaudel@live.com> 2015-07-17 17:25:10 -0700
commit: 7c766a43a77845ed1af5a0e5367e7a21edf13a8f (patch)
tree: 21911b3d9a25d4cc74dca3f831a635929428b993 /Test
parent: fc6ebea9b9ec614e4e014c64d9cad7940deb86fb (diff)
parent: 61a5be0930c43694d270809ed5550c74b6e59e5d (diff)
58 files changed, 1547 insertions, 167 deletions
diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy
index 10ad2d3a..4205035d 100644
--- a/Test/VerifyThis2015/Problem3.dfy
+++ b/Test/VerifyThis2015/Problem3.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:5 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Rustan Leino
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index c8fa76c8..89b0f02a 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -100,7 +100,7 @@ method ExpliesAssociativityM(A: bool, B: bool, C: bool) {
   }
 }
 
-method ExpliesShortCircuiting(a: array<T>)
+method ExpliesShortCircuiting(a: array)
 {
   assert a == null || 0 <= a.Length;  // (W)
   assert a != null ==> 0 <= a.Length;  // (X) -- same as (W)
diff --git a/Test/dafny0/EqualityTypes.dfy b/Test/dafny0/EqualityTypes.dfy
index b2812759..c510cfb1 100644
--- a/Test/dafny0/EqualityTypes.dfy
+++ b/Test/dafny0/EqualityTypes.dfy
@@ -241,3 +241,115 @@ module Deep {
     var m1 := map[ko := 5];  // error: bad type
   }
 }
+
+//--------------------------
+
+module UnderspecifiedTypeParameters {
+  method UP<T>()
+  function method UG<T>(): int
+  method Callee<T(==)>()
+  class TakesParam<U> { }
+  
+  method MPG()
+  {
+    var g := UG();  // error: type parameter underspecified
+    UP();  // error: type parameter underspecified
+  }
+  method M() {
+    var zs: set;  // error: type is underspecified
+    Callee<(int)>();
+    Callee<set>();  // error: type is underspecified
+    Callee<()>();
+    // The following 
+    Callee<TakesParam>();  // error: type is underspecified
+  }
+}
+
+module EqualitySupportingTypes {
+  method P<T>()
+  function method G<T>(): int
+  class AClass<V(==),Y> {
+    static function method H<W,X(==)>(): bool
+    static method Q<A,B(==)>()
+  }
+
+  method Callee<T(==)>()
+  function method FCallee<T>(): T
+
+  datatype Dt = Dt(f: int -> int)
+  codatatype Stream<T> = Cons(T, Stream)
+
+  method M<ArbitraryTypeArg>()
+  {
+    Callee<Dt>();  // error:  Dt is not an equality-supporting type
+    Callee<Stream<int>>();  // error: specified type does not support equality
+
+    // set<X> is allowed in a non-ghost context only if X is equality supporting.
+    // Ditto for multiset<X> and map<X,Y>.
+    var s3x: set<Dt>;  // error: this type not allowed in a non-ghost context
+    var is3x: iset<Dt>;  // error: this type not allowed in a non-ghost context
+    var mast: multiset<ArbitraryTypeArg>;  // error: this type not allowed in a non-ghost context
+    var qt: seq<Stream<int>>;  // allowed
+    var mp0: map<Dt,int>;  // error: this type not allowed in a non-ghost context
+    var mp1: map<int,Dt>;  // allowed
+    var imp0: imap<Dt,int>;  // error: this type not allowed in a non-ghost context
+    var imp1: imap<int,Dt>;  // allowed
+
+    var S := FCallee<set>();  // this gives s:set<?>
+    if 4 in S {              // this constrains the type further to be s:set<int>
+    }
+
+    var xy: set<set<int>>;
+    var xz: set<set<Stream<int>>>;  // error: set type argument must support equality
+    
+    Callee<set<Stream<int>>>();  // bogus: a set shouldn't ever be allowed to take a Stream as an argument (this check seems to be missing for explicit type arguments)  -- Note: language definition should be changed, because it doesn't make sense for it to talk about a type appearing in a ghost or non-ghost context. Instead, set/iset/multiset/map/imap should always be allowed to take any type argument, but these types may or may not support equality.
+    var xg := G<set<Stream<int>>>();
+    
+    var ac0: AClass<int,int>;
+    var ac1: AClass<Stream<int>,int>;  // error: type parameter 0 is required to support equality
+    var ac2: AClass<int,Stream<int>>;
+    var xd0 := ac0.H<real,real>();
+    var xd1 := ac1.H<Stream<real>,real>();  // error (remnant of the fact that the type of ac1 is not allowed)
+    var xd2 := ac2.H<real,Stream<real>>();  // error: type parameter 1 is required to support equality
+    var xe0 := ac0.H<real,real>;
+    var xe1 := ac1.H<Stream<real>,real>;  // error (remnant of the fact that the type of ac1 is not allowed)
+    var xe2 := ac2.H<real,Stream<real>>;  // error: type parameter 1 is required to support equality
+    var xh0 := AClass<int,int>.H<real,real>();
+    var xh1 := AClass<int,int>.H<Stream<real>,real>();
+    var xh2 := AClass<int,int>.H<real,Stream<real>>();  // error: type parameter 1 is required to support equality
+    var xk0 := AClass<real,real>.H<int,int>;
+    var xk1 := AClass<Stream<real>,real>.H<int,int>;  // error: class type param 0 wants an equality-supporting type
+    var xk2 := AClass<real,Stream<real>>.H<int,int>;
+    AClass<Stream<int>,int>.Q<real,real>();  // error: class type param 0 wants an equality-supporting type
+    AClass<int,Stream<int>>.Q<real,real>();
+    AClass<int,Stream<int>>.Q<Stream<real>,real>();
+    AClass<int,Stream<int>>.Q<real,Stream<real>>();  // error: method type param 1 wants an equality-supporting type
+  
+/*************************** TESTS YET TO COME
+    var ac8: AClass<real,real>;
+    var xd8 := (if 5/0 == 3 then ac0 else ac8).H<real,real>();  // error: this should be checked by the verifier
+
+    AClass<int,set<Stream<int>>>.Q<real,real>();  // error: cannot utter "set<Stream<int>>"   Or is that okay???
+    AClass<int,int>.Q<set<Stream<real>>,real>();  // error: cannot utter "set<Stream<real>>"   Or is that okay???
+    var xi0 := AClass<int,set<Stream<int>>>.H<real,real>();  // error: cannot utter "set<Stream<int>>"   Or is that okay???
+    var xi1 := AClass<int,int>.H<real,set<Stream<real>>>();  // error: cannot utter "set<Stream<real>>"   Or is that okay???
+
+    var x, t, s: seq<int -> int>, fii: int -> int;
+    if s == t {
+      x := 5;  // error: assigning to non-ghost variable in ghost context
+    }
+    if fii in s {
+      x := 4;  // error: assigning to non-ghost variable in ghost context
+    }
+    if !(fii in s) {
+      x := 3;  // error: assigning to non-ghost variable in ghost context
+    }
+
+    ghost var ghostset: set<Stream<int>> := {};  // fine, since this is ghost
+    forall u | 0 <= u < 100
+      ensures var lets: set<Stream<int>> := {}; lets == lets  // this is ghost, so the equality requirement doesn't apply
+    {
+    }
+*********************************************/
+  }
+}
diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect
index 9f277582..1c02f3a0 100644
--- a/Test/dafny0/EqualityTypes.dfy.expect
+++ b/Test/dafny0/EqualityTypes.dfy.expect
@@ -35,4 +35,26 @@ EqualityTypes.dfy(238,24): Error: set argument type must support equality (got C
 EqualityTypes.dfy(239,21): Error: multiset argument type must support equality (got Co)
 EqualityTypes.dfy(241,8): Error: map domain type must support equality (got Co)
 EqualityTypes.dfy(241,14): Error: map domain type must support equality (got Co)
-37 resolution/type errors detected in EqualityTypes.dfy
+EqualityTypes.dfy(255,13): Error: type variable 'T' in the function call to 'UG' could not be determined
+EqualityTypes.dfy(256,4): Error: type '?' to the method 'UP' is not determined
+EqualityTypes.dfy(259,8): Error: the type of this local variable is underspecified
+EqualityTypes.dfy(261,4): Error: type 'set<?>' to the method 'Callee' is not determined
+EqualityTypes.dfy(264,4): Error: type 'TakesParam<?>' to the method 'Callee' is not determined
+EqualityTypes.dfy(284,14): Error: type parameter 0 (T) passed to method Callee must support equality (got Dt)
+EqualityTypes.dfy(285,23): Error: type parameter 0 (T) passed to method Callee must support equality (got Stream<int>)
+EqualityTypes.dfy(289,8): Error: set argument type must support equality (got Dt)
+EqualityTypes.dfy(290,8): Error: iset argument type must support equality (got Dt)
+EqualityTypes.dfy(291,8): Error: multiset argument type must support equality (got ArbitraryTypeArg) (perhaps try declaring type parameter 'ArbitraryTypeArg' on line 282 as 'ArbitraryTypeArg(==)', which says it can only be instantiated with a type that supports equality)
+EqualityTypes.dfy(293,8): Error: map domain type must support equality (got Dt)
+EqualityTypes.dfy(295,8): Error: imap domain type must support equality (got Dt)
+EqualityTypes.dfy(303,8): Error: set argument type must support equality (got Stream<int>)
+EqualityTypes.dfy(309,8): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream<int>)
+EqualityTypes.dfy(312,19): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream<int>)
+EqualityTypes.dfy(313,19): Error: type parameter 1 (X) passed to function H must support equality (got Stream<real>)
+EqualityTypes.dfy(315,19): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream<int>)
+EqualityTypes.dfy(316,19): Error: type parameter 1 (X) passed to function 'H' must support equality (got Stream<real>)
+EqualityTypes.dfy(319,31): Error: type parameter 1 (X) passed to function H must support equality (got Stream<real>)
+EqualityTypes.dfy(321,41): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream<real>)
+EqualityTypes.dfy(323,28): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream<int>)
+EqualityTypes.dfy(326,48): Error: type parameter 1 (B) passed to method Q must support equality (got Stream<real>)
+59 resolution/type errors detected in EqualityTypes.dfy
diff --git a/Test/dafny0/Fuel.dfy b/Test/dafny0/Fuel.dfy
new file mode 100644
index 00000000..c8a1fc2f
--- /dev/null
+++ b/Test/dafny0/Fuel.dfy
@@ -0,0 +1,423 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module TestModule1 {
+    function pos(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos(x - 1)
+    }
+
+    method test(y:int, z:int) 
+        requires y > 5;
+        requires z < 0;
+    {
+        assert pos(z) == 0;
+        assert pos(-1) == 0;
+        assert pos(y) == 3 + pos(y - 3);    // error: Should fail, due to lack of fuel
+        assert pos(y) == 4 + pos(y - 4);    // Succeeds, thanks to the assume from the preceding assert
+    }
+}
+
+// Test with function-level fuel boost
+module TestModule2 {
+    function {:fuel 3} pos1(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos1(x - 1)
+    }
+
+    function {:fuel 3,5} pos2(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos2(x - 1)
+    }
+
+    function {:fuel 3,5} pos3(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos3(x - 1)
+    }
+
+    function {:opaque} {:fuel 3,5} pos4(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos3(x - 1)
+    }
+
+    method test(y:int, z:int) 
+        requires y > 5;
+        requires z < 0;
+    {
+        assert pos1(z) == 0;
+        assert pos1(-1) == 0;
+        assert pos1(y) == 3 + pos1(y - 3);
+        assert pos1(y) == 4 + pos1(y - 4);
+
+        assert pos2(z) == 0;
+        assert pos2(-1) == 0;
+        assert pos2(y) == 3 + pos2(y - 3);
+        assert pos2(y) == 4 + pos2(y - 4);
+
+        if (*) {
+            assert pos3(y) == 5 + pos3(y - 5);  // Just enough fuel to get here
+        } else {
+            assert pos3(y) == 6 + pos3(y - 6);  // error: Should fail even with a boost, since boost is too small
+        }
+
+        if (*) {
+            assert pos4(z) == 0;    // error: Fuel shouldn't overcome opaque
+        } else {
+            reveal_pos4();
+            assert pos4(y) == 5 + pos4(y - 5);  // With reveal, everything should work as above
+        }
+
+
+    }
+}
+
+
+module TestModule3 {
+    // This fuel setting is equivalent to opaque, except for literals
+    function {:fuel 0,0} pos(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos(x - 1)
+    }
+
+    method test(y:int, z:int) 
+        requires y > 5;
+        requires z < 0;
+    {
+        assert pos(z) == 0;             // error: Opaque setting hides body
+        assert pos(-1) == 0;            // Passes, since Dafny's computation mode for lits ignore fuel
+        assert pos(y) == 3 + pos(y - 3);// error: Opaque setting hides body
+    }
+}
+
+// Test fuel settings via different contexts
+module TestModule4 {
+    function pos(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos(x - 1)
+    }
+
+    // Should pass
+    method {:fuel pos,3,5} test1(y:int, z:int) 
+        requires y > 5;
+        requires z < 0;
+    {
+        assert pos(z) == 0;
+        assert pos(-1) == 0;
+        assert pos(y) == 3 + pos(y - 3);
+    }
+
+    method {:fuel pos,0,0} test2(y:int, z:int) 
+        requires y > 5;
+        requires z < 0;
+    {
+        assert pos(z) == 0;               // error: Should fail due to "opaque" fuel setting
+        assert pos(-1) == 0;
+        assert pos(y) == 3 + pos(y - 3);  // error: Should fail due to "opaque" fuel setting
+    }
+
+    method test3(y:int, z:int) 
+        requires y > 5;
+        requires z < 0;
+    {
+        assert {:fuel pos,0,0} pos(z) == 0;               // error: Should fail due to "opaque" fuel setting
+        assert pos(-1) == 0;
+        if (*) {
+            assert pos(y) == 3 + pos(y - 3);  // error: Should fail without extra fuel setting
+            assert pos(y) == 6 + pos(y - 6);  // error: Should fail even with previous assert turned into assume
+        } else {
+            assert {:fuel pos,3,5} pos(y) == 3 + pos(y - 3);  // Should succeed with extra fuel setting
+            assert pos(y) == 6 + pos(y - 6);  // Should succeed thanks to previous assert turned into assume
+        } 
+    }
+
+    method test4(y:int, z:int) 
+        requires y > 5;
+        requires z < 0;
+    {
+        forall t:int {:fuel pos,3} | t > 0 
+            ensures true;
+        {
+            assert pos(y) == 3 + pos(y - 3);    // Expected to pass, due to local fuel boost
+        }
+
+        if (*) {
+            calc {:fuel pos,3} {
+                pos(y);
+                3 + pos(y - 3);
+            }
+        }
+
+        assert pos(y) == 3 + pos(y - 3);    // error: Should fail, due to lack of fuel outside the forall
+    }
+}
+
+// Test fuel settings via different module contexts
+module TestModule5 {
+    // Test module level fuel settings, with nested modules
+
+    module TestModule5a {
+        module {:fuel TestModule5aiA.pos,3} TestModule5ai {
+            module TestModule5aiA {
+                function pos(x:int) : int 
+                {
+                    if x < 0 then 0
+                    else 1 + pos(x - 1)
+                }
+
+                method test(y:int, z:int) 
+                    requires y > 5;
+                    requires z < 0;
+                {
+                    assert pos(z) == 0;
+                    assert pos(-1) == 0;
+                    assert pos(y) == 3 + pos(y - 3);    // Should pass due to intermediate module's fuel setting
+                }
+            }
+
+            method test(y:int, z:int) 
+                requires y > 5;
+                requires z < 0;
+            {
+                assert TestModule5aiA.pos(z) == 0;
+                assert TestModule5aiA.pos(-1) == 0;
+                assert TestModule5aiA.pos(y) == 3 + TestModule5aiA.pos(y - 3);    // Should pass due to module level fuel
+            }
+        }
+  
+        method test(y:int, z:int) 
+            requires y > 5;
+            requires z < 0;
+        {
+            assert TestModule5ai.TestModule5aiA.pos(z) == 0;
+            assert TestModule5ai.TestModule5aiA.pos(-1) == 0;
+            assert TestModule5ai.TestModule5aiA.pos(y) == 3 + TestModule5ai.TestModule5aiA.pos(y - 3);    // error: Should fail, due to lack of fuel
+        }
+    }
+
+    module {:fuel TestModule5bi.TestModule5biA.pos,3} TestModule5b {
+        module  TestModule5bi {
+            module TestModule5biA {
+                function pos(x:int) : int 
+                {
+                    if x < 0 then 0
+                    else 1 + pos(x - 1)
+                }
+
+                method test(y:int, z:int) 
+                    requires y > 5;
+                    requires z < 0;
+                {
+                    assert pos(z) == 0;
+                    assert pos(-1) == 0;
+                    assert pos(y) == 3 + pos(y - 3);    // Should succceed due to outer module fuel setting
+                }
+            }
+        }
+    }
+}
+
+// Test fuel setting for multiple functions
+module TestModule6 {
+    function pos(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos(x - 1)
+    }
+
+    function neg(x:int) : int
+        decreases 1 - x;
+    {
+        if x > 0 then 0
+        else 1 + neg(x + 1)
+    }
+
+    method test1(y:int, z:int) 
+        requires y > 5;
+        requires z < 5;
+    {
+        assert pos(y) == 3 + pos(y - 3);    // error: Should fail, due to lack of fuel
+
+        assert neg(z) == 3 + neg(z + 3);    // error: Should fail, due to lack of fuel
+    }
+
+    method {:fuel pos,3} {:fuel neg,4} test2(y:int, z:int) 
+        requires y > 5;
+        requires z < -5;
+    {
+        assert pos(y) == 3 + pos(y - 3);    
+
+        assert neg(z) == 3 + neg(z + 3);    
+    }
+}
+
+// Test fuel settings with multiple overlapping contexts
+module TestModule7 {
+    function {:fuel 3} pos(x:int) : int 
+    {
+        if x < 0 then 0
+        else 1 + pos(x - 1)
+    }
+
+    function {:fuel 0,0} neg(x:int) : int
+        decreases 1 - x;
+    {
+        if x > 0 then 0
+        else 1 + neg(x + 1)
+    }
+
+    method {:fuel neg,4} {:fuel pos,0,0} test1(y:int, z:int) 
+        requires y > 5;
+        requires z < -5;
+    {
+        if (*) {
+            assert pos(y) == 3 + pos(y - 3);    // error: Method fuel should override function fuel, so this should fail
+            assert neg(z) == 3 + neg(z + 3);    // Method fuel should override function fuel, so this succeeds
+        }
+
+        forall t:int {:fuel pos,3} | t > 0 
+            ensures true;
+        {
+            assert pos(y) == 3 + pos(y - 3);    // Statement fuel should override method fuel, so this should succeed
+        }
+    }
+}
+
+// Test fuel in a slightly more complicated setting
+module TestModule8 {
+
+    newtype byte = i:int | 0 <= i < 0x100
+    newtype uint64 = i:int | 0 <= i < 0x10000000000000000
+
+    datatype G = GUint64
+               | GArray(elt:G)
+               | GTuple(t:seq<G>)
+               | GByteArray
+               | GTaggedUnion(cases:seq<G>)
+
+        datatype V = VUint64(u:uint64)
+                   | VTuple(t:seq<V>)
+                   | VCase(c:uint64, val:V)
+
+        predicate {:fuel 2} ValInGrammar(val:V, grammar:G)
+        {
+            match val
+                case VUint64(_) => grammar.GUint64?
+                case VTuple(t)  => grammar.GTuple? && |t| == |grammar.t|
+                                      && forall i :: 0 <= i < |t| ==> ValInGrammar(t[i], grammar.t[i])
+                case VCase(c, val) => grammar.GTaggedUnion? && int(c) < |grammar.cases| && ValInGrammar(val, grammar.cases[c])
+        }
+
+        datatype CRequest = CRequest(client:EndPoint, seqno:uint64, request:CAppMessage) | CRequestNoOp()
+
+        type EndPoint
+        function method EndPoint_grammar() : G { GUint64 }
+        function method CRequest_grammar() : G { GTaggedUnion([ GTuple([EndPoint_grammar(), GUint64, CAppMessage_grammar()]), GUint64]) }
+
+        function method parse_EndPoint(val:V) : EndPoint
+            requires ValInGrammar(val, EndPoint_grammar());
+
+        type CAppMessage
+        function method CAppMessage_grammar() : G { GTaggedUnion([GUint64, GUint64, GUint64]) }
+        function method parse_AppMessage(val:V) : CAppMessage
+            requires ValInGrammar(val, CAppMessage_grammar());
+
+        function method {:fuel ValInGrammar,1,2} parse_Request1(val:V) : CRequest
+            requires ValInGrammar(val, CRequest_grammar());
+        {
+            if val.c == 0 then
+                var ep := parse_EndPoint(val.val.t[0]); // With default fuel, error: function precondition, destructor, index
+                CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2]))    // error: index out of range, destructor
+            else 
+                CRequestNoOp()
+        }
+
+        function method parse_Request2(val:V) : CRequest
+            requires ValInGrammar(val, CRequest_grammar());
+        {
+            if val.c == 0 then
+                var ep := parse_EndPoint(val.val.t[0]);                      // With fuel boosted to 2 this succeeds
+                CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2])) // error: destructor
+            else 
+                CRequestNoOp()
+        }
+
+        function method {:fuel ValInGrammar,3} parse_Request3(val:V) : CRequest
+            requires ValInGrammar(val, CRequest_grammar());
+        {
+            if val.c == 0 then
+                var ep := parse_EndPoint(val.val.t[0]); 
+                CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2]))    // With one more boost, everything succeeds
+            else 
+                CRequestNoOp()
+        }
+
+        // With the method, everything succeeds with one less fuel boost (i.e., 2, rather than 3, as in parse_Request3)
+        method parse_Request4(val:V) returns (req:CRequest)     
+            requires ValInGrammar(val, CRequest_grammar());
+        {
+            if val.c == 0 {
+                var ep := parse_EndPoint(val.val.t[0]);
+                req := CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2]));
+            } else {
+                req := CRequestNoOp();
+            }
+        }
+}
+
+
+// Test fuel when it's applied to a non-recursive function
+module TestModule9 {
+    function abs(x:int) : int
+    {
+        if x < 0 then -1 * x else x
+    }
+
+    // All should pass.
+    method test1(y:int, z:int)
+        requires y > 5;
+        requires z < 0;
+    {
+        assert abs(z) == -1*z;
+        assert abs(y) == y;
+        assert abs(-1) == 1;
+    }
+
+    // Method-level fuel override
+    method {:fuel abs,0,0} test2(y:int, z:int)
+        requires y > 5;
+        requires z < 0;
+    {
+        assert abs(z) == -1*z;  // error: Cannot see the body of abs
+        assert abs(y) == y;     // error: Cannot see the body of abs
+        assert abs(-1) == 1;    // lit bypasses fuel, so this should succeed
+    }
+
+    // Statement-level fuel override
+    method test3(y:int, z:int)
+        requires y > 5;
+        requires z < 0;
+    {
+        assert {:fuel abs,0,0} abs(z) == -1*z;  // error: Cannot see the body of abs
+        assert abs(y) == y;     // Normal success
+        assert abs(-1) == 1;    // lit bypasses fuel, so this should succeed
+    }
+
+    // Giving more fuel to a non-recursive function won't help,
+    // but it shouldn't hurt either.
+    method {:fuel abs,5,7} test4(y:int, z:int)
+        requires y > 5;
+        requires z < 0;
+    {
+        assert abs(z) == -1*z;
+        assert abs(y) == y;
+        assert abs(-1) == 1;
+    }
+}
+
diff --git a/Test/dafny0/Fuel.dfy.expect b/Test/dafny0/Fuel.dfy.expect
new file mode 100644
index 00000000..4c180a9c
--- /dev/null
+++ b/Test/dafny0/Fuel.dfy.expect
@@ -0,0 +1,95 @@
+Fuel.dfy(17,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(65,28): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon6_Else
+Fuel.dfy(69,28): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon6_Then
+    (0,0): anon7_Then
+Fuel.dfy(92,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(94,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(120,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(122,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(129,39): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(132,27): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Then
+Fuel.dfy(133,27): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Then
+Fuel.dfy(157,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon10_Else
+    (0,0): anon9
+Fuel.dfy(200,56): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(245,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(247,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(280,27): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Then
+Fuel.dfy(335,27): Error: possible violation of function precondition
+Fuel.dfy(324,22): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(335,50): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple'
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(335,51): Error: index out of range
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(336,39): Error: index out of range
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(336,43): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64'
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(346,43): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64'
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(397,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(398,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(407,39): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 51 verified, 24 errors
diff --git a/Test/dafny0/JustWarnings.dfy b/Test/dafny0/JustWarnings.dfy
new file mode 100644
index 00000000..86523f5b
--- /dev/null
+++ b/Test/dafny0/JustWarnings.dfy
@@ -0,0 +1,19 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /warnShadowing "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file tests the behavior where the Resolver reports some warnings
+// but no errors.  In the case of errors, resolution does not continue
+// to clone modules and resolve them, but the cloning does proceed if there
+// are only warnings.  Dafny should report only one copy of these warnings,
+// and warnings are therefore turned off when processing the clones.  This
+// test file makes sure the warnings don't appear twice.
+
+method M(x: int)
+{
+  var x := 10;  // warning: this shadows the parameter 'x'
+}
+
+class C<T> {
+  var u: T
+  method P<T>(t: T)  // warning: this shadows the type parameter 'T'
+}
diff --git a/Test/dafny0/JustWarnings.dfy.expect b/Test/dafny0/JustWarnings.dfy.expect
new file mode 100644
index 00000000..5f0e66d8
--- /dev/null
+++ b/Test/dafny0/JustWarnings.dfy.expect
@@ -0,0 +1,4 @@
+JustWarnings.dfy(18,11): Warning: Shadowed type-parameter name: T
+JustWarnings.dfy(13,6): Warning: Shadowed local-variable name: x
+
+Dafny program verifier finished with 3 verified, 0 errors
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index 34aba3de..dbbffd87 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -71,16 +71,17 @@ module X1 {
 }
 
 module X2 {
+  import opened X1
   class MyClass2 {
-    method Down(x1: MyClass1, x0: MyClass0) {
+    method Down(x1: MyClass1, x0: X0'.MyClass0) {
       x1.Down(x0);
     }
-    method WayDown(x0: MyClass0) {
+    method WayDown(x0: X0'.MyClass0) {
       x0.Down();
     }
     method Up() {
     }
-    method Somewhere(y: MyClassY) {
+    method Somewhere(y: MyClassY) {  // error: no such type in scope
       y.M();
     }
   }
@@ -97,8 +98,7 @@ module YY {
 class ClassG {
   method T() { }
   function method TFunc(): int { 10 }
-  method V(y: MyClassY) {  // Note, MyClassY is in scope, since we are in the _default
-                           // module, which imports everything
+  method V(y: MyClassY) {
     y.M();
   }
 }
@@ -141,10 +141,10 @@ class AClassWithSomeField {
     SomeField := SomeField + 4;
     var a := old(SomeField);  // error: old can only be used in ghost contexts
     var b := fresh(this);  // error: fresh can only be used in ghost contexts
-    var c := allocated(this);  // error: allocated can only be used in ghost contexts
+//    var c := allocated(this);  // error: allocated can only be used in ghost contexts
     if (fresh(this)) {  // this guard makes the if statement a ghost statement
       ghost var x := old(SomeField);  // this is a ghost context, so it's okay
-      ghost var y := allocated(this);  // this is a ghost context, so it's okay
+//      ghost var y := allocated(this);  // this is a ghost context, so it's okay
     }
   }
 }
diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect
index 5d11f9c9..d2f0bcc8 100644
--- a/Test/dafny0/Modules0.dfy.expect
+++ b/Test/dafny0/Modules0.dfy.expect
@@ -9,13 +9,8 @@ Modules0.dfy(15,11): Error: Duplicate name of top-level declaration: WazzupB
 Modules0.dfy(56,21): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?)
 Modules0.dfy(57,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)
 Modules0.dfy(68,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)
-Modules0.dfy(76,9): Error: type MyClass1 does not have a member Down
-Modules0.dfy(76,13): Error: expected method call, found expression
-Modules0.dfy(79,9): Error: type MyClass0 does not have a member Down
-Modules0.dfy(79,13): Error: expected method call, found expression
-Modules0.dfy(84,8): Error: type MyClassY does not have a member M
-Modules0.dfy(84,9): Error: expected method call, found expression
-Modules0.dfy(92,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)
+Modules0.dfy(84,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)
+Modules0.dfy(93,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)
 Modules0.dfy(226,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
 Modules0.dfy(226,8): Error: new can be applied only to reference types (got X)
 Modules0.dfy(235,13): Error: module 'B' does not declare a type 'X'
@@ -35,11 +30,5 @@ Modules0.dfy(320,11): Error: Undeclared top-level type or type parameter: Wazzup
 Modules0.dfy(321,17): Error: module 'Q_Imp' does not declare a type 'Edon'
 Modules0.dfy(323,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)
 Modules0.dfy(324,30): Error: member Create does not exist in class Klassy
-Modules0.dfy(102,6): Error: type MyClassY does not have a member M
-Modules0.dfy(102,7): Error: expected method call, found expression
-Modules0.dfy(127,11): Error: ghost variables are allowed only in specification contexts
-Modules0.dfy(142,13): Error: old expressions are allowed only in specification and ghost contexts
-Modules0.dfy(143,13): Error: fresh expressions are allowed only in specification and ghost contexts
-Modules0.dfy(144,13): Error: unresolved identifier: allocated
-Modules0.dfy(147,21): Error: unresolved identifier: allocated
-42 resolution/type errors detected in Modules0.dfy
+Modules0.dfy(101,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)
+31 resolution/type errors detected in Modules0.dfy
diff --git a/Test/dafny0/NestedMatch.dfy b/Test/dafny0/NestedMatch.dfy
index e6e7c489..81319b4a 100644
--- a/Test/dafny0/NestedMatch.dfy
+++ b/Test/dafny0/NestedMatch.dfy
@@ -28,7 +28,7 @@ function last<T>(xs: List<T>): T
   case Cons(y, Cons(z, zs)) => last(Cons(z, zs))
 }
 
-method checkLast(y: T) {
+method checkLast<T>(y: T) {
   assert last(Cons(y, Nil)) == y;
   assert last(Cons(y, Cons(y, Nil))) == last(Cons(y, Nil));
 }
diff --git a/Test/dafny0/NestedPatterns.dfy b/Test/dafny0/NestedPatterns.dfy
index ef597936..d1d88b2a 100644
--- a/Test/dafny0/NestedPatterns.dfy
+++ b/Test/dafny0/NestedPatterns.dfy
@@ -69,7 +69,7 @@ method MethodG<T>(xs: List<T>) returns (xxs: List<List<T>>)
   case Cons(h, Cons(ht, tt)) => 
 }
 
-method AssertionFailure(xs: List<T>)
+method AssertionFailure(xs: List)
 {
   match xs
   case (Nil) =>  // BUG: this line causes an assertion in the Dafny implementation (what should happen is that "(Nil)" should not be allowed here)
@@ -100,7 +100,7 @@ method DuplicateIdentifierInPattern2<T>(xs: List<T>)
   case Cons(h, Cons(e, e)) =>  // BUG:  here, the duplicate identifier is detected, but the error message is shown 3 times, which is less than ideal
 }
 
-method Tuples0(xs: List<T>, ys: List<T>)
+method Tuples0(xs: List, ys: List)
 {
   match (xs, ys)
   case (Nil, Nil) =>
@@ -110,14 +110,14 @@ method Tuples0(xs: List<T>, ys: List<T>)
                                     // only the identifiers in the last constructors are
 }
 
-method Tuples1(xs: List<T>, ys: List<T>)
+method Tuples1(xs: List, ys: List)
 {
   match (xs, ys, 4)
   case (Nil, Nil) =>  // BUG: the mismatch of 3 versus 2 arguments in the previous line and this line causes Dafny to crash with an
                       // assertion failure "mc.CasePatterns.Count == e.Arguments.Count"
 }
 
-method Tuples2(xs: List<T>, ys: List<T>)
+method Tuples2(xs: List, ys: List)
 {
   match (xs, ys, ())
   case (Nil, Nil, ()) =>  // BUG: Dafny crashes with an assertion failure "e.Arguments.Count >= 1"
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 761cffa0..8c910959 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1253,14 +1253,14 @@ module SignatureCompletion {
   datatype Dt = Ctor(X -> Dt)  // error: X is not a declared type
   datatype Et<Y> = Ctor(X -> Et, Y)  // error: X is not a declared type
 
-  // For methods and functions, signatures can auto-declare type parameters
-  method My0(s: set, x: A -> B)
-  method My1(x: A -> B, s: set)
+
+  method My0<A,B>(s: set, x: A -> B)
+  method My1<A,B>(x: A -> B, s: set)
   method My2<A,B>(s: set, x: A -> B)
   method My3<A,B>(x: A -> B, s: set)
 
-  function F0(s: set, x: A -> B): int
-  function F1(x: A -> B, s: set): int
+  function F0<A,B>(s: set, x: A -> B): int
+  function F1<A,B>(x: A -> B, s: set): int
   function F2<A,B>(s: set, x: A -> B): int
   function F3<A,B>(x: A -> B, s: set): int
 }
diff --git a/Test/dafny0/Shadows.dfy b/Test/dafny0/Shadows.dfy
new file mode 100644
index 00000000..da1e74d6
--- /dev/null
+++ b/Test/dafny0/Shadows.dfy
@@ -0,0 +1,42 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /warnShadowing "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module Module0 {
+  class C<alpha> {
+    method M<beta, beta>(x: beta)  // error: duplicate type parameter
+    method P<alpha>(x: alpha)  // shadowed type parameter
+    function F<beta, beta>(x: beta): int  // error: duplicate type parameter
+    function G<alpha>(x: alpha): int  // shadowed type parameter
+
+    method Q0(x: int) returns (x: int)  // error: duplicate variable name
+  }
+}
+module Module1 {
+  class D {
+    method Q1(x: int) returns (y: int)
+    {
+      var x;  // shadowed
+      var y;  // error: duplicate
+    }
+
+    var f: int
+    method R()
+    {
+      var f;  // okay
+      var f;  // error: duplicate
+    }
+    method S()
+    {
+      var x;
+      {
+        var x;  // shadow
+      }
+    }
+    method T()
+    {
+      var x;
+      ghost var b := forall x :: x < 10;  // shadow
+      ghost var c := forall y :: forall y :: y != y + 1;  // shadow
+    }
+  }
+}
diff --git a/Test/dafny0/Shadows.dfy.expect b/Test/dafny0/Shadows.dfy.expect
new file mode 100644
index 00000000..5083ac64
--- /dev/null
+++ b/Test/dafny0/Shadows.dfy.expect
@@ -0,0 +1,12 @@
+Shadows.dfy(6,19): Error: Duplicate type-parameter name: beta
+Shadows.dfy(7,13): Warning: Shadowed type-parameter name: alpha
+Shadows.dfy(8,21): Error: Duplicate type-parameter name: beta
+Shadows.dfy(9,15): Warning: Shadowed type-parameter name: alpha
+Shadows.dfy(11,31): Error: Duplicate parameter name: x
+Shadows.dfy(18,10): Warning: Shadowed local-variable name: x
+Shadows.dfy(19,10): Error: Duplicate local-variable name: y
+Shadows.dfy(26,10): Error: Duplicate local-variable name: f
+Shadows.dfy(32,12): Warning: Shadowed local-variable name: x
+Shadows.dfy(38,28): Warning: Shadowed bound-variable name: x
+Shadows.dfy(39,40): Warning: Shadowed bound-variable name: y
+5 resolution/type errors detected in Shadows.dfy
diff --git a/Test/dafny0/Trait/TraitsDecreases.dfy b/Test/dafny0/Trait/TraitsDecreases.dfy
index 53ce28be..8ab3672a 100644
--- a/Test/dafny0/Trait/TraitsDecreases.dfy
+++ b/Test/dafny0/Trait/TraitsDecreases.dfy
@@ -106,3 +106,49 @@ class CC extends TT {
     decreases *
   { }
 }
+
+
+// The following module contains various regression tests
+module More {
+  trait A0 {
+    predicate P() decreases 5
+  }
+  class B0 extends A0 {
+    predicate P()  // error: rank is not lower
+  }
+
+  trait A1 {
+    predicate P() decreases 5
+  }
+  class B1 extends A1 {
+    predicate P() reads this  // error: rank is not lower
+  }
+
+  trait A2 {
+    predicate P(x: int)
+  }
+  class B2 extends A2 {
+    predicate P(x: int) reads this  // error: rank is not lower
+  }
+
+  trait A3 {
+    predicate P() reads this
+  }
+  class B3 extends A3 {
+    predicate P()  // error: rank is not lower
+  }
+
+  trait A4 {
+    predicate P(x: int) decreases 5
+  }
+  class B4 extends A4 {
+    predicate P(x: int)  // error: rank is not lower
+  }
+
+  trait A5 {
+    method M(x: int) decreases 5
+  }
+  class B5 extends A5 {
+    method M(x: int)  // error: rank is not lower
+  }
+}
diff --git a/Test/dafny0/Trait/TraitsDecreases.dfy.expect b/Test/dafny0/Trait/TraitsDecreases.dfy.expect
index 6c76f9a8..2607a0c6 100644
--- a/Test/dafny0/Trait/TraitsDecreases.dfy.expect
+++ b/Test/dafny0/Trait/TraitsDecreases.dfy.expect
@@ -1,3 +1,21 @@
+TraitsDecreases.dfy(117,15): Error: predicate's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
+TraitsDecreases.dfy(124,15): Error: predicate's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
+TraitsDecreases.dfy(131,15): Error: predicate's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
+TraitsDecreases.dfy(138,15): Error: predicate's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
+TraitsDecreases.dfy(145,15): Error: predicate's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
+TraitsDecreases.dfy(152,12): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
 TraitsDecreases.dfy(57,10): Error: method's decreases clause must be below or equal to that in the trait
 Execution trace:
     (0,0): anon0
@@ -14,4 +32,4 @@ TraitsDecreases.dfy(88,10): Error: method's decreases clause must be below or eq
 Execution trace:
     (0,0): anon0
 
-Dafny program verifier finished with 63 verified, 5 errors
+Dafny program verifier finished with 75 verified, 11 errors
diff --git a/Test/dafny4/Circ.dfy b/Test/dafny4/Circ.dfy
index e7609195..d110c05c 100644
--- a/Test/dafny4/Circ.dfy
+++ b/Test/dafny4/Circ.dfy
@@ -16,6 +16,7 @@ function zip(a: Stream, b: Stream): Stream { Cons(a.head, zip(b, a.tail)) }
 colemma BlinkZipProperty()
   ensures zip(zeros(), ones()) == blink();
 {
+    BlinkZipProperty();
 }
 
 // ----- Thue-Morse sequence -----
@@ -75,6 +76,7 @@ colemma FProperty(s: Stream<Bit>)
     // def. zip
     Cons(s.head, Cons(not(s).head, zip(s.tail, not(s).tail)));
   }
+  FProperty(s.tail);
 }
 
 // The fix-point theorem now follows easily.
diff --git a/Test/dafny4/NipkowKlein-chapter3.dfy b/Test/dafny4/NipkowKlein-chapter3.dfy
index ab45f536..725d68f6 100644
--- a/Test/dafny4/NipkowKlein-chapter3.dfy
+++ b/Test/dafny4/NipkowKlein-chapter3.dfy
@@ -131,6 +131,12 @@ lemma AsimpCorrect(a: aexp, s: state)
   forall a' | a' < a { AsimpCorrect(a', s); }
 }
 
+// The following lemma is not in the Nipkow and Klein book, but it's a fun one to prove.
+lemma ASimplInvolutive(a: aexp)
+  ensures asimp(asimp(a)) == asimp(a)
+{
+}
+
 // ----- boolean expressions -----
 
 datatype bexp = Bc(v: bool) | Not(bexp) | And(bexp, bexp) | Less(aexp, aexp)
diff --git a/Test/dafny4/NipkowKlein-chapter3.dfy.expect b/Test/dafny4/NipkowKlein-chapter3.dfy.expect
index ab18d98e..bb45fee9 100644
--- a/Test/dafny4/NipkowKlein-chapter3.dfy.expect
+++ b/Test/dafny4/NipkowKlein-chapter3.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 28 verified, 0 errors
+Dafny program verifier finished with 30 verified, 0 errors
diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy
index f51ae924..3dba6325 100644
--- a/Test/dafny4/NumberRepresentations.dfy
+++ b/Test/dafny4/NumberRepresentations.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /vcsMaxKeepGoingSplits:5 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // We consider a number representation that consists of a sequence of digits.  The least
diff --git a/Test/hofs/Classes.dfy b/Test/hofs/Classes.dfy
index 0ceb46f1..9d8044db 100644
--- a/Test/hofs/Classes.dfy
+++ b/Test/hofs/Classes.dfy
@@ -47,3 +47,20 @@ method U(t : T)
   t.h := x => x;
   assert J(t) == 0; // ok
 }
+
+class MyClass {
+  var data: int
+	function method F(): int
+	  reads this
+	{
+	  data
+	}	
+  method M(that: MyClass)
+	  requires that != null
+	{
+	  var fn := that.F;  // "that" is captured into the closure
+	  var d := fn();
+		assert d == that.data;  // yes
+		assert d == this.data;  // error: no reason to believe that this would hold
+	}	
+}
diff --git a/Test/hofs/Classes.dfy.expect b/Test/hofs/Classes.dfy.expect
index e490dbe0..1c9e31f0 100644
--- a/Test/hofs/Classes.dfy.expect
+++ b/Test/hofs/Classes.dfy.expect
@@ -1,7 +1,10 @@
+Classes.dfy(64,12): Error: assertion violation
+Execution trace:
+    (0,0): anon0
 Classes.dfy(40,6): Error: possible violation of function precondition
 Execution trace:
     (0,0): anon0
     (0,0): anon7_Else
     (0,0): anon8_Else
 
-Dafny program verifier finished with 6 verified, 1 error
+Dafny program verifier finished with 8 verified, 2 errors
diff --git a/Test/hofs/Examples.dfy b/Test/hofs/Examples.dfy
index be2672f5..306d278d 100644
--- a/Test/hofs/Examples.dfy
+++ b/Test/hofs/Examples.dfy
@@ -1,14 +1,14 @@
 // RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-function Apply(f: A -> B, x: A): B
+function Apply<A,B>(f: A -> B, x: A): B
   reads f.reads(x);
   requires f.requires(x);
 {
   f(x)
 }
 
-function Apply'(f: A -> B) : A -> B
+function Apply'<A,B>(f: A -> B) : A -> B
 {
   x reads f.reads(x)
     requires f.requires(x)
@@ -16,7 +16,7 @@ function Apply'(f: A -> B) : A -> B
 }
 
 
-function Compose(f: B -> C, g:A -> B): A -> C
+function Compose<A,B,C>(f: B -> C, g:A -> B): A -> C
 {
   x reads g.reads(x)
     reads if g.requires(x) then f.reads(g(x)) else {}
@@ -25,21 +25,21 @@ function Compose(f: B -> C, g:A -> B): A -> C
     => f(g(x))
 }
 
-function W(f : (A,A) -> A): A -> A
+function W<A>(f : (A,A) -> A): A -> A
 {
   x requires f.requires(x,x)
     reads f.reads(x,x)
     => f(x,x)
 }
 
-function Curry(f : (A,B) -> C) : A -> B -> C
+function Curry<A,B,C>(f : (A,B) -> C) : A -> B -> C
 {
   x => y requires f.requires(x,y)
          reads f.reads(x,y)
          => f(x,y)
 }
 
-function Uncurry(f : A -> B -> C) : (A,B) -> C
+function Uncurry<A,B,C>(f : A -> B -> C) : (A,B) -> C
 {
   (x,y) requires f.requires(x)
         requires f(x).requires(y)
@@ -48,7 +48,7 @@ function Uncurry(f : A -> B -> C) : (A,B) -> C
         => f(x)(y)
 }
 
-function S(f : (A,B) -> C, g : A -> B): A -> C
+function S<A,B,C>(f : (A,B) -> C, g : A -> B): A -> C
 {
   x requires g.requires(x)
     requires f.requires(x,g(x))
diff --git a/Test/hofs/Fold.dfy b/Test/hofs/Fold.dfy
index 6ca2d3b1..9bcd9e02 100644
--- a/Test/hofs/Fold.dfy
+++ b/Test/hofs/Fold.dfy
@@ -13,7 +13,7 @@ function method Eval(e : Expr): int
     case Lit(i)  => i
 }
 
-function method Fold(xs : List<A>, unit : B, f : (A,B) -> B): B
+function method Fold<A,B>(xs : List<A>, unit : B, f : (A,B) -> B): B
   reads f.reads;
   requires forall x, y :: x < xs ==> f.requires(x,y);
 {
diff --git a/Test/hofs/Monads.dfy b/Test/hofs/Monads.dfy
index 3598d2b3..633dd339 100644
--- a/Test/hofs/Monads.dfy
+++ b/Test/hofs/Monads.dfy
@@ -4,29 +4,29 @@
 abstract module Monad {
   type M<A>
 
-  function method Return(x: A): M<A>
-  function method Bind(m: M<A>, f:A -> M<B>):M<B>
-    reads f.reads;
-    requires forall a :: f.requires(a);
+  function method Return<A>(x: A): M<A>
+  function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B>
+    reads f.reads
+    requires forall a :: f.requires(a)
 
   // return x >>= f = f x
-  lemma LeftIdentity(x : A, f : A -> M<B>)
-    requires forall a :: f.requires(a);
-    ensures Bind(Return(x),f) == f(x);
+  lemma LeftIdentity<A,B>(x : A, f : A -> M<B>)
+    requires forall a :: f.requires(a)
+    ensures Bind(Return(x),f) == f(x)
 
   // m >>= return = m
-  lemma RightIdentity(m : M<A>)
-    ensures Bind(m,Return) == m;
+  lemma RightIdentity<A>(m : M<A>)
+    ensures Bind(m,Return) == m
 
   // (m >>= f) >>= g = m >>= (x => f(x) >>= g)
-  lemma Associativity(m : M<A>, f:A -> M<B>, g: B -> M<C>)
-    requires forall a :: f.requires(a);
-    requires forall b :: g.requires(b);
+  lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>)
+    requires forall a :: f.requires(a)
+    requires forall b :: g.requires(b)
 	ensures Bind(Bind(m,f),g) ==
 	        Bind(m,x reads f.reads(x)
 	                 reads g.reads
 					 requires f.requires(x)
-					 requires forall b :: g.requires(b) => Bind(f(x),g));
+					 requires forall b :: g.requires(b) => Bind(f(x),g))
 }
 
 module Identity refines Monad {
@@ -101,21 +101,21 @@ module List refines Monad {
   function method Return<A>(x: A): M<A>
   { Cons(x,Nil) }
 
-  function method Concat(xs: M<A>, ys: M<A>): M<A>
+  function method Concat<A>(xs: M<A>, ys: M<A>): M<A>
   {
     match xs
 	  case Nil => ys
 	  case Cons(x,xs) => Cons(x,Concat(xs,ys))
   }
 
-  function method Join(xss: M<M<A>>) : M<A>
+  function method Join<A>(xss: M<M<A>>) : M<A>
   {
     match xss
 	  case Nil => Nil
 	  case Cons(xs,xss) => Concat(xs,Join(xss))
   }
 
-  function method Map(xs: M<A>, f: A -> B):M<B>
+  function method Map<A,B>(xs: M<A>, f: A -> B):M<B>
     reads f.reads;
 	requires forall a :: f.requires(a);
   {
@@ -170,7 +170,7 @@ module List refines Monad {
     ensures Concat(Concat(xs,ys),zs) == Concat(xs,Concat(ys,zs));
   {}
 
-  lemma BindMorphism(xs : M<A>, ys: M<A>, f : A -> M<B>)
+  lemma BindMorphism<A,B>(xs : M<A>, ys: M<A>, f : A -> M<B>)
     requires forall a :: f.requires(a);
 	ensures Bind(Concat(xs,ys),f) == Concat(Bind(xs,f),Bind(ys,f));
   {
diff --git a/Test/hofs/Naked.dfy b/Test/hofs/Naked.dfy
index fa99377f..d23eb507 100644
--- a/Test/hofs/Naked.dfy
+++ b/Test/hofs/Naked.dfy
@@ -19,17 +19,17 @@ module Functions {
 
 module Requires {
   function t(x: nat): nat
-  requires !t.requires(x);
+  requires !t.requires(x);  // error: use of naked function in its own SCC
   { x }
 
   function g(x: nat): nat
-  requires !(g).requires(x);
+  requires !(g).requires(x);  // error: use of naked function in its own SCC
   { x }
 
-  function g2(x: int): int { h(x) }
-
+  function D(x: int): int  // used so termination errors don't mask other errors
+  function g2(x: int): int decreases D(x) { h(x) }  // error: precondition violation
   function h(x: int): int
-    requires !g2.requires(x);
+    requires !g2.requires(x);  // error: use of naked function in its own SCC
   { x }
 }
 
diff --git a/Test/hofs/Naked.dfy.expect b/Test/hofs/Naked.dfy.expect
index b4dfc561..514952a1 100644
--- a/Test/hofs/Naked.dfy.expect
+++ b/Test/hofs/Naked.dfy.expect
@@ -21,11 +21,7 @@ Execution trace:
 Naked.dfy(26,14): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
 Execution trace:
     (0,0): anon0
-Naked.dfy(29,30): Error: cannot prove termination; try supplying a decreases clause
-Execution trace:
-    (0,0): anon0
-    (0,0): anon4_Else
-Naked.dfy(29,30): Error: possible violation of function precondition
+Naked.dfy(30,45): Error: possible violation of function precondition
 Naked.dfy(32,14): Related location
 Execution trace:
     (0,0): anon0
@@ -47,4 +43,4 @@ Naked.dfy(48,11): Error: cannot use naked function in recursive setting. Possibl
 Execution trace:
     (0,0): anon0
 
-Dafny program verifier finished with 1 verified, 12 errors
+Dafny program verifier finished with 2 verified, 11 errors
diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy
index e11473bd..a6f8d922 100644
--- a/Test/hofs/ReadsReads.dfy
+++ b/Test/hofs/ReadsReads.dfy
@@ -2,58 +2,58 @@
 // RUN: %diff "%s.expect" "%t"
 
 module ReadsRequiresReads {
-  function MyReadsOk(f : A -> B, a : A) : set<object>
-    reads f.reads(a);
+  function MyReadsOk<A,B>(f : A -> B, a : A) : set<object>
+    reads f.reads(a)
   {
     f.reads(a)
   }
 
-  function MyReadsOk2(f : A -> B, a : A) : set<object>
-    reads f.reads(a);
+  function MyReadsOk2<A,B>(f : A -> B, a : A) : set<object>
+    reads f.reads(a)
   {
     (f.reads)(a)
   }
 
-  function MyReadsOk3(f : A -> B, a : A) : set<object>
-    reads (f.reads)(a);
+  function MyReadsOk3<A,B>(f : A -> B, a : A) : set<object>
+    reads (f.reads)(a)
   {
     f.reads(a)
   }
 
-  function MyReadsOk4(f : A -> B, a : A) : set<object>
-    reads (f.reads)(a);
+  function MyReadsOk4<A,B>(f : A -> B, a : A) : set<object>
+    reads (f.reads)(a)
   {
     (f.reads)(a)
   }
 
-  function MyReadsBad(f : A -> B, a : A) : set<object>
+  function MyReadsBad<A,B>(f : A -> B, a : A) : set<object>
   {
     f.reads(a)  // error: MyReadsBad does not have permission to read what f.reads(a) reads
   }
 
-  function MyReadsBad2(f : A -> B, a : A) : set<object>
+  function MyReadsBad2<A,B>(f : A -> B, a : A) : set<object>
   {
     (f.reads)(a)  // error: MyReadsBad2 does not have permission to read what f.reads(a) reads
   }
 
-  function MyReadsOk'(f : A -> B, a : A, o : object) : bool
-    reads f.reads(a);
+  function MyReadsOk'<A,B>(f : A -> B, a : A, o : object) : bool
+    reads f.reads(a)
   {
     o in f.reads(a)
   }
 
-  function MyReadsBad'(f : A -> B, a : A, o : object) : bool
+  function MyReadsBad'<A,B>(f : A -> B, a : A, o : object) : bool
   {
     o in f.reads(a)  // error: MyReadsBad' does not have permission to read what f.reads(a) reads
   }
 
-  function MyRequiresOk(f : A -> B, a : A) : bool
-    reads f.reads(a);
+  function MyRequiresOk<A,B>(f : A -> B, a : A) : bool
+    reads f.reads(a)
   {
     f.requires(a)
   }
 
-  function MyRequiresBad(f : A -> B, a : A) : bool
+  function MyRequiresBad<A,B>(f : A -> B, a : A) : bool
   {
     f.requires(a)  // error: MyRequiresBad does not have permission to read what f.requires(a) reads
   }
@@ -72,11 +72,11 @@ module WhatWeKnowAboutReads {
   }
 
   class S {
-    var s : S;
+    var s : S
   }
 
   function ReadsSomething(s : S):()
-    reads s;
+    reads s
   {()}
 
   method MaybeSomething() {
@@ -105,29 +105,29 @@ module WhatWeKnowAboutReads {
 
 module ReadsAll {
   function A(f: int -> int) : int
-    reads set o,x | o in f.reads(x) :: o;
-    requires forall x :: f.requires(x);
+    reads set o,x | o in f.reads(x) :: o
+    requires forall x :: f.requires(x)
   {
     f(0) + f(1) + f(2)
   }
 
   function method B(f: int -> int) : int
-    reads set o,x | o in f.reads(x) :: o;
-    requires forall x :: f.requires(x);
+    reads set o,x | o in f.reads(x) :: o
+    requires forall x :: f.requires(x)
   {
     f(0) + f(1) + f(2)
   }
 
   function C(f: int -> int) : int
-    reads f.reads;
-    requires forall x :: f.requires(x);
+    reads f.reads
+    requires forall x :: f.requires(x)
   {
     f(0) + f(1) + f(2)
   }
 
   function method D(f: int -> int) : int
-    reads f.reads;
-    requires forall x :: f.requires(x);
+    reads f.reads
+    requires forall x :: f.requires(x)
   {
     f(0) + f(1) + f(2)
   }
diff --git a/Test/hofs/Requires.dfy b/Test/hofs/Requires.dfy
new file mode 100644
index 00000000..68677b3e
--- /dev/null
+++ b/Test/hofs/Requires.dfy
@@ -0,0 +1,82 @@
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main()
+{
+  test0(10);
+	test5(11);
+	test6(12);
+	test1();
+	test2();
+}
+
+predicate valid(x:int) 
+{
+  x > 0
+}
+
+function ref1(y:int) : int
+  requires valid(y);
+{
+  y - 1
+}
+
+lemma assumption1()
+  ensures forall a, b :: valid(a) && valid(b) && ref1(a) == ref1(b) ==> a == b;
+{
+} 
+
+method test0(a: int)
+{
+  if ref1.requires(a) {
+    // the precondition should suffice to let us call the method
+    ghost var b := ref1(a);
+  }
+}
+method test5(a: int)
+{
+  if valid(a) {
+    // valid(a) is the precondition of ref1
+    assert ref1.requires(a);
+  }  
+} 
+method test6(a: int)
+{
+  if ref1.requires(a) {
+    // the precondition of ref1 is valid(a)
+    assert valid(a);
+  }  
+}
+
+method test1()
+{
+  if * {
+    assert forall a, b :: valid(a) && valid(b) && ref1(a) == ref1(b) ==> a == b;
+  } else {
+    assert forall a, b :: ref1.requires(a) && ref1.requires(b) && ref1(a) == ref1(b) 
+                          ==> a == b;
+  }
+}
+
+function {:opaque} ref2(y:int) : int        // Now with an opaque attribute
+  requires valid(y);
+{
+  y - 1
+}
+
+lemma assumption2()
+  ensures forall a, b :: valid(a) && valid(b) && ref2(a) == ref2(b) ==> a == b;
+{
+  reveal_ref2();
+}
+
+method test2()
+{
+  assumption2();
+  if * {
+    assert forall a, b :: valid(a) && valid(b) && ref2(a) == ref2(b) ==> a == b;
+  } else {
+    assert forall a, b :: ref2.requires(a) && ref2.requires(b) && ref2(a) == ref2(b) 
+                          ==> a == b;
+  }
+}
diff --git a/Test/hofs/Requires.dfy.expect b/Test/hofs/Requires.dfy.expect
new file mode 100644
index 00000000..b9a40d66
--- /dev/null
+++ b/Test/hofs/Requires.dfy.expect
@@ -0,0 +1,5 @@
+
+Dafny program verifier finished with 20 verified, 0 errors
+Program compiled successfully
+Running...
+
diff --git a/Test/hofs/ResolveError.dfy b/Test/hofs/ResolveError.dfy
index 3c0d7cd9..ae838eb3 100644
--- a/Test/hofs/ResolveError.dfy
+++ b/Test/hofs/ResolveError.dfy
@@ -3,9 +3,9 @@
 
 
 method ResolutionErrors() {
-    var x;
-    var g5 := x, y => (y, x);   // fail at resolution
-    var g6 := x, (y => (y, x)); // fail at resolution
+  var x;
+  var g5 := x, y => (y, x);   // fail at resolution
+  var g6 := x, (y => (y, x)); // fail at resolution
 }
 
 // cannot assign functions
@@ -23,20 +23,20 @@ method Nope3() {
 
 method RequiresFail(f : int -> int)
   // ok
-  requires f(0) == 0;
-  requires f.requires(0);
-  requires f.reads(0) == {};
+  requires f(0) == 0
+  requires f.requires(0)
+  requires f.reads(0) == {}
 
   // fail
-  requires f(0) == true;
-  requires f(1,2) == 0;
-  requires f(true) == 0;
-  requires f.requires(true);
-  requires f.requires(1) == 0;
-  requires f.requires(1,2);
-  requires f.reads(true) == {};
-  requires f.reads(1) == 0;
-  requires f.reads(1,2) == {};
+  requires f(0) == true
+  requires f(1,2) == 0
+  requires f(true) == 0
+  requires f.requires(true)
+  requires f.requires(1) == 0
+  requires f.requires(1,2)
+  requires f.reads(true) == {}
+  requires f.reads(1) == 0
+  requires f.reads(1,2) == {}
 {
 }
 
@@ -56,7 +56,7 @@ method Bla() {
   assert Bool;
 }
 
-method Pli(f : A -> B) requires f != null;
+method Pli<A,B>(f : A -> B) requires f != null
 {
   var o : object;
   assert f != o;
@@ -102,7 +102,7 @@ module AritySituations {
     w := V;  // error
   }
 
-  method P(r: T -> U, x: T) returns (u: U)
+  method P<T,U>(r: T -> U, x: T) returns (u: U)
     requires r.requires(x);
   {
     u := r(x);
diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect
index c3e0c242..11471ffd 100644
--- a/Test/hofs/ResolveError.dfy.expect
+++ b/Test/hofs/ResolveError.dfy.expect
@@ -2,8 +2,8 @@ ResolveError.dfy(86,6): Error: RHS (of type ((int,bool)) -> real) not assignable
 ResolveError.dfy(91,15): Error: incorrect type of method in-parameter 0 (expected ? -> ?, got (int,bool) -> real)
 ResolveError.dfy(101,6): Error: RHS (of type (()) -> real) not assignable to LHS (of type () -> real)
 ResolveError.dfy(102,6): Error: RHS (of type () -> real) not assignable to LHS (of type (()) -> real)
-ResolveError.dfy(7,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment
-ResolveError.dfy(8,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment
+ResolveError.dfy(7,9): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment
+ResolveError.dfy(8,9): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment
 ResolveError.dfy(21,6): Error: LHS of assignment must denote a mutable field
 ResolveError.dfy(31,16): Error: arguments must have the same type (got int and bool)
 ResolveError.dfy(32,12): Error: wrong number of arguments to function application (function type 'int -> int' expects 1, got 2)
@@ -17,7 +17,7 @@ ResolveError.dfy(39,18): Error: wrong number of arguments to function applicatio
 ResolveError.dfy(46,15): Error: a reads-clause expression must denote an object or a collection of objects (instead got int)
 ResolveError.dfy(47,7): Error: Precondition must be boolean (got int)
 ResolveError.dfy(56,9): Error: condition is expected to be of type bool, but is () -> bool
-ResolveError.dfy(59,34): Error: arguments must have the same type (got A -> B and ?)
+ResolveError.dfy(59,39): Error: arguments must have the same type (got A -> B and ?)
 ResolveError.dfy(62,11): Error: arguments must have the same type (got A -> B and object)
 ResolveError.dfy(68,24): Error: unresolved identifier: _
 22 resolution/type errors detected in ResolveError.dfy
diff --git a/Test/hofs/Simple.dfy b/Test/hofs/Simple.dfy
index c27fa82c..6d98531e 100644
--- a/Test/hofs/Simple.dfy
+++ b/Test/hofs/Simple.dfy
@@ -50,7 +50,7 @@ method Main() {
 }
 
 function method succ(x : int) : int
-  requires x > 0;
+  requires x > 0
 {
   x + 1
 }
@@ -74,24 +74,24 @@ method Main3() {
 }
 
 
-function P(f: A -> B, x : A): B
-  reads (f.reads)(x);
-  requires (f.requires)(x);
+function P<A,B>(f: A -> B, x : A): B
+  reads (f.reads)(x)
+  requires (f.requires)(x)
 {
   f(x)
 }
 
 
-function Q(f: U -> V, x : U): V
-  reads P.reads(f,x);
-  requires f.requires(x);  // would be nice to be able to write P.requires(f,x)
+function Q<U,V>(f: U -> V, x : U): V
+  reads P.reads(f,x)
+  requires f.requires(x)  // would be nice to be able to write P.requires(f,x)
 {
   P(f,x)
 }
 
-function QQ(f: U -> V, x : U): V
-  reads ((() => ((()=>f)()).reads)())((()=>x)());
-  requires ((() => ((()=>f)()).requires)())((()=>x)());
+function QQ<U,V>(f: U -> V, x : U): V
+  reads ((() => ((()=>f)()).reads)())((()=>x)())
+  requires ((() => ((()=>f)()).requires)())((()=>x)())
 {
   ((() => P)())((()=>f)(),(()=>x)())
 }
diff --git a/Test/hofs/Simple.dfy.expect b/Test/hofs/Simple.dfy.expect
index 1a1027ae..e2f16ef3 100644
--- a/Test/hofs/Simple.dfy.expect
+++ b/Test/hofs/Simple.dfy.expect
@@ -20,13 +20,10 @@ Execution trace:
 Simple.dfy(61,10): Error: possible violation of function precondition
 Execution trace:
     (0,0): anon0
-Simple.dfy(61,18): Error: assertion violation
-Execution trace:
-    (0,0): anon0
 Simple.dfy(73,10): Error: assertion violation
 Execution trace:
     (0,0): anon0
     Simple.dfy(72,38): anon5_Else
     Simple.dfy(73,38): anon6_Else
 
-Dafny program verifier finished with 14 verified, 7 errors
+Dafny program verifier finished with 14 verified, 6 errors
diff --git a/Test/hofs/TreeMapSimple.dfy b/Test/hofs/TreeMapSimple.dfy
index a853b82c..6b8f1377 100644
--- a/Test/hofs/TreeMapSimple.dfy
+++ b/Test/hofs/TreeMapSimple.dfy
@@ -6,7 +6,7 @@ datatype List<A> = Nil | Cons(head: A,tail: List<A>)
 datatype Tree<A> = Branch(val: A,trees: List<Tree<A>>)
 
 function ListData(xs : List) : set
-  ensures forall x :: x in ListData(xs) ==> x < xs;
+  ensures forall x :: x in ListData(xs) ==> x < xs
 {
   match xs
     case Nil => {}
@@ -14,32 +14,32 @@ function ListData(xs : List) : set
 }
 
 function TreeData(t0 : Tree) : set
-  ensures forall t :: t in TreeData(t0) ==> t < t0;
+  ensures forall t :: t in TreeData(t0) ==> t < t0
 {
   var Branch(x,ts) := t0;
   {x} + set t, y | t in ListData(ts) && y in TreeData(t) :: y
 }
 
-function Pre(f : A -> B, s : set<A>) : bool
-  reads (set x, y | x in s && y in f.reads(x) :: y);
+function Pre<A,B>(f : A -> B, s : set<A>) : bool
+  reads (set x, y | x in s && y in f.reads(x) :: y)
 {
   forall x :: x in s ==> f.reads(x) == {} && f.requires(x)
 }
 
-function method Map(xs : List<A>, f : A -> B): List<B>
-  reads Pre.reads(f, ListData(xs));
-  requires Pre(f, ListData(xs));
-  decreases xs;
+function method Map<A,B>(xs : List<A>, f : A -> B): List<B>
+  reads Pre.reads(f, ListData(xs))
+  requires Pre(f, ListData(xs))
+  decreases xs
 {
   match xs
     case Nil => Nil
     case Cons(x,xs) => Cons(f(x),Map(xs,f))
 }
 
-function method TMap(t0 : Tree<A>, f : A -> B) : Tree<B>
-  reads Pre.reads(f, TreeData(t0));
-  requires Pre(f, TreeData(t0));
-  decreases t0;
+function method TMap<A,B>(t0 : Tree<A>, f : A -> B) : Tree<B>
+  reads Pre.reads(f, TreeData(t0))
+  requires Pre(f, TreeData(t0))
+  decreases t0
 {
   var Branch(x,ts) := t0;
   Branch(f(x),Map(ts, t  requires t in ListData(ts)
diff --git a/Test/hofs/Twice.dfy b/Test/hofs/Twice.dfy
index add7e83c..5d948a58 100644
--- a/Test/hofs/Twice.dfy
+++ b/Test/hofs/Twice.dfy
@@ -1,7 +1,7 @@
 // RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-function method Twice(f : A -> A): A -> A
+function method Twice<A>(f : A -> A): A -> A
 {
   x requires f.requires(x) && f.requires(f(x))
     reads f.reads(x) reads if f.requires(x) then f.reads(f(x)) else {}
@@ -29,7 +29,7 @@ method WithReads() {
 }
 
 
-function method Twice_bad(f : A -> A): A -> A
+function method Twice_bad<A>(f : A -> A): A -> A
 {
   x requires f.requires(x) && f.requires(f(x))
     reads f.reads(x) + f.reads(f(x))
diff --git a/Test/hofs/VectorUpdate.dfy b/Test/hofs/VectorUpdate.dfy
index 96edbe77..ca6b20b3 100644
--- a/Test/hofs/VectorUpdate.dfy
+++ b/Test/hofs/VectorUpdate.dfy
@@ -1,28 +1,59 @@
 // RUN: %dafny /compile:3 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-method VectorUpdate(N: int, a : array<A>, f : (int,A) -> A)
-  requires a != null;
-  requires N == a.Length;
-  requires forall j :: 0 <= j < N ==> f.requires(j,a[j]);
-  requires forall j :: 0 <= j < N ==> a !in f.reads(j,a[j]);
-  modifies a;
-  ensures forall j :: 0 <= j < N ==> a[j] == f(j,old(a[j]));
+// this is a rather verbose version of the VectorUpdate method
+method VectorUpdate<A>(N: int, a : array<A>, f : (int,A) -> A)
+  requires a != null
+  requires N == a.Length
+  requires forall j :: 0 <= j < N ==> f.requires(j,a[j])
+  requires forall j :: 0 <= j < N ==> a !in f.reads(j,a[j])
+  modifies a
+  ensures forall j :: 0 <= j < N ==> a[j] == f(j,old(a[j]))
 {
   var i := 0;
-  while (i < N)
-    invariant 0 <= i <= N;
-    invariant forall j :: i <= j < N ==> f.requires(j,a[j]);
-    invariant forall j :: 0 <= j < N ==> f.requires(j,old(a[j]));
-    invariant forall j :: i <= j < N ==> a !in f.reads(j,a[j]);
-    invariant forall j :: i <= j < N ==> a[j] == old(a[j]);
-    invariant forall j :: 0 <= j < i ==> a[j] == f(j,old(a[j]));
+  while i < N
+    invariant 0 <= i <= N
+    invariant forall j :: i <= j < N ==> f.requires(j,a[j])
+    invariant forall j :: 0 <= j < N ==> f.requires(j,old(a[j]))
+    invariant forall j :: i <= j < N ==> a !in f.reads(j,a[j])
+    invariant forall j :: i <= j < N ==> a[j] == old(a[j])
+    invariant forall j :: 0 <= j < i ==> a[j] == f(j,old(a[j]))
   {
     a[i] := f(i,a[i]);
     i := i + 1;
   }
 }
 
+// here's a shorter version of the method above
+method VectorUpdate'<A>(a : array<A>, f : (int,A) -> A)
+  requires a != null
+  requires forall j :: 0 <= j < a.Length ==> a !in f.reads(j,a[j]) && f.requires(j,a[j])
+  modifies a
+  ensures forall j :: 0 <= j < a.Length ==> a[j] == f(j,old(a[j]))
+{
+  var i := 0;
+  while i < a.Length
+    invariant 0 <= i <= a.Length
+    invariant forall j :: i <= j < a.Length ==> a[j] == old(a[j])
+    invariant forall j :: 0 <= j < i ==> a[j] == f(j,old(a[j]))
+  {
+    a[i] := f(i,a[i]);
+    i := i + 1;
+  }
+}
+
+// here's yet another version
+method VectorUpdate''<A>(a : array<A>, f : (int,A) -> A)
+  requires a != null
+  requires forall j :: 0 <= j < a.Length ==> a !in f.reads(j,a[j]) && f.requires(j,a[j])
+  modifies a
+  ensures forall j :: 0 <= j < a.Length ==> a[j] == f(j,old(a[j]))
+{
+  forall i | 0 <= i < a.Length {
+    a[i] := f(i,a[i]);
+  }
+}
+
 method Main() 
 {
   var v := new int[10];
@@ -46,11 +77,11 @@ method Main()
 }
 
 method PrintArray(a : array<int>)
-  requires a != null;
+  requires a != null
 {
   var i := 0;
-  while (i < a.Length) {
-    if (i != 0) {
+  while i < a.Length {
+    if i != 0 {
 	  print ", ";
 	}
     print a[i];
diff --git a/Test/hofs/VectorUpdate.dfy.expect b/Test/hofs/VectorUpdate.dfy.expect
index b01ace00..18a7b110 100644
--- a/Test/hofs/VectorUpdate.dfy.expect
+++ b/Test/hofs/VectorUpdate.dfy.expect
@@ -1,5 +1,5 @@
 
-Dafny program verifier finished with 6 verified, 0 errors
+Dafny program verifier finished with 10 verified, 0 errors
 Program compiled successfully
 Running...
 
diff --git a/Test/irondafny0/FIFO.dfy b/Test/irondafny0/FIFO.dfy
new file mode 100644
index 00000000..ded8f567
--- /dev/null
+++ b/Test/irondafny0/FIFO.dfy
@@ -0,0 +1,43 @@
+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+include "Queue.dfyi"
+
+module FIFO exclusively refines Queue {
+    type Item = int
+
+    method Init() returns (q: Queue) {
+        q := [];
+    }
+
+    method Push(item: Item, q: Queue) returns (q': Queue) {
+        return q + [item];
+    }
+
+    method Pop(q: Queue) returns (item: Item, q': Queue)
+        ensures item == q[0]
+    {
+        item := q[0];
+        q' := q[1..];
+    }
+}
+
+module MainImpl refines MainSpec {
+    import Q = FIFO
+
+    method Main()
+    {
+        var q := Q.Init();
+        q := Q.Push(0, q);
+        q := Q.Push(1, q);
+        q := Q.Push(2, q);
+
+        var n: int;
+        n, q := Q.Pop(q);
+        print n, "\n";
+        n, q := Q.Pop(q);
+        print n, "\n";
+        n, q := Q.Pop(q);
+        print n, "\n";
+    }
+}
diff --git a/Test/irondafny0/FIFO.dfy.expect b/Test/irondafny0/FIFO.dfy.expect
new file mode 100644
index 00000000..25021947
--- /dev/null
+++ b/Test/irondafny0/FIFO.dfy.expect
@@ -0,0 +1,8 @@
+
+Dafny program verifier finished with 8 verified, 0 errors
+Program compiled successfully
+Running...
+
+0
+1
+2
diff --git a/Test/irondafny0/LIFO.dfy b/Test/irondafny0/LIFO.dfy
new file mode 100644
index 00000000..8c0a08e8
--- /dev/null
+++ b/Test/irondafny0/LIFO.dfy
@@ -0,0 +1,43 @@
+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+include "Queue.dfyi"
+
+module LIFO exclusively refines Queue {
+    type Item = int
+
+    method Init() returns (q: Queue) {
+        q := [];
+    }
+
+    method Push(item: Item, q: Queue) returns (q': Queue) {
+        return [item] + q;
+    }
+
+    method Pop(q: Queue) returns (item: Item, q': Queue)
+        ensures item == q[0]
+    {
+        item := q[0];
+        q' := q[1..];
+    }
+}
+
+module MainImpl refines MainSpec {
+    import Q = LIFO
+
+    method Main()
+    {
+        var q := Q.Init();
+        q := Q.Push(0, q);
+        q := Q.Push(1, q);
+        q := Q.Push(2, q);
+
+        var n: int;
+        n, q := Q.Pop(q);
+        print n, "\n";
+        n, q := Q.Pop(q);
+        print n, "\n";
+        n, q := Q.Pop(q);
+        print n, "\n";
+    }
+}
diff --git a/Test/irondafny0/LIFO.dfy.expect b/Test/irondafny0/LIFO.dfy.expect
new file mode 100644
index 00000000..83f90a5b
--- /dev/null
+++ b/Test/irondafny0/LIFO.dfy.expect
@@ -0,0 +1,8 @@
+
+Dafny program verifier finished with 8 verified, 0 errors
+Program compiled successfully
+Running...
+
+2
+1
+0
diff --git a/Test/irondafny0/Queue.dfyi b/Test/irondafny0/Queue.dfyi
new file mode 100644
index 00000000..9f7eb534
--- /dev/null
+++ b/Test/irondafny0/Queue.dfyi
@@ -0,0 +1,22 @@
+// Queue.dfyi
+
+abstract module Queue {
+    type Item
+    type Queue = seq<Item>
+
+    method Init() returns (q: Queue)
+        ensures |q| == 0;
+
+    method Push(item: Item, q: Queue) returns (q': Queue)
+        ensures |q'| == |q| + 1;
+
+    method Pop(q: Queue) returns (item: Item, q': Queue)
+        requires |q| > 0;
+        ensures item in q;
+        ensures |q'| == |q| - 1;
+}
+
+abstract module MainSpec {
+    import Q as Queue
+}
+
diff --git a/Test/irondafny0/inheritreqs0.dfy b/Test/irondafny0/inheritreqs0.dfy
new file mode 100644
index 00000000..a0117da0
--- /dev/null
+++ b/Test/irondafny0/inheritreqs0.dfy
@@ -0,0 +1,22 @@
+// RUN: %dafny /compile:3 /optimize /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+abstract module Spec {
+    method Greet(b: bool)
+        requires b;
+}
+
+module Impl refines Spec {
+    method Greet(b: bool) {
+        print "o hai!\n";
+    }
+
+    method Xyzzy(b: bool)
+        requires b;
+    {}
+
+    method Main() {
+        Greet(false);
+        Xyzzy(false);
+    }
+}
diff --git a/Test/irondafny0/inheritreqs0.dfy.expect b/Test/irondafny0/inheritreqs0.dfy.expect
new file mode 100644
index 00000000..eaadc85a
--- /dev/null
+++ b/Test/irondafny0/inheritreqs0.dfy.expect
@@ -0,0 +1,6 @@
+inheritreqs0.dfy(19,14): Error BP5002: A precondition for this call might not hold.
+inheritreqs0.dfy[Impl](6,18): Related location: This is the precondition that might not hold.
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 6 verified, 1 error
diff --git a/Test/irondafny0/inheritreqs1.dfy b/Test/irondafny0/inheritreqs1.dfy
new file mode 100644
index 00000000..c83d04ac
--- /dev/null
+++ b/Test/irondafny0/inheritreqs1.dfy
@@ -0,0 +1,22 @@
+// RUN: %dafny /compile:3 /optimize /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+abstract module Spec {
+    method Greet(b: bool)
+        requires b;
+}
+
+module Impl refines Spec {
+    method Greet(b: bool) {
+        print "o hai!\n";
+    }
+
+    method Xyzzy(b: bool)
+        requires b;
+    {}
+
+    method Main() {
+        Greet(true);
+        Xyzzy(false);
+    }
+}
diff --git a/Test/irondafny0/inheritreqs1.dfy.expect b/Test/irondafny0/inheritreqs1.dfy.expect
new file mode 100644
index 00000000..27c76fee
--- /dev/null
+++ b/Test/irondafny0/inheritreqs1.dfy.expect
@@ -0,0 +1,6 @@
+inheritreqs1.dfy(20,14): Error BP5002: A precondition for this call might not hold.
+inheritreqs1.dfy(15,18): Related location: This is the precondition that might not hold.
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 6 verified, 1 error
diff --git a/Test/irondafny0/opened_workaround.dfy b/Test/irondafny0/opened_workaround.dfy
new file mode 100644
index 00000000..7464c346
--- /dev/null
+++ b/Test/irondafny0/opened_workaround.dfy
@@ -0,0 +1,21 @@
+// RUN: %dafny /ironDafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module A {
+
+    predicate P() 
+
+    class C
+    {
+        static method{:axiom} M()
+            ensures P();
+    } 
+}
+
+abstract module B {
+    import opened A
+}
+
+abstract module C {
+    import Bee as B       // Works
+}
diff --git a/Test/irondafny0/opened_workaround.dfy.expect b/Test/irondafny0/opened_workaround.dfy.expect
new file mode 100644
index 00000000..0be94b4c
--- /dev/null
+++ b/Test/irondafny0/opened_workaround.dfy.expect
@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 3 verified, 0 errors
+Compilation error: Function _0_A_Compile._default.P has no body
diff --git a/Test/irondafny0/xrefine0.dfy b/Test/irondafny0/xrefine0.dfy
new file mode 100644
index 00000000..b849111c
--- /dev/null
+++ b/Test/irondafny0/xrefine0.dfy
@@ -0,0 +1,6 @@
+// RUN: %dafny /ironDafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+abstract module Delicious {}
+module Chocolate exclusively refines Delicious {}
+module Strawberry exclusively refines Delicious {}
diff --git a/Test/irondafny0/xrefine0.dfy.expect b/Test/irondafny0/xrefine0.dfy.expect
new file mode 100644
index 00000000..136e06db
--- /dev/null
+++ b/Test/irondafny0/xrefine0.dfy.expect
@@ -0,0 +1,2 @@
+xrefine0.dfy(6,7): Error: no more than one exclusive refinement may exist for a given module.
+1 resolution/type errors detected in xrefine0.dfy
diff --git a/Test/irondafny0/xrefine1.dfy b/Test/irondafny0/xrefine1.dfy
new file mode 100644
index 00000000..4b085e6b
--- /dev/null
+++ b/Test/irondafny0/xrefine1.dfy
@@ -0,0 +1,77 @@
+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+abstract module ProtocolSpec {
+    type ProtoT
+
+    predicate Init(p:ProtoT)
+}
+
+abstract module HostSpec {
+    type HostT
+    import P as ProtocolSpec
+
+    function method foo(h:HostT) : P.ProtoT
+}
+
+module ProtocolImpl exclusively refines ProtocolSpec {
+    type ProtoT = bool    
+
+    predicate Init(p:ProtoT) { !p }
+
+    method orange(i:nat) returns (j:nat)
+    {
+        j := i + 1;
+    }
+}
+
+module HostImpl exclusively refines HostSpec {
+    import P = ProtocolImpl
+
+    type HostT = int
+
+    function method foo(h:HostT) : P.ProtoT
+    {
+        h > 0
+    }
+
+    method apple(i:nat) returns (j:nat)
+    {
+        j := i + 1;
+    }
+}
+
+abstract module MainSpec {
+    import HI as HostSpec
+    import PI as ProtocolSpec
+
+    method Test(h1:HI.HostT, h2:HI.HostT) 
+        requires HI.foo(h1) == HI.foo(h2);
+        requires PI.Init(HI.foo(h1))
+}
+
+module MainImpl exclusively refines MainSpec {
+    import HI = HostImpl
+    import PI = ProtocolImpl
+    
+    method Test(h1:HI.HostT, h2:HI.HostT) 
+    {
+        var a := HI.foo(h1);
+        print "HI.foo(h1) => ", a, "\n";
+        var b := HI.foo(h2);
+        print "HI.foo(h2) => ", b, "\n";
+        var i := PI.orange(1);
+        print "PI.orange(1) => ", i, "\n";
+        var j := HI.apple(2);
+        print "PI.apple(2) => ", j, "\n";
+    }
+
+    method Main()
+    {
+        Test(-1, 1);
+    }
+}
+
+
+
+
diff --git a/Test/irondafny0/xrefine1.dfy.expect b/Test/irondafny0/xrefine1.dfy.expect
new file mode 100644
index 00000000..ae844fc8
--- /dev/null
+++ b/Test/irondafny0/xrefine1.dfy.expect
@@ -0,0 +1,6 @@
+xrefine1.dfy(71,13): Error BP5002: A precondition for this call might not hold.
+xrefine1.dfy[MainImpl](49,29): Related location: This is the precondition that might not hold.
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 12 verified, 1 error
diff --git a/Test/irondafny0/xrefine2.dfy b/Test/irondafny0/xrefine2.dfy
new file mode 100644
index 00000000..1de4e201
--- /dev/null
+++ b/Test/irondafny0/xrefine2.dfy
@@ -0,0 +1,77 @@
+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+abstract module ProtocolSpec {
+    type ProtoT
+
+    predicate Init(p:ProtoT)
+}
+
+abstract module HostSpec {
+    type HostT
+    import P as ProtocolSpec
+
+    function method foo(h:HostT) : P.ProtoT
+}
+
+module ProtocolImpl exclusively refines ProtocolSpec {
+    type ProtoT = bool    
+
+    predicate Init(p:ProtoT) { p }
+
+    method orange(i:nat) returns (j:nat)
+    {
+        j := i + 1;
+    }
+}
+
+module HostImpl exclusively refines HostSpec {
+    import P = ProtocolImpl
+
+    type HostT = int
+
+    function method foo(h:HostT) : P.ProtoT
+    {
+        h != 0
+    }
+
+    method apple(i:nat) returns (j:nat)
+    {
+        j := i + 1;
+    }
+}
+
+abstract module MainSpec {
+    import HI as HostSpec
+    import PI as ProtocolSpec
+
+    method Test(h1:HI.HostT, h2:HI.HostT) 
+        requires HI.foo(h1) == HI.foo(h2);
+        requires PI.Init(HI.foo(h1))
+}
+
+module MainImpl exclusively refines MainSpec {
+    import HI = HostImpl
+    import PI = ProtocolImpl
+    
+    method Test(h1:HI.HostT, h2:HI.HostT) 
+    {
+        var a := HI.foo(h1);
+        print "HI.foo(h1) => ", a, "\n";
+        var b := HI.foo(h2);
+        print "HI.foo(h2) => ", b, "\n";
+        var i := PI.orange(1);
+        print "PI.orange(1) => ", i, "\n";
+        var j := HI.apple(2);
+        print "PI.apple(2) => ", j, "\n";
+    }
+
+    method Main()
+    {
+        Test(-1, 1);
+    }
+}
+
+
+
+
diff --git a/Test/irondafny0/xrefine2.dfy.expect b/Test/irondafny0/xrefine2.dfy.expect
new file mode 100644
index 00000000..6d3fecd4
--- /dev/null
+++ b/Test/irondafny0/xrefine2.dfy.expect
@@ -0,0 +1,9 @@
+
+Dafny program verifier finished with 13 verified, 0 errors
+Program compiled successfully
+Running...
+
+HI.foo(h1) => True
+HI.foo(h2) => True
+PI.orange(1) => 2
+PI.apple(2) => 3
diff --git a/Test/irondafny0/xrefine3.dfy b/Test/irondafny0/xrefine3.dfy
new file mode 100644
index 00000000..44add7cc
--- /dev/null
+++ b/Test/irondafny0/xrefine3.dfy
@@ -0,0 +1,72 @@
+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+abstract module AlphaSpec {
+    type Alpha
+
+    predicate IsValid(a:Alpha)
+
+    method Init() returns (a:Alpha)
+        ensures IsValid(a);
+}
+
+abstract module BetaSpec {
+    type Beta
+    import A as AlphaSpec
+
+    predicate IsValid(b:Beta)
+
+    method Init(ays:seq<A.Alpha>) returns (b:Beta)
+        requires forall i :: 0 <= i < |ays| ==> A.IsValid(ays[i]);
+        ensures IsValid(b);
+}
+
+module AlphaImpl exclusively refines AlphaSpec {
+    type Alpha = bool    
+
+    predicate IsValid(a:Alpha) { 
+        a 
+    }
+
+    method Init() returns (a:Alpha)
+        ensures IsValid(a);
+    {
+        a := true;
+    }
+}
+
+module BetaImpl exclusively refines BetaSpec {
+    import A = AlphaImpl
+    type Beta = seq<A.Alpha>
+
+    predicate IsValid(b:Beta) {
+        forall i :: 0 <= i < |b| ==> A.IsValid(b[i])
+    }
+
+    method Init(ays:seq<A.Alpha>) returns (b:Beta) {
+        b := ays;
+    }
+}
+
+abstract module MainSpec {
+    import A as AlphaSpec
+    import B as BetaSpec
+
+    method Main()
+    {
+        var a := A.Init();
+        var ays := [a, a];
+        assert forall i :: 0 <= i < |ays| ==> A.IsValid(ays[i]);
+        var b := B.Init(ays);
+        print "o hai!\n";
+    }
+}
+
+module MainImpl exclusively refines MainSpec {
+    import B = BetaImpl
+    import A = AlphaImpl
+}
+
+
+
+
diff --git a/Test/irondafny0/xrefine3.dfy.expect b/Test/irondafny0/xrefine3.dfy.expect
new file mode 100644
index 00000000..1e5a5b4e
--- /dev/null
+++ b/Test/irondafny0/xrefine3.dfy.expect
@@ -0,0 +1,6 @@
+
+Dafny program verifier finished with 14 verified, 0 errors
+Program compiled successfully
+Running...
+
+o hai!
author	Clément Pit--Claudel <clement.pitclaudel@live.com>	2015-07-17 17:25:10 -0700
committer	Clément Pit--Claudel <clement.pitclaudel@live.com>	2015-07-17 17:25:10 -0700
commit	7c766a43a77845ed1af5a0e5367e7a21edf13a8f (patch)
tree	21911b3d9a25d4cc74dca3f831a635929428b993 /Test
parent	fc6ebea9b9ec614e4e014c64d9cad7940deb86fb (diff)
parent	61a5be0930c43694d270809ed5550c74b6e59e5d (diff)