combined few tests

8 files changed, 141 insertions, 154 deletions

diff --git a/Test/dafny0/Trait/TraitOverride1.dfy b/Test/dafny0/Trait/TraitOverride1.dfy
index 980054ee..90a25f53 100644
--- a/Test/dafny0/Trait/TraitOverride1.dfy
+++ b/Test/dafny0/Trait/TraitOverride1.dfy
@@ -1,6 +1,7 @@
 // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

+//everything should work OK in this test file

 trait T1

 {

    function method Plus (x:int, y:int) : int

@@ -52,3 +53,142 @@ class C1 extends T1
    }

 }

 

+trait T2 

+{

+	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 C2 extends T2 

+{

+	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;

+	}

+}

+

+

+trait T3 

+{

+	function method F(y: int): int

+	function method G(y: int): int { 12 }

+	method M(y: int)

+	method N(y: int) {  

+           var a:int := 100;

+	   assert a==100;

+	}

+}

+class C3 extends T3

+{

+	function method NewFunc (a:int, b:int) : int

+	{

+	    a + b

+	}

+	function method F(y: int): int { 20 }

+	method M(y: int) { 

+	   var a:int := 100;

+	   assert a==100;

+	}

+}

+

+trait t

+{

+  function f(s2:int):int

+  ensures f(s2) > 0;

+  //requires s != null && s.Length > 1;

+  //reads s, s2;

+}

+

+class c extends t

+{

+  function f(s3:int):int

+  ensures f(s3) > 1;

+  //requires s0 != null && s0.Length > (0);

+  //reads s0;

+  { 

+     2

+  }

+}

+

+trait P1

+{

+  method M(N: int, a: array<int>) returns (sum: int)

+  {

+    sum := 1;   

+  }

+}

+

+class CC1 extends P1

+{

+

+}

+

+trait TT

+{

+   static function method M(a:int, b:int) : int

+     ensures M(a,b) == a + b;

+   {

+       a + b

+   }

+}

+

+class CC extends TT 

+{

+   method Testing(a:int,b:int)

+   {

+       assert (TT.M(a,b) == a + b);

+   }

+}

+

+

+trait T4 

+{

+	function method F(y: int): int

+	

+	function method G(y: int): int 

+	{ 

+	   100 

+	}

+	

+	method M(y: int) returns (kobra:int)

+	  requires y > 0;

+	  ensures kobra > 0;

+	   

+	method N(y: int) 

+	{ 

+	   var x: int;

+	   var y : int;

+	   y := 10;

+	   x := 1000;

+	   y := y + x;

+	}

+}

+

+class C4 extends T4 

+{

+	function method F(y: int): int 

+	{ 

+	  200 

+	}

+

+	method M(kk:int) returns (ksos:int)

+	  requires kk > (-1);

+	  ensures ksos > 0;

+	{

+		ksos:=10;	

+	}	 

+}

diff --git a/Test/dafny0/Trait/TraitOverride1.dfy.expect b/Test/dafny0/Trait/TraitOverride1.dfy.expect
index 5f41963f..0f7b49e3 100644
--- a/Test/dafny0/Trait/TraitOverride1.dfy.expect
+++ b/Test/dafny0/Trait/TraitOverride1.dfy.expect
@@ -1,2 +1,2 @@
 

-Dafny program verifier finished with 17 verified, 0 errors

+Dafny program verifier finished with 62 verified, 0 errors

diff --git a/Test/dafny0/Trait/TraitOverride2.dfy b/Test/dafny0/Trait/TraitOverride2.dfy
deleted file mode 100644
index fca79b2e..00000000
--- a/Test/dafny0/Trait/TraitOverride2.dfy
+++ /dev/null
@@ -1,30 +0,0 @@
-// 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
diff --git a/Test/dafny0/Trait/TraitOverride2.dfy.expect b/Test/dafny0/Trait/TraitOverride2.dfy.expect
deleted file mode 100644
index 76f19e0d..00000000
--- a/Test/dafny0/Trait/TraitOverride2.dfy.expect
+++ /dev/null
@@ -1,2 +0,0 @@
-

