1 files changed, 44 insertions, 0 deletions
diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy b/Test/dafny0/Trait/TraitUsingParentMembers.dfy
new file mode 100644
index 00000000..dd45d0e6
--- /dev/null
+++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy
@@ -0,0 +1,44 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+trait P1
+{
+	method N0() {
+	    var a: array<int>;
+	    if (a != null && 5 < a.Length) {
+	      a[5] := 12;  // error: violates modifies clause
+	    }
+	}
+
+	method Mul(x: int, y: int) returns (r: int)
+	  requires 0 <= x && 0 <= y;
+	  ensures r == x*y;
+	  decreases x;
+}
+
+class C1 extends P1
+{
+    method Mul(x: int, y: int) returns (r: int)
+	  requires 0 <= x && 0 <= y;
+	  ensures r == x*y;
+	  decreases x;
+	{
+	  if (x == 0) {
+		r := 0;
+	  } else {
+		var m := Mul(x-1, y);
+		r := m + y;
+	  }
+	}
+
+   method Testing(arr:array<int>)
+     requires arr != null && arr.Length == 2 && arr[0]== 1 && arr[1] == 10;
+   {
+      N0(); //calling parent trait methods
+      var x := 2;
+      var y := 5;
+      var z := Mul(x,y);
+      assert (z == 10);
+   }   
+}
+\ No newline at end of file