blob: b4bbd9d854af177873f09fd63e33e633444f3895 (
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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
// 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;
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
}
// 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;
}
}
module BadNonTermination {
trait TT1 {
method N(x: int)
decreases x
}
class CC1 extends TT1 {
method N(x: int)
decreases * // error: can't override a terminating method with a possibly non-terminating method
{ }
}
}
|