-Dafny program verifier finished with 7 verified, 0 errors

diff --git a/Test/dafny0/Trait/TraitOverride3.dfy b/Test/dafny0/Trait/TraitOverride3.dfy
deleted file mode 100644
index 6a5fa59f..00000000
--- a/Test/dafny0/Trait/TraitOverride3.dfy
+++ /dev/null
@@ -1,76 +0,0 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-

-

-//everything should work OK in the following program

-trait J 

-{

-	function method F(y: int): int

-	function method G(y: int): int { 12 }

-	method M(y: int)

-	method N(y: int) {  

-           var a:int := 100;

-	   assert a==100;

-	}

-}

-class C extends J 

-{

-	function method NewFunc (a:int, b:int) : int

-	{

-	    a + b

-	}

-	function method F(y: int): int { 20 }

-	method M(y: int) { 

-	   var a:int := 100;

-	   assert a==100;

-	}

-}

-

-trait t

-{

-  function f(s2:int):int

-  ensures f(s2) > 0;

-  //requires s != null && s.Length > 1;

-  //reads s, s2;

-}

-

-class c extends t

-{

-  function f(s3:int):int

-  ensures f(s3) > 1;

-  //requires s0 != null && s0.Length > (0);

-  //reads s0;

-  { 

-     2

-  }

-}

-

-trait P1

-{

-  method M(N: int, a: array<int>) returns (sum: int)

-  {

-    sum := 1;   

-  }

-}

-

-class C1 extends P1

-{

-

-}

-

-trait TT

-{

-   static function method M(a:int, b:int) : int

-     ensures M(a,b) == a + b;

-   {

-       a + b

-   }

-}

-

-class CC extends TT 

-{

-   method Testing(a:int,b:int)

-   {

-       assert (TT.M(a,b) == a + b);

-   }

-}

diff --git a/Test/dafny0/Trait/TraitOverride3.dfy.expect b/Test/dafny0/Trait/TraitOverride3.dfy.expect
deleted file mode 100644
index 9d7e625f..00000000
--- a/Test/dafny0/Trait/TraitOverride3.dfy.expect
+++ /dev/null
@@ -1,2 +0,0 @@
-

-Dafny program verifier finished with 25 verified, 0 errors

diff --git a/Test/dafny0/Trait/TraitOverride4.dfy b/Test/dafny0/Trait/TraitOverride4.dfy
deleted file mode 100644
index c9cc3953..00000000
--- a/Test/dafny0/Trait/TraitOverride4.dfy
+++ /dev/null
@@ -1,41 +0,0 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-

-

-trait J 

-{

-	function method F(y: int): int

-	

-	function method G(y: int): int 

-	{ 

-	   100 

-	}

-	

-	method M(y: int) returns (kobra:int)

-	  requires y > 0;

-	  ensures kobra > 0;

-	   

-	method N(y: int) 

-	{ 

-	   var x: int;

-	   var y : int;

-	   y := 10;

-	   x := 1000;

-	   y := y + x;

-	}

-}

-

-class C extends J 

-{

-	function method F(y: int): int 

-	{ 

-	  200 

-	}

-

-	method M(kk:int) returns (ksos:int)

-	  requires kk > (-1);

-	  ensures ksos > 0;

-	{

-		ksos:=10;	

-	}	 

-}
\ No newline at end of file
diff --git a/Test/dafny0/Trait/TraitOverride4.dfy.expect b/Test/dafny0/Trait/TraitOverride4.dfy.expect
deleted file mode 100644
index aeb37948..00000000
--- a/Test/dafny0/Trait/TraitOverride4.dfy.expect
+++ /dev/null
@@ -1,2 +0,0 @@
-

-Dafny program verifier finished with 13 verified, 0 errors