diff options
| author |  leino <unknown> | 2015-04-03 23:56:19 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-04-03 23:56:19 -0700 |
| commit | cee337934c619bfeb646d83243eff1f08e83902d (patch) | |
| tree | bbb66d0de46fef2c342f61e194bdd77c71a339d2 | |
| parent | 098607bcd7deade4835c35111a80b0af5de4151c (diff) | |
Whitespace deltas in test files (in particular, removing tabs and adjusting some indentation)
| -rw-r--r-- | Test/dafny0/Trait/TraitBasix.dfy | 280 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitBasix.dfy.expect | 10 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitExtend.dfy | 56 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitExtend.dfy.expect | 4 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitMultiModule.dfy | 19 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitMultiModule.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitOverride0.dfy | 18 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitOverride1.dfy | 242 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitPolymorphism.dfy | 8 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitSpecsOverride0.dfy | 98 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitUsingParentMembers.dfy | 64 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitsMultipleInheritance.dfy | 4 |
13 files changed, 403 insertions, 404 deletions
diff --git a/Test/dafny0/Trait/TraitBasix.dfy b/Test/dafny0/Trait/TraitBasix.dfy index e16e8fc4..eaf4ba4b 100644 --- a/Test/dafny0/Trait/TraitBasix.dfy +++ b/Test/dafny0/Trait/TraitBasix.dfy @@ -3,95 +3,95 @@ 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
- {
-
- }
+ 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
+ {
+
+ }
}
@@ -100,7 +100,7 @@ trait I0 var x: int;
constructor I0(x0: int) // error: constructor is not allowed in a trait
{
- x:=x0;
+ x:=x0;
}
}
@@ -108,66 +108,66 @@ trait I1 {
function M1(x:int,y:int) :int
{
- x*y
+ x*y
}
}
method TestI1()
{
- var i1 := new I1; //error: new is not allowed in a trait
+ var i1 := new I1; //error: new is not allowed in a trait
}
-trait I2 //all is fine in this 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;
- }
+ 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;
+ 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);
+ 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 index 4a908ee7..5ebf1d5c 100644 --- a/Test/dafny0/Trait/TraitBasix.dfy.expect +++ b/Test/dafny0/Trait/TraitBasix.dfy.expect @@ -1,7 +1,7 @@ -TraitBasix.dfy(91,23): Error: unresolved identifier: IX
-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,24): Error: unresolved identifier: IX
+TraitBasix.dfy(77,8): Error: member in the class has been already inherited from its parent trait
+TraitBasix.dfy(70,8): Error: class: I0Child does not implement trait member: Customizable
+TraitBasix.dfy(80,8): Error: class: I0Child2 does not implement trait member: F
TraitBasix.dfy(98,6): Error: a trait is not allowed to declare a constructor
-TraitBasix.dfy(117,10): Error: new cannot be applied to a trait
+TraitBasix.dfy(117,9): Error: new cannot be applied to a trait
6 resolution/type errors detected in TraitBasix.dfy
diff --git a/Test/dafny0/Trait/TraitExtend.dfy b/Test/dafny0/Trait/TraitExtend.dfy index 1a59439c..f0e9dd33 100644 --- a/Test/dafny0/Trait/TraitExtend.dfy +++ b/Test/dafny0/Trait/TraitExtend.dfy @@ -3,41 +3,41 @@ trait t
{
- var f: int;
+ var f: int;
- function method Plus (x:int, y:int) : int
- requires x>y;
- {
- x + y
- }
+ 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 Mul (x:int, y:int, z:int) : int
+ requires x>y;
+ {
+ x * y * z
+ }
- //function method BodyLess1() : int
+ //function method BodyLess1() : int
- static method GetPhoneNumber (code:int, n:int) returns (z:int)
- {
- z := code + n;
- }
+ static method GetPhoneNumber (code:int, n:int) returns (z:int)
+ {
+ z := code + n;
+ }
- method TestPhone ()
- {
- var num : int;
- num := GetPhoneNumber (10, 30028);
- }
+ 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
- }
+ 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 index 2051fd81..69f4befa 100644 --- a/Test/dafny0/Trait/TraitExtend.dfy.expect +++ b/Test/dafny0/Trait/TraitExtend.dfy.expect @@ -1,3 +1,3 @@ -TraitExtend.dfy(40,24): Error: wrong number of arguments to function application (function 'Mul' expects 3, got 2)
-TraitExtend.dfy(41,24): Error: wrong number of arguments to function application (function 'Plus' expects 2, got 3)
+TraitExtend.dfy(40,21): Error: wrong number of arguments to function application (function 'Mul' expects 3, got 2)
+TraitExtend.dfy(41,21): Error: wrong number of arguments to function application (function 'Plus' expects 2, got 3)
2 resolution/type errors detected in TraitExtend.dfy
diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy b/Test/dafny0/Trait/TraitMultiModule.dfy index f60db7b4..b31e4b0d 100644 --- a/Test/dafny0/Trait/TraitMultiModule.dfy +++ b/Test/dafny0/Trait/TraitMultiModule.dfy @@ -5,22 +5,21 @@ module M1 {
trait T1
{
- method M1 (a:int)
+ method M1 (a:int)
}
class C1 extends T1
{
- method M1 (x:int)
- {
- var y: int := x;
- }
+ method M1 (x:int)
+ {
+ var y: int := x;
+ }
}
}
module M2
{
- class C2 extends T1
- {
+ 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 index b9031dac..a1617395 100644 --- a/Test/dafny0/Trait/TraitMultiModule.dfy.expect +++ b/Test/dafny0/Trait/TraitMultiModule.dfy.expect @@ -1,2 +1,2 @@ -TraitMultiModule.dfy(21,20): Error: class M2.C2 is in a different module than trait M1.T1. A class may only extend a trait in the same module
+TraitMultiModule.dfy(21,19): 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 index a8fb8596..63ca94ce 100644 --- a/Test/dafny0/Trait/TraitOverride0.dfy +++ b/Test/dafny0/Trait/TraitOverride0.dfy @@ -14,7 +14,7 @@ trait T1 function method Mul (x:int, y:int, z:int) : int
requires x>y;
{
- x * y * z
+ x * y * z
}
function method BodyLess1() : int
@@ -23,13 +23,13 @@ trait T1 static method GetPhoneNumber (code:int, n:int) returns (z:int)
{
- z := code + n;
+ z := code + n;
}
method TestPhone ()
{
- var num : int;
- num := GetPhoneNumber (10, 30028);
+ var num : int;
+ num := GetPhoneNumber (10, 30028);
}
}
@@ -47,24 +47,24 @@ class C1 extends T1 function method BodyLess1(i:int) : int //error, overriding function has too many parameters
{
- 12
+ 12
}
function method Mul (x:int, y:int, z:int) : int //error, can not override implemented methods
requires x>y;
{
- x * y * z
+ x * y * z
}
function method BodyLess2(a:int, b:int) : int
{
- a+b
+ a+b
}
}
class C2 extends T1
{
- //error, there are body-less methods in the parent trait that must be implemented
+ //error, there are body-less methods in the parent trait that must be implemented
}
abstract module AM1
@@ -78,4 +78,4 @@ abstract module AM1 {
method Calc(ii:int, jj:int) returns (kk:int)
}
-}
\ No newline at end of file +}
diff --git a/Test/dafny0/Trait/TraitOverride1.dfy b/Test/dafny0/Trait/TraitOverride1.dfy index c963f847..d0d16401 100644 --- a/Test/dafny0/Trait/TraitOverride1.dfy +++ b/Test/dafny0/Trait/TraitOverride1.dfy @@ -4,178 +4,178 @@ //everything should work OK in this test file
trait T1
{
- function method Plus (x:int, y:int) : int
- requires x>y;
- {
- x + y
- }
+ 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 bb(x:int):int
- requires x>10;
+ function method dd(a:int) : int
- function method BodyLess1(a:int) : int
- requires a > 0;
-
- function method dd(a:int) : int
-
- method Testing()
+ 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
+ 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);
- }
+ {
+ 2
+ }
+
+ method CallBodyLess(x:int)
+ requires x > (-10);
+ {
+ var k:int := BodyLess1(x);
+ assert (k==2);
+ }
}
trait T2
{
- 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;
+ 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 C2 extends T2
{
- 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;
- }
+ 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;
+ }
}
trait T3
{
- 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;
- }
+ 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 C3 extends T3
{
- 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;
- }
+ 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;
+ }
}
trait t
{
function f(s2:int):int
- ensures f(s2) > 0;
- //requires s != null && s.Length > 1;
- //reads s, s2;
+ ensures f(s2) > 0;
+ //requires s != null && s.Length > 1;
+ //reads s, s2;
}
class c extends t
{
function f(s3:int):int
- ensures f(s3) > 1;
- //requires s0 != null && s0.Length > (0);
- //reads s0;
+ ensures f(s3) > 1;
+ //requires s0 != null && s0.Length > (0);
+ //reads s0;
{
- 2
+ 2
}
}
trait TT
{
- static function method M(a:int, b:int) : int
- ensures M(a,b) == a + b;
- {
- a + b
- }
+ static function method M(a:int, b:int) : int
+ ensures M(a,b) == a + b;
+ {
+ a + b
+ }
}
class CC extends TT
{
- method Testing(a:int,b:int)
- {
- assert (TT.M(a,b) == a + b);
- }
+ method Testing(a:int,b:int)
+ {
+ assert (TT.M(a,b) == a + b);
+ }
}
trait T4
{
- 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;
- }
+ 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 C4 extends T4
{
- function method F(y: int): int
- {
- 200
- }
+ function method F(y: int): int
+ {
+ 200
+ }
- method M(kk:int) returns (ksos:int)
- requires kk > (-1);
- ensures ksos > 0;
- {
- ksos:=10;
- }
+ method M(kk:int) returns (ksos:int)
+ requires kk > (-1);
+ ensures ksos > 0;
+ {
+ ksos:=10;
+ }
}
diff --git a/Test/dafny0/Trait/TraitPolymorphism.dfy b/Test/dafny0/Trait/TraitPolymorphism.dfy index b1ee9eea..f53d8346 100644 --- a/Test/dafny0/Trait/TraitPolymorphism.dfy +++ b/Test/dafny0/Trait/TraitPolymorphism.dfy @@ -14,20 +14,20 @@ trait T1 function method Mul (x:int, y:int, z:int) : int
requires x>y;
{
- x * y * z
+ x * y * z
}
//function method BodyLess1() : int
static method GetPhoneNumber (code:int, n:int) returns (z:int)
{
- z := code + n;
+ z := code + n;
}
method TestPhone ()
{
- var num : int;
- num := GetPhoneNumber (10, 30028);
+ var num : int;
+ num := GetPhoneNumber (10, 30028);
}
}
diff --git a/Test/dafny0/Trait/TraitSpecsOverride0.dfy b/Test/dafny0/Trait/TraitSpecsOverride0.dfy index 7e16c630..b4bbd9d8 100644 --- a/Test/dafny0/Trait/TraitSpecsOverride0.dfy +++ b/Test/dafny0/Trait/TraitSpecsOverride0.dfy @@ -4,61 +4,61 @@ trait J
{
- function method F(k:int, y: array<int>): int
- reads y;
- decreases k;
- ensures F(k, y) < 100
-
- 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;
- }
-
- method arrM (y: array<int>, x: int, a: int, b: int) returns (c: int)
- requires a > b;
- requires y != null && y.Length > 0;
- ensures c == a + b;
- modifies y;
- decreases x;
+ function method F(k:int, y: array<int>): int
+ reads y;
+ decreases k;
+ ensures F(k, y) < 100
+
+ 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;
+ }
+
+ method arrM (y: array<int>, x: int, a: int, b: int) returns (c: int)
+ requires a > b;
+ requires y != null && y.Length > 0;
+ ensures c == a + b;
+ modifies y;
+ decreases x;
}
class C extends J
{
- // F's postcondition (true) is too weak, but that won't be detected until verification time
- function method F(kk:int, yy: array<int>): int
- {
- 200
- }
+ // F's postcondition (true) is too weak, but that won't be detected until verification time
+ function method F(kk:int, yy: array<int>): int
+ {
+ 200
+ }
- // M's postcondition (true) is too weak, but that won't be detected until verification time
- method M(kk:int) returns (ksos:int)
- {
- ksos:=10;
- }
+ // M's postcondition (true) is too weak, but that won't be detected until verification time
+ method M(kk:int) returns (ksos:int)
+ {
+ ksos:=10;
+ }
- method arrM (y1: array<int>, x1: int, a1: int, b1: int) returns (c1: int)
- requires a1 > b1;
- requires y1 != null && y1.Length > 0;
- ensures c1 == a1 + b1;
- modifies y1;
- decreases x1;
- {
- y1[0] := a1 + b1;
- c1 := a1 + b1;
- }
+ method arrM (y1: array<int>, x1: int, a1: int, b1: int) returns (c1: int)
+ requires a1 > b1;
+ requires y1 != null && y1.Length > 0;
+ ensures c1 == a1 + b1;
+ modifies y1;
+ decreases x1;
+ {
+ y1[0] := a1 + b1;
+ c1 := a1 + b1;
+ }
}
module BadNonTermination {
diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy b/Test/dafny0/Trait/TraitUsingParentMembers.dfy index dd45d0e6..fb6480a4 100644 --- a/Test/dafny0/Trait/TraitUsingParentMembers.dfy +++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy @@ -4,41 +4,41 @@ trait P1
{
- method N0() {
- var a: array<int>;
- if (a != null && 5 < a.Length) {
- a[5] := 12; // error: violates modifies clause
- }
- }
+ method N0() {
+ var a: array<int>;
+ if (a != null && 5 < a.Length) {
+ a[5] := 12; // error: violates modifies clause
+ }
+ }
- method Mul(x: int, y: int) returns (r: int)
- requires 0 <= x && 0 <= y;
- ensures r == x*y;
- decreases x;
+ method Mul(x: int, y: int) returns (r: int)
+ requires 0 <= x && 0 <= y;
+ ensures r == x*y;
+ decreases x;
}
class C1 extends P1
{
- method Mul(x: int, y: int) returns (r: int)
- requires 0 <= x && 0 <= y;
- ensures r == x*y;
- decreases x;
- {
- if (x == 0) {
- r := 0;
- } else {
- var m := Mul(x-1, y);
- r := m + y;
- }
- }
+ method Mul(x: int, y: int) returns (r: int)
+ requires 0 <= x && 0 <= y;
+ ensures r == x*y;
+ decreases x;
+ {
+ if (x == 0) {
+ r := 0;
+ } else {
+ var m := Mul(x-1, y);
+ r := m + y;
+ }
+ }
- method Testing(arr:array<int>)
- requires arr != null && arr.Length == 2 && arr[0]== 1 && arr[1] == 10;
- {
- N0(); //calling parent trait methods
- var x := 2;
- var y := 5;
- var z := Mul(x,y);
- assert (z == 10);
- }
-}
\ No newline at end of file + method Testing(arr:array<int>)
+ requires arr != null && arr.Length == 2 && arr[0]== 1 && arr[1] == 10;
+ {
+ N0(); //calling parent trait methods
+ var x := 2;
+ var y := 5;
+ var z := Mul(x,y);
+ assert (z == 10);
+ }
+}
diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect index 6849499c..ebda3b9f 100644 --- a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect +++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect @@ -1,4 +1,4 @@ -TraitUsingParentMembers.dfy(10,9): Error: assignment may update an array element not in the enclosing context's modifies clause
+TraitUsingParentMembers.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon5_Then
diff --git a/Test/dafny0/Trait/TraitsMultipleInheritance.dfy b/Test/dafny0/Trait/TraitsMultipleInheritance.dfy index 67acbc67..640d0d8d 100644 --- a/Test/dafny0/Trait/TraitsMultipleInheritance.dfy +++ b/Test/dafny0/Trait/TraitsMultipleInheritance.dfy @@ -2,11 +2,11 @@ // RUN: %diff "%s.expect" "%t"
trait J1{
- var x: int;
+ var x: int;
}
trait J2{
- var y: int;
+ var y: int;
}
class C extends J1, J2{
|