diff options
author | Reza Ahmadi <reza.ahmadi@uta.fi> | 2014-07-31 17:01:45 +0300 |
---|---|---|
committer | Reza Ahmadi <reza.ahmadi@uta.fi> | 2014-07-31 17:01:45 +0300 |
commit | c6f5d1f5ee5e869406f25d3c0603aae9fa45e699 (patch) | |
tree | 1e895e8249e3a420e70da41c122fe615175785c9 /Test/dafny0/Trait | |
parent | 540c87e2a7ded5ecec189f0ef3cd97fd692d181a (diff) |
combined two tests
Diffstat (limited to 'Test/dafny0/Trait')
-rw-r--r-- | Test/dafny0/Trait/Trait.dfy.expect | 5 | ||||
-rw-r--r-- | Test/dafny0/Trait/TraitBasics.dfy | 79 | ||||
-rw-r--r-- | Test/dafny0/Trait/TraitBasics.dfy.expect | 3 | ||||
-rw-r--r-- | Test/dafny0/Trait/TraitBasix.dfy (renamed from Test/dafny0/Trait/Trait.dfy) | 80 | ||||
-rw-r--r-- | Test/dafny0/Trait/TraitBasix.dfy.expect | 7 |
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
|