blob: 4a740bbcf7adc50b59434efd2d72b225f350a8db (
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
|
procedure main(x:int)
{
var A:[int]int;
var i:int;
var b:bool;
var size:int;
call i,b := find(A, size, x);
if(b) {
assert(i > 0 && A[i] == x);
}
return;
}
procedure {:inline 1} find(A:[int]int, size:int, x:int) returns (ret:int, found:bool)
{
var i:int;
var b:bool;
ret := -1;
b := false;
found := b;
i := 0;
while(i < size) {
call b := check(A, i, x);
if(b) {
ret := i;
found := b;
break;
}
}
return;
}
procedure {:inline 3} check (A:[int]int, i:int, c:int) returns (ret:bool)
requires i >= 0;
ensures (old(A[i]) > c) ==> ret == true;
{
if(A[i] == c) {
ret := true;
} else {
ret := false;
}
return;
}
|
