diff options
| author |  leino <unknown> | 2014-12-09 19:34:08 -0800 |
|---|---|---|
| committer | leino <unknown> | 2014-12-09 19:34:08 -0800 |
| commit | 2cb39832d3acc19e48d07efd37758d005785f09d (patch) | |
| tree | d0269c15ad86bdd3bb02a84afffde370b489d1f4 /Test/dafny0/Trait | |
| parent | 22ea901b086b05385d98019ee9eefdab97652499 (diff) | |
| parent | 5ceb4c87998c2b0eaa5a6431b717b295e39c2d29 (diff) | |
Merge
Diffstat (limited to 'Test/dafny0/Trait')
| -rw-r--r-- | Test/dafny0/Trait/TraitOverride1.dfy | 13 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitOverride1.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/dafny0/Trait/Traits-Fields.dfy | 38 | ||||
| -rw-r--r-- | Test/dafny0/Trait/Traits-Fields.dfy.expect | 7 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitsMultipleInheritance.dfy | 30 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitsMultipleInheritance.dfy.expect | 7 |
7 files changed, 84 insertions, 15 deletions
diff --git a/Test/dafny0/Trait/TraitOverride1.dfy b/Test/dafny0/Trait/TraitOverride1.dfy index 90a25f53..c963f847 100644 --- a/Test/dafny0/Trait/TraitOverride1.dfy +++ b/Test/dafny0/Trait/TraitOverride1.dfy @@ -124,19 +124,6 @@ class c extends t }
}
-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
diff --git a/Test/dafny0/Trait/TraitOverride1.dfy.expect b/Test/dafny0/Trait/TraitOverride1.dfy.expect index c90560b0..85c793d4 100644 --- a/Test/dafny0/Trait/TraitOverride1.dfy.expect +++ b/Test/dafny0/Trait/TraitOverride1.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 52 verified, 0 errors
+Dafny program verifier finished with 58 verified, 0 errors
diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect index b59d7b80..6849499c 100644 --- a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect +++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect @@ -5,4 +5,4 @@ Execution trace: (0,0): anon2
(0,0): anon6_Then
-Dafny program verifier finished with 7 verified, 1 error
+Dafny program verifier finished with 9 verified, 1 error
diff --git a/Test/dafny0/Trait/Traits-Fields.dfy b/Test/dafny0/Trait/Traits-Fields.dfy new file mode 100644 index 00000000..41f596b4 --- /dev/null +++ b/Test/dafny0/Trait/Traits-Fields.dfy @@ -0,0 +1,38 @@ +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait J
+{
+ var x: int;
+}
+
+class C extends J
+{
+
+}
+
+method Main()
+{
+ var c := new C;
+ var j: J := new C;
+
+ j.x := 8;
+ c.x := 9;
+ assert j.x + 1 == c.x;
+
+ j := c;
+ //assert j.x == 9; //why this does not hold??
+
+ print "j"; Print(j);
+ print "c"; Print(c);
+
+ c := null;
+ assert j != null;
+ j := null;
+}
+
+method Print(j: J)
+ requires j != null;
+{
+ print ".x = ", j.x, "\n";
+}
diff --git a/Test/dafny0/Trait/Traits-Fields.dfy.expect b/Test/dafny0/Trait/Traits-Fields.dfy.expect new file mode 100644 index 00000000..4e367bf5 --- /dev/null +++ b/Test/dafny0/Trait/Traits-Fields.dfy.expect @@ -0,0 +1,7 @@ +
+Dafny program verifier finished with 4 verified, 0 errors
+Program compiled successfully
+Running...
+
+j.x = 9
+c.x = 9
diff --git a/Test/dafny0/Trait/TraitsMultipleInheritance.dfy b/Test/dafny0/Trait/TraitsMultipleInheritance.dfy new file mode 100644 index 00000000..67acbc67 --- /dev/null +++ b/Test/dafny0/Trait/TraitsMultipleInheritance.dfy @@ -0,0 +1,30 @@ +// 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;
+
+ print "c.x + c.y = " , c.x + c.y, "\n";
+ print "j1.x + j2.y = " , j1.x + j2.y, "\n";
+
+ 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..127b65f7 --- /dev/null +++ b/Test/dafny0/Trait/TraitsMultipleInheritance.dfy.expect @@ -0,0 +1,7 @@ +
+Dafny program verifier finished with 2 verified, 0 errors
+Program compiled successfully
+Running...
+
+c.x + c.y = 30
+j1.x + j2.y = 30
|