diff options
Diffstat (limited to 'Test/dafny0/Trait/TraitUsingParentMembers.dfy')
| -rw-r--r-- | Test/dafny0/Trait/TraitUsingParentMembers.dfy | 64 |
1 files changed, 32 insertions, 32 deletions
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);
+ }
+}
|