6 files changed, 167 insertions, 33 deletions
diff --git a/Test/dafny0/Trait/TraitBasix.dfy.expect b/Test/dafny0/Trait/TraitBasix.dfy.expect
index 69af0dc5..dbb11c21 100644
--- a/Test/dafny0/Trait/TraitBasix.dfy.expect
+++ b/Test/dafny0/Trait/TraitBasix.dfy.expect
@@ -1,4 +1,4 @@
-TraitBasix.dfy(91,24): Error: Undeclared top-level type or type parameter: IX (did you forget to qualify a name?)
+TraitBasix.dfy(91,24): Error: Undeclared top-level type or type parameter: IX (did you forget to qualify a name or declare a module import 'opened?')
 TraitBasix.dfy(77,8): Error: field 'x' is inherited from trait 'I2' and is not allowed to be re-declared
 TraitBasix.dfy(70,8): Error: class 'I0Child' does not implement trait method 'I2.Customizable'
 TraitBasix.dfy(80,8): Error: class 'I0Child2' does not implement trait function 'I2.F'
diff --git a/Test/dafny0/Trait/TraitExample.dfy b/Test/dafny0/Trait/TraitExample.dfy
index be38bfe5..9474c7ba 100644
--- a/Test/dafny0/Trait/TraitExample.dfy
+++ b/Test/dafny0/Trait/TraitExample.dfy
@@ -4,79 +4,148 @@
 trait Automobile {
   ghost var Repr: set<object>
   predicate Valid()
-    reads this //, Repr
+    reads this, Repr
     ensures Valid() ==> this in Repr
   function method Brand(): string
   var position: int
   method Drive()
     requires Valid()
-    modifies this // Repr
+    modifies Repr
+    ensures Valid() && fresh(Repr - old(Repr))
     ensures old(position) <= position
 }
 
+class Fiat extends Automobile {
+  predicate Valid()
+    reads this, Repr
+    ensures Valid() ==> this in Repr
+  {
+    this in Repr && null !in Repr && position <= 100
+  }
+  constructor (pos: int)
+    requires pos <= 100
+    modifies this
+    ensures Valid() && fresh(Repr - {this}) && position == pos
+  {
+    position, Repr := pos, {this};
+  }
+  function method Brand(): string {
+    "Fiat"
+  }
+  method Drive()
+    requires Valid()
+    modifies Repr
+    ensures Valid() && fresh(Repr - old(Repr))
+    ensures old(position) <= position
+  {
+    position := if position < 97 then position + 3 else 100;
+  }
+}
+
 class Volvo extends Automobile {
+  var odometer: Odometer
   predicate Valid()
-    reads this //, Repr
+    reads this, Repr
     ensures Valid() ==> this in Repr
   {
-    this in Repr
+    this in Repr && null !in Repr && odometer in Repr &&
+    position % 10 == 0 &&  // position is always a multiple of 10
+    odometer.value == position
   }
-  constructor()
+  constructor ()
     modifies this
-    ensures Valid()
+    ensures Valid() && fresh(Repr - {this})
   {
-    Repr := {this};
+    position, Repr := 0, {this};
+    odometer := new Odometer();
+    Repr := Repr + {odometer};
   }
   function method Brand(): string {
     "Volvo"
   }
   method Drive()
-//    requires Valid()
-    modifies this // Repr
-    ensures old(position) <= position
+    requires Valid()
+    modifies Repr
+    ensures Valid() && fresh(Repr - old(Repr))
+    ensures old(position) < position  // always promises to make a move
   {
     position := position + 10;
+    odometer.Advance(10);
   }
 }
 
-class Fiat extends Automobile {
+class Odometer {
+  var value: int
+  constructor ()
+    modifies this
+    ensures value == 0
+  {
+    value := 0;
+  }
+  method Advance(d: int)
+    requires 0 <= d
+    modifies this
+    ensures value == old(value) + d
+  {
+    value := value + d;
+  }
+}
+
+class Catacar extends Automobile {
+  var f: Fiat
+  var v: Volvo
   predicate Valid()
-    reads this // , Repr
+    reads this, Repr
     ensures Valid() ==> this in Repr
   {
-    this in Repr
+    this in Repr && null !in Repr &&
+    f in Repr && this !in f.Repr && f.Repr <= Repr && f.Valid() &&
+    v in Repr && this !in v.Repr && v.Repr <= Repr && v.Valid() &&
+    f.Repr !! v.Repr &&
+    position == f.position + v.position
   }
-  constructor()
+  constructor ()
     modifies this
-    ensures Valid()
+    ensures Valid() && fresh(Repr - {this})
   {
     Repr := {this};
+    f := new Fiat(0);  Repr := Repr + f.Repr;
+    v := new Volvo();  Repr := Repr + v.Repr;
+    position := v.position;
   }
   function method Brand(): string {
-    "Fiat"
+    "Catacar"
   }
   method Drive()
-//    requires Valid()
-    modifies this // Repr
+    requires Valid()
+    modifies Repr
+    ensures Valid() && fresh(Repr - old(Repr))
     ensures old(position) <= position
   {
-    position := position + 3;
+    f := new Fiat(f.position);
+    f.Drive();  v.Drive();
+    Repr := Repr + v.Repr + f.Repr;
+    position := f.position + v.position;
   }
 }
 
 method Main() {
   var auto: Automobile;
+  auto := new Fiat(0);
+  WorkIt(auto);
   auto := new Volvo();
   WorkIt(auto);
-  auto := new Fiat();
+  auto := new Catacar();
   WorkIt(auto);
 }
 
 method WorkIt(auto: Automobile)
   requires auto != null && auto.Valid()
-  modifies auto // auto.Repr
+  modifies auto.Repr
 {
   auto.Drive();
+  auto.Drive();
+  assert old(auto.position) <= auto.position;
   print auto.Brand(), ": ", auto.position, "\n";
-  auto.position := 0;
+  auto.position := 18;  // note, this may destroy the automobile's consistency condition (given by Valid)
 }
diff --git a/Test/dafny0/Trait/TraitExample.dfy.expect b/Test/dafny0/Trait/TraitExample.dfy.expect
index 4fc71fb5..337b8f2f 100644
--- a/Test/dafny0/Trait/TraitExample.dfy.expect
+++ b/Test/dafny0/Trait/TraitExample.dfy.expect
@@ -1,7 +1,8 @@
 
-Dafny program verifier finished with 25 verified, 0 errors
+Dafny program verifier finished with 38 verified, 0 errors
 Program compiled successfully
 Running...
 
-Volvo: 10
-Fiat: 3
+Fiat: 6
+Volvo: 20
+Catacar: 26
diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect
index 9960c1d9..1517dee4 100644
--- a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect
+++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect
@@ -1,4 +1,4 @@
-TraitUsingParentMembers.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+TraitUsingParentMembers.dfy(10,7): Error: assignment may update an array element not in the enclosing context's modifies clause
 Execution trace:
     (0,0): anon0
     (0,0): anon5_Then
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..7d646bd1 100644
--- a/Test/dafny0/Trait/TraitsDecreases.dfy.expect
+++ b/Test/dafny0/Trait/TraitsDecreases.dfy.expect
@@ -1,17 +1,35 @@
-TraitsDecreases.dfy(57,10): Error: method's decreases clause must be below or equal to that in the trait
+TraitsDecreases.dfy(117,14): Error: predicate's decreases clause must be below or equal to that in the trait
 Execution trace:
     (0,0): anon0
-TraitsDecreases.dfy(69,10): Error: method's decreases clause must be below or equal to that in the trait
+TraitsDecreases.dfy(124,14): Error: predicate's decreases clause must be below or equal to that in the trait
 Execution trace:
     (0,0): anon0
-TraitsDecreases.dfy(72,10): Error: method's decreases clause must be below or equal to that in the trait
+TraitsDecreases.dfy(131,14): Error: predicate's decreases clause must be below or equal to that in the trait
 Execution trace:
     (0,0): anon0
-TraitsDecreases.dfy(78,10): Error: method's decreases clause must be below or equal to that in the trait
+TraitsDecreases.dfy(138,14): Error: predicate's decreases clause must be below or equal to that in the trait
 Execution trace:
     (0,0): anon0
-TraitsDecreases.dfy(88,10): Error: method's decreases clause must be below or equal to that in the trait
+TraitsDecreases.dfy(145,14): Error: predicate's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
+TraitsDecreases.dfy(152,11): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
+TraitsDecreases.dfy(57,9): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
+TraitsDecreases.dfy(69,9): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
+TraitsDecreases.dfy(72,9): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
+TraitsDecreases.dfy(78,9): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+    (0,0): anon0
+TraitsDecreases.dfy(88,9): Error: method's decreases clause must be below or equal to that in the trait
 Execution trace:
     (0,0): anon0
 
-Dafny program verifier finished with 63 verified, 5 errors
+Dafny program verifier finished with 75 verified, 11 errors