diff options
| author |  Reza Ahmadi <reza.ahmadi@uta.fi> | 2014-07-31 17:48:42 +0300 |
|---|---|---|
| committer | Reza Ahmadi <reza.ahmadi@uta.fi> | 2014-07-31 17:48:42 +0300 |
| commit | a5be808ee60f37b3e74e03660eab66c95154083e (patch) | |
| tree | eb3c3fe1bb400d3f877d67e084d2322365b5b05d /Test/dafny0/Trait | |
| parent | 47de1c8add4f4ac5c390a96bbd8d2e5acaf87540 (diff) | |
added one more test case
Diffstat (limited to 'Test/dafny0/Trait')
| -rw-r--r-- | Test/dafny0/Trait/TraitSpecsOverride0.dfy | 20 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect | 8 |
2 files changed, 23 insertions, 5 deletions
diff --git a/Test/dafny0/Trait/TraitSpecsOverride0.dfy b/Test/dafny0/Trait/TraitSpecsOverride0.dfy index 5b4417c3..614adc2d 100644 --- a/Test/dafny0/Trait/TraitSpecsOverride0.dfy +++ b/Test/dafny0/Trait/TraitSpecsOverride0.dfy @@ -25,6 +25,13 @@ trait J 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
@@ -37,5 +44,16 @@ class C extends J method M(kk:int) returns (ksos:int) //errors here, M must provide its own specifications
{
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;
+ }
}
\ No newline at end of file diff --git a/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect b/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect index cbdcdf05..750e13e0 100644 --- a/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect +++ b/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect @@ -1,5 +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
+TraitSpecsOverride0.dfy(39,17): Error: Function must provide its own Reads clauses anew
+TraitSpecsOverride0.dfy(39,17): Error: Function must provide its own Decreases clauses anew
+TraitSpecsOverride0.dfy(44,8): Error: Method must provide its own Requires clauses anew
+TraitSpecsOverride0.dfy(44,8): Error: Method must provide its own Ensures clauses anew
4 resolution/type errors detected in TraitSpecsOverride0.dfy
|