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 /Test/dafny0/Trait/TraitExtend.dfy | |
| parent | 098607bcd7deade4835c35111a80b0af5de4151c (diff) | |
Whitespace deltas in test files (in particular, removing tabs and adjusting some indentation)
Diffstat (limited to 'Test/dafny0/Trait/TraitExtend.dfy')
| -rw-r--r-- | Test/dafny0/Trait/TraitExtend.dfy | 56 |
1 files changed, 28 insertions, 28 deletions
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 |