1 files changed, 81 insertions, 0 deletions
diff --git a/Test/dafny0/Trait/TraitOverride0.dfy b/Test/dafny0/Trait/TraitOverride0.dfy
new file mode 100644
index 00000000..a8fb8596
--- /dev/null
+++ b/Test/dafny0/Trait/TraitOverride0.dfy
@@ -0,0 +1,81 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait T1
+{
+   var f: int;
+   
+   function method Plus (x:int, y:int) : int
+     requires x>y;
+   {
+      x + y
+   }
+   
+   function method Mul (x:int, y:int, z:int) : int
+     requires x>y;
+   {
+	x * y * z
+   }
+   
+   function method BodyLess1() : int
+   
+   function method BodyLess2(a:int, b:int) : int
+   
+   static method GetPhoneNumber (code:int, n:int) returns (z:int)
+   {
+	z := code + n;
+   }
+   
+   method TestPhone ()
+   {
+        var num : int;
+	num := GetPhoneNumber (10, 30028);
+   }
+}
+
+trait T2
+{
+}
+
+class C1 extends T1
+{
+    method P2(x:int, y:int) returns (z:int)
+      requires x>y;
+    {
+       z:= Plus(x,y) + Mul (x,y,1);
+    }
+    
+    function method BodyLess1(i:int) : int //error, overriding function has too many parameters
+    {
+	12
+    }
+        
+    function method Mul (x:int, y:int, z:int) : int //error, can not override implemented methods
+     requires x>y;
+   {
+	x * y * z
+   }
+   
+   function method BodyLess2(a:int, b:int) : int
+     {
+	a+b
+     }
+}
+
+class C2 extends T1
+{
+      //error, there are body-less methods in the parent trait that must be implemented	
+}
+
+abstract module AM1
+{
+   trait T2
+   {
+      method Calc(i:int, j:int) returns (k:int)
+   }
+   
+   class T2Client extends T2
+   {
+      method Calc(ii:int, jj:int) returns (kk:int)
+   }
+}
+\ No newline at end of file