diff options
| author |  Reza Ahmadi <reza.ahmadi@uta.fi> | 2014-07-18 21:16:40 +0300 |
|---|---|---|
| committer | Reza Ahmadi <reza.ahmadi@uta.fi> | 2014-07-18 21:16:40 +0300 |
| commit | 77143c833cbb14a20c704fb60fc28dd94edb44eb (patch) | |
| tree | 7da7588d8dccb94fb1c5c42f23ec69c4edab2785 /Test/dafny0/Trait | |
| parent | c377658acba5472b6d0c1e1452ce4c4c8f1fc28e (diff) | |
added trait feature:
-possibility to declare traits in Dafny
-possibility to extend a class by a trait
-possibility to override body-less methods
Diffstat (limited to 'Test/dafny0/Trait')
22 files changed, 618 insertions, 0 deletions
diff --git a/Test/dafny0/Trait/Trait.dfy b/Test/dafny0/Trait/Trait.dfy new file mode 100644 index 00000000..cf76e860 --- /dev/null +++ b/Test/dafny0/Trait/Trait.dfy @@ -0,0 +1,95 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module m1
+{
+ trait I1
+ {
+ function M1(x:int,y:int) :int
+ {
+ x*y
+ }
+ }
+
+
+ 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);
+ }
+
+ class I0Child extends I2 //errors, body-less methods/functions in the parent have not implemented here
+ {
+ function method F(z: int): int
+ reads this;
+ {
+ z
+ }
+ var x: int; //error, x has been declared in the parent trait
+ }
+
+ class I0Child2 extends I2
+ {
+ method Customizable(w: int) returns (p: int)
+ modifies this;
+ {
+ w:=w+1;
+ }
+
+ var c1: I0Child;
+ }
+
+ class IXChild extends IX //error, IX trait is undefined
+ {
+
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/Trait/Trait.dfy.expect b/Test/dafny0/Trait/Trait.dfy.expect new file mode 100644 index 00000000..253144ea --- /dev/null +++ b/Test/dafny0/Trait/Trait.dfy.expect @@ -0,0 +1,5 @@ +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 new file mode 100644 index 00000000..6bfe76bb --- /dev/null +++ b/Test/dafny0/Trait/TraitBasics.dfy @@ -0,0 +1,79 @@ +// 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 new file mode 100644 index 00000000..c9fb096e --- /dev/null +++ b/Test/dafny0/Trait/TraitBasics.dfy.expect @@ -0,0 +1,3 @@ +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/TraitExtend.dfy b/Test/dafny0/Trait/TraitExtend.dfy new file mode 100644 index 00000000..1a59439c --- /dev/null +++ b/Test/dafny0/Trait/TraitExtend.dfy @@ -0,0 +1,43 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait t
+{
+ var f: int;
+
+ function method Plus (x:int, y:int) : int
+ requires x>y;
+ {
+ x + y
+ }
+
+ function method Mul (x:int, y:int, z:int) : int
+ requires x>y;
+ {
+ x * y * z
+ }
+
+ //function method BodyLess1() : int
+
+ static method GetPhoneNumber (code:int, n:int) returns (z:int)
+ {
+ z := code + n;
+ }
+
+ method TestPhone ()
+ {
+ var num : int;
+ num := GetPhoneNumber (10, 30028);
+ }
+}
+
+class c1 extends t
+{
+ method P2(x:int, y:int) returns (z:int)
+ requires x>y;
+ {
+ z:= Plus(x,y) + Mul (x,y,1);
+ var j:int := Mul (x,y); //error, too few parameters in calling inherited method
+ var k:int := Plus(x,y,1); //error, too many parameters in calling inherited method
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/Trait/TraitExtend.dfy.expect b/Test/dafny0/Trait/TraitExtend.dfy.expect new file mode 100644 index 00000000..73a24ad8 --- /dev/null +++ b/Test/dafny0/Trait/TraitExtend.dfy.expect @@ -0,0 +1,3 @@ +TraitExtend.dfy(40,20): Error: wrong number of function arguments (got 2, expected 3)
+TraitExtend.dfy(41,20): Error: wrong number of function arguments (got 3, expected 2)
+2 resolution/type errors detected in TraitExtend.dfy
diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy b/Test/dafny0/Trait/TraitMultiModule.dfy new file mode 100644 index 00000000..f60db7b4 --- /dev/null +++ b/Test/dafny0/Trait/TraitMultiModule.dfy @@ -0,0 +1,26 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module M1
+{
+ trait T1
+ {
+ method M1 (a:int)
+ }
+ class C1 extends T1
+ {
+ method M1 (x:int)
+ {
+ var y: int := x;
+ }
+ }
+}
+
+module M2
+{
+ class C2 extends T1
+ {
+
+ }
+
+}
\ No newline at end of file diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy.expect b/Test/dafny0/Trait/TraitMultiModule.dfy.expect new file mode 100644 index 00000000..589fba07 --- /dev/null +++ b/Test/dafny0/Trait/TraitMultiModule.dfy.expect @@ -0,0 +1,2 @@ +TraitMultiModule.dfy(21,9): Error: class M2.C2 is in a different module than trait M1.T1. A class may only extend a trait in the same module
+1 resolution/type errors detected in TraitMultiModule.dfy
diff --git a/Test/dafny0/Trait/TraitOverride0.dfy b/Test/dafny0/Trait/TraitOverride0.dfy new file mode 100644 index 00000000..a8fb8596 --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride0.dfy @@ -0,0 +1,81 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait T1
+{
+ var f: int;
+
+ function method Plus (x:int, y:int) : int
+ requires x>y;
+ {
+ x + y
+ }
+
+ function method Mul (x:int, y:int, z:int) : int
+ requires x>y;
+ {
+ x * y * z
+ }
+
+ function method BodyLess1() : int
+
+ function method BodyLess2(a:int, b:int) : int
+
+ static method GetPhoneNumber (code:int, n:int) returns (z:int)
+ {
+ z := code + n;
+ }
+
+ method TestPhone ()
+ {
+ var num : int;
+ num := GetPhoneNumber (10, 30028);
+ }
+}
+
+trait T2
+{
+}
+
+class C1 extends T1
+{
+ method P2(x:int, y:int) returns (z:int)
+ requires x>y;
+ {
+ z:= Plus(x,y) + Mul (x,y,1);
+ }
+
+ function method BodyLess1(i:int) : int //error, overriding function has too many parameters
+ {
+ 12
+ }
+
+ function method Mul (x:int, y:int, z:int) : int //error, can not override implemented methods
+ requires x>y;
+ {
+ x * y * z
+ }
+
+ function method BodyLess2(a:int, b:int) : int
+ {
+ a+b
+ }
+}
+
+class C2 extends T1
+{
+ //error, there are body-less methods in the parent trait that must be implemented
+}
+
+abstract module AM1
+{
+ trait T2
+ {
+ method Calc(i:int, j:int) returns (k:int)
+ }
+
+ class T2Client extends T2
+ {
+ method Calc(ii:int, jj:int) returns (kk:int)
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/Trait/TraitOverride0.dfy.expect b/Test/dafny0/Trait/TraitOverride0.dfy.expect new file mode 100644 index 00000000..4020b880 --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride0.dfy.expect @@ -0,0 +1,5 @@ +TraitOverride0.dfy(53,20): Error: a class can not override implemented functions
+TraitOverride0.dfy(48,20): Error: function 'BodyLess1' is declared with a different number of parameter (1 instead of 0) than the corresponding function in the module it overrides
+TraitOverride0.dfy(65,6): Error: class: C2 does not implement trait member: BodyLess1
+TraitOverride0.dfy(65,6): Error: class: C2 does not implement trait member: BodyLess2
+4 resolution/type errors detected in TraitOverride0.dfy
diff --git a/Test/dafny0/Trait/TraitOverride1.dfy b/Test/dafny0/Trait/TraitOverride1.dfy new file mode 100644 index 00000000..980054ee --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride1.dfy @@ -0,0 +1,54 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait T1
+{
+ function method Plus (x:int, y:int) : int
+ requires x>y;
+ {
+ x + y
+ }
+
+ function method bb(x:int):int
+ requires x>10;
+
+ function method BodyLess1(a:int) : int
+ requires a > 0;
+
+ function method dd(a:int) : int
+
+ method Testing()
+}
+
+class C1 extends T1
+{
+ function method dd(x:int):int
+ {
+ 2
+ }
+
+ method Testing()
+ {
+ var x:int := 11;
+ x := bb(x);
+ }
+
+ function method bb(x:int):int
+ requires x >10;
+ {
+ x
+ }
+ function method BodyLess1(bda:int) : int
+ requires bda > (-10);
+ {
+ 2
+ }
+
+ method CallBodyLess(x:int)
+ requires x > (-10);
+ {
+ var k:int := BodyLess1(x);
+ assert (k==2);
+ }
+}
+
diff --git a/Test/dafny0/Trait/TraitOverride1.dfy.expect b/Test/dafny0/Trait/TraitOverride1.dfy.expect new file mode 100644 index 00000000..5f41963f --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride1.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 17 verified, 0 errors
diff --git a/Test/dafny0/Trait/TraitOverride2.dfy b/Test/dafny0/Trait/TraitOverride2.dfy new file mode 100644 index 00000000..fca79b2e --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride2.dfy @@ -0,0 +1,30 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait J
+{
+ function method F(x: int): int
+ requires x < 100;
+ ensures F(x) < 100;
+
+ method M(x: int) returns (y: int)
+ requires 0 <= x;
+ ensures x < y;
+}
+
+class C extends J
+{
+ function method F(x: int): int
+ requires x < 100;
+ ensures F(x) < 100;
+ {
+ x
+ }
+
+ method M(x: int) returns (y: int)
+ requires -2000 <= x; // a more permissive precondition than in the interface
+ ensures 2*x < y; // a more detailed postcondition than in the interface
+ {
+ y := (2 * x) + 1;
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/Trait/TraitOverride2.dfy.expect b/Test/dafny0/Trait/TraitOverride2.dfy.expect new file mode 100644 index 00000000..76f19e0d --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride2.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 7 verified, 0 errors
diff --git a/Test/dafny0/Trait/TraitOverride3.dfy b/Test/dafny0/Trait/TraitOverride3.dfy new file mode 100644 index 00000000..498a0a6b --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride3.dfy @@ -0,0 +1,28 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+//related compiler changes
+//everything works OK in the following code
+trait J
+{
+ function method F(y: int): int
+ function method G(y: int): int { 12 }
+ method M(y: int)
+ method N(y: int) {
+ var a:int := 100;
+ assert a==100;
+ }
+}
+class C extends J
+{
+ function method NewFunc (a:int, b:int) : int
+ {
+ a + b
+ }
+ function method F(y: int): int { 20 }
+ method M(y: int) {
+ var a:int := 100;
+ assert a==100;
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/Trait/TraitOverride3.dfy.expect b/Test/dafny0/Trait/TraitOverride3.dfy.expect new file mode 100644 index 00000000..f5019f3b --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride3.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 14 verified, 0 errors
diff --git a/Test/dafny0/Trait/TraitOverride4.dfy b/Test/dafny0/Trait/TraitOverride4.dfy new file mode 100644 index 00000000..c9cc3953 --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride4.dfy @@ -0,0 +1,41 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+trait J
+{
+ function method F(y: int): int
+
+ function method G(y: int): int
+ {
+ 100
+ }
+
+ method M(y: int) returns (kobra:int)
+ requires y > 0;
+ ensures kobra > 0;
+
+ method N(y: int)
+ {
+ var x: int;
+ var y : int;
+ y := 10;
+ x := 1000;
+ y := y + x;
+ }
+}
+
+class C extends J
+{
+ function method F(y: int): int
+ {
+ 200
+ }
+
+ method M(kk:int) returns (ksos:int)
+ requires kk > (-1);
+ ensures ksos > 0;
+ {
+ ksos:=10;
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/Trait/TraitOverride4.dfy.expect b/Test/dafny0/Trait/TraitOverride4.dfy.expect new file mode 100644 index 00000000..aeb37948 --- /dev/null +++ b/Test/dafny0/Trait/TraitOverride4.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 13 verified, 0 errors
diff --git a/Test/dafny0/Trait/TraitPolymorphism.dfy b/Test/dafny0/Trait/TraitPolymorphism.dfy new file mode 100644 index 00000000..b1ee9eea --- /dev/null +++ b/Test/dafny0/Trait/TraitPolymorphism.dfy @@ -0,0 +1,65 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait T1
+{
+ var f: int;
+
+ function method Plus (x:int, y:int) : int
+ requires x>y;
+ {
+ x + y
+ }
+
+ function method Mul (x:int, y:int, z:int) : int
+ requires x>y;
+ {
+ x * y * z
+ }
+
+ //function method BodyLess1() : int
+
+ static method GetPhoneNumber (code:int, n:int) returns (z:int)
+ {
+ z := code + n;
+ }
+
+ method TestPhone ()
+ {
+ var num : int;
+ num := GetPhoneNumber (10, 30028);
+ }
+}
+
+trait T2
+{
+}
+
+class C1 extends T1
+{
+ method P2(x:int, y:int) returns (z:int)
+ requires x>y;
+ {
+ z:= Plus(x,y) + Mul (x,y,1);
+ }
+}
+
+
+
+method Good(c: C1) returns (t: T1)
+ensures c == t;
+{
+ t := c;
+}
+
+method Bad1(c: C1) returns (t: T2)
+ensures c == t;
+{
+ t := c; //error, C1 has not implemented T2
+}
+
+method Bad2(c: C1) returns (t: T1)
+ensures c == t;
+{
+ c := t; //error, can not assign a trait to a class
+}
diff --git a/Test/dafny0/Trait/TraitPolymorphism.dfy.expect b/Test/dafny0/Trait/TraitPolymorphism.dfy.expect new file mode 100644 index 00000000..8c68b4b9 --- /dev/null +++ b/Test/dafny0/Trait/TraitPolymorphism.dfy.expect @@ -0,0 +1,4 @@ +TraitPolymorphism.dfy(56,10): Error: arguments must have the same type (got C1 and T2)
+TraitPolymorphism.dfy(58,6): Error: RHS (of type C1) not assignable to LHS (of type T2)
+TraitPolymorphism.dfy(64,4): Error: LHS of assignment must denote a mutable variable
+3 resolution/type errors detected in TraitPolymorphism.dfy
diff --git a/Test/dafny0/Trait/TraitSpecsOverride0.dfy b/Test/dafny0/Trait/TraitSpecsOverride0.dfy new file mode 100644 index 00000000..5b4417c3 --- /dev/null +++ b/Test/dafny0/Trait/TraitSpecsOverride0.dfy @@ -0,0 +1,41 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+trait J
+{
+ function method F(k:int, y: array<int>): int
+ reads y;
+ decreases k;
+
+ function method G(y: int): int
+ {
+ 100
+ }
+
+ method M(y: int) returns (kobra:int)
+ requires y > 0;
+ ensures kobra > 0;
+
+ method N(y: int)
+ {
+ var x: int;
+ var y : int;
+ y := 10;
+ x := 1000;
+ y := y + x;
+ }
+}
+
+class C extends J
+{
+ function method F(kk:int, yy: array<int>): int
+ {
+ 200
+ }
+
+ method M(kk:int) returns (ksos:int) //errors here, M must provide its own specifications
+ {
+ ksos:=10;
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect b/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect new file mode 100644 index 00000000..cbdcdf05 --- /dev/null +++ b/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect @@ -0,0 +1,5 @@ +TraitSpecsOverride0.dfy(32,17): Error: Function must provide its own Reads clauses anew
+TraitSpecsOverride0.dfy(32,17): Error: Function must provide its own Decreases clauses anew
+TraitSpecsOverride0.dfy(37,8): Error: Method must provide its own Requires clauses anew
+TraitSpecsOverride0.dfy(37,8): Error: Method must provide its own Ensures clauses anew
+4 resolution/type errors detected in TraitSpecsOverride0.dfy
|