combined two tests

5 files changed, 86 insertions, 88 deletions

diff --git a/Test/dafny0/Trait/Trait.dfy.expect b/Test/dafny0/Trait/Trait.dfy.expect
deleted file mode 100644
index 253144ea..00000000
--- a/Test/dafny0/Trait/Trait.dfy.expect
+++ /dev/null
@@ -1,5 +0,0 @@
-Trait.dfy(77,13): Error: member in the class has been already inherited from its parent trait

-Trait.dfy(70,7): Error: class: I0Child does not implement trait member: Customizable

-Trait.dfy(80,7): Error: class: I0Child2 does not implement trait member: F

-Trait.dfy(91,7): Error: unresolved identifier: IX

-4 resolution/type errors detected in Trait.dfy

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

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

-

-trait I0 

-{

-   var x: int;

-   constructor I0(x0: int) // error: constructor is not allowed in a trait

-   {

-      x:=x0;

-   }

-}

-

-trait I1

-{

-  function M1(x:int,y:int) :int

-  {

-     x*y

-  }

-}

-

-method TestI1()

-{

-   var i1 := new I1; 	//error: new is not allowed in a trait

-}

-

-trait I2   		//all is fine in this trait

-{

-	var x: int;

-	

-	function method Twice(): int

-	 reads this;

-	{

-		x + x

-	}

-	

-	function method F(z: int): int

-	 reads this;

-

-	 

-	method Compute(s: bool) returns (t: int, u: int)

-	 modifies this;

-	{

-		if s {

-			t, u := F(F(15)), Twice();

-		} else {

-			t := Twice();

-			x := F(45);

-			u := Twice();

-			var p := Customizable(u);

-			return t+p, u;

-		}

-	}

-	

-	method Customizable(w: int) returns (p: int)

-	 modifies this;

-

-	 

-	static method StaticM(a: int) returns (b: int)

-	{

-		b := a;

-	}

-	

-	static method SS(a: int) returns (b:int)

-	{

-		b:=a*2;

-	}

-}

-

-method I2Client(j: I2) returns (p: int)     //all is fine in this client method

- requires j != null;

- modifies j;

-{

-	j.x := 100;

-	var h := j.Twice() + j.F(j.Twice());

-	var a, b := j.Compute(h < 33);

-	var c, d := j.Compute(33 <= h);

-	p := j.Customizable(a + b + c + d);

-	p := I2.StaticM(p);

-}

diff --git a/Test/dafny0/Trait/TraitBasics.dfy.expect b/Test/dafny0/Trait/TraitBasics.dfy.expect
deleted file mode 100644
index c9fb096e..00000000
--- a/Test/dafny0/Trait/TraitBasics.dfy.expect
+++ /dev/null
@@ -1,3 +0,0 @@
-TraitBasics.dfy(4,6): Error: a trait is not allowed to declare a constructor

-TraitBasics.dfy(23,10): Error: new can not be applied to a trait

-2 resolution/type errors detected in TraitBasics.dfy

diff --git a/Test/dafny0/Trait/Trait.dfy b/Test/dafny0/Trait/TraitBasix.dfy
index cf76e860..e16e8fc4 100644
--- a/Test/dafny0/Trait/Trait.dfy
+++ b/Test/dafny0/Trait/TraitBasix.dfy
@@ -92,4 +92,82 @@ module m1
 	{

 	

 	}

-}
\ No newline at end of file
+}

+

+

+trait I0 

+{

+   var x: int;

+   constructor I0(x0: int) // error: constructor is not allowed in a trait

+   {

+      x:=x0;

+   }

+}

+

+trait I1

+{

+  function M1(x:int,y:int) :int

+  {

+     x*y

+  }

+}

+

+method TestI1()

+{

+   var i1 := new I1; 	//error: new is not allowed in a trait

+}

+

+trait I2   		//all is fine in this trait

+{

+	var x: int;

+	

+	function method Twice(): int

+	 reads this;

+	{

+		x + x

+	}

+	

+	function method F(z: int): int

+	 reads this;

+

+	 

+	method Compute(s: bool) returns (t: int, u: int)

+	 modifies this;

+	{

+		if s {

+			t, u := F(F(15)), Twice();

+		} else {

+			t := Twice();

+			x := F(45);

+			u := Twice();

+			var p := Customizable(u);

+			return t+p, u;

+		}

+	}

+	

+	method Customizable(w: int) returns (p: int)

+	 modifies this;

+

+	 

+	static method StaticM(a: int) returns (b: int)

+	{

+		b := a;

+	}

+	

+	static method SS(a: int) returns (b:int)

+	{

+		b:=a*2;

+	}

+}

+

+method I2Client(j: I2) returns (p: int)     //all is fine in this client method

+ requires j != null;

+ modifies j;

+{

+	j.x := 100;

+	var h := j.Twice() + j.F(j.Twice());

+	var a, b := j.Compute(h < 33);

+	var c, d := j.Compute(33 <= h);

+	p := j.Customizable(a + b + c + d);

+	p := I2.StaticM(p);

+}

diff --git a/Test/dafny0/Trait/TraitBasix.dfy.expect b/Test/dafny0/Trait/TraitBasix.dfy.expect
new file mode 100644
index 00000000..1d44d0f6
--- /dev/null
+++ b/Test/dafny0/Trait/TraitBasix.dfy.expect
@@ -0,0 +1,7 @@
+TraitBasix.dfy(77,13): Error: member in the class has been already inherited from its parent trait

+TraitBasix.dfy(70,7): Error: class: I0Child does not implement trait member: Customizable

+TraitBasix.dfy(80,7): Error: class: I0Child2 does not implement trait member: F

+TraitBasix.dfy(91,7): Error: unresolved identifier: IX

+TraitBasix.dfy(98,6): Error: a trait is not allowed to declare a constructor

+TraitBasix.dfy(117,10): Error: new can not be applied to a trait

+6 resolution/type errors detected in TraitBasix.dfy