added multiple trait inheritance.

- a class can now extend more than one traits

3 files changed, 33 insertions, 1 deletions

diff --git a/Test/dafny0/Trait/Traits-Fields.dfy b/Test/dafny0/Trait/Traits-Fields.dfy
index c215ecf8..41f596b4 100644
--- a/Test/dafny0/Trait/Traits-Fields.dfy
+++ b/Test/dafny0/Trait/Traits-Fields.dfy
@@ -21,7 +21,7 @@ method Main()
   assert j.x + 1 == c.x;

 

   j := c;

-  //assert j.x == 9;

+  //assert j.x == 9; //why this does not hold??

 

   print "j"; Print(j);

   print "c"; Print(c);

diff --git a/Test/dafny0/Trait/TraitsMultipleInheritance.dfy b/Test/dafny0/Trait/TraitsMultipleInheritance.dfy
new file mode 100644
index 00000000..8b26eeea
--- /dev/null
+++ b/Test/dafny0/Trait/TraitsMultipleInheritance.dfy
@@ -0,0 +1,27 @@
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

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

+

+trait J1{

+	var x: int;

+}

+

+trait J2{

+	var y: int;

+}

+

+class C extends J1, J2{  

+}

+

+method Main()

+{

+  var c := new C;

+  var j1: J1 := new C;

+  var j2: J2 := new C;

+  

+  c.x := 10;

+  c.y := 20;

+  j1.x := 20;

+  j2.y := 10;

+  

+  assert c.x + c.y == j1.x + j2.y;

+}
\ No newline at end of file
diff --git a/Test/dafny0/Trait/TraitsMultipleInheritance.dfy.expect b/Test/dafny0/Trait/TraitsMultipleInheritance.dfy.expect
new file mode 100644
index 00000000..d5daa038
--- /dev/null
+++ b/Test/dafny0/Trait/TraitsMultipleInheritance.dfy.expect
@@ -0,0 +1,5 @@
+

+Dafny program verifier finished with 2 verified, 0 errors

+Program compiled successfully

+Running...

+