diff options
| author |  Reza Ahmadi <reza.ahmadi@uta.fi> | 2014-12-03 12:44:41 +0200 |
|---|---|---|
| committer | Reza Ahmadi <reza.ahmadi@uta.fi> | 2014-12-03 12:44:41 +0200 |
| commit | c5d7c43605d832cc64e16c66a2c830a880a3d3a2 (patch) | |
| tree | 2a11e88fa879a224cadd9f488ffbd78b4c35b5d2 /Test/dafny0/Trait/TraitsMultipleInheritance.dfy | |
| parent | fc43d9d56bdf3cae68bb15871f074149d1381c6a (diff) | |
added multiple trait inheritance.
- a class can now extend more than one traits
Diffstat (limited to 'Test/dafny0/Trait/TraitsMultipleInheritance.dfy')
| -rw-r--r-- | Test/dafny0/Trait/TraitsMultipleInheritance.dfy | 27 |
1 files changed, 27 insertions, 0 deletions
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 |