1 files changed, 30 insertions, 0 deletions
diff --git a/Test/dafny0/Trait/TraitOverride2.dfy b/Test/dafny0/Trait/TraitOverride2.dfy
new file mode 100644
index 00000000..fca79b2e
--- /dev/null
+++ b/Test/dafny0/Trait/TraitOverride2.dfy
@@ -0,0 +1,30 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait J 
+{
+	function method F(x: int): int
+	requires x < 100;
+	ensures F(x) < 100;
+	
+	method M(x: int) returns (y: int)
+	requires 0 <= x;
+	ensures x < y;
+}
+
+class C extends J 
+{
+	function method F(x: int): int
+	requires x < 100;
+	ensures F(x) < 100;
+	{
+	   x
+	}
+	
+	method M(x: int) returns (y: int)
+	requires -2000 <= x; // a more permissive precondition than in the interface
+	ensures 2*x < y; // a more detailed postcondition than in the interface
+	{
+	   y := (2 * x) + 1;
+	}
+}
+\ No newline at end of file