blob: 614adc2d4b06033283cfc97b2999ac92341f00b8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
// 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;
}
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
{
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;
}
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;
}
}
|
