blob: effedf928aa94ab91ea85b408ec1545958f65986 (
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
|
// Declare a constant 'K' and a function 'f' and postulate that 'K' is
// in the image of 'f'
const K: int;
function f(int) returns (int);
axiom (exists k: int :: f(k) == K);
// This procedure will find a domain value 'k' that 'f' maps to 'K'. It will
// do that by recursively enlarging the range where no such domain value exists.
// Note, Boogie does not prove termination.
procedure Find(a: int, b: int) returns (k: int)
requires a <= b;
requires (forall j: int :: a < j && j < b ==> f(j) != K);
ensures f(k) == K;
{
goto A, B, C; // nondeterministically choose one of these 3 goto targets
A:
assume f(a) == K; // assume we get here only if 'f' maps 'a' to 'K'
k := a;
return;
B:
assume f(b) == K; // assume we get here only if 'f' maps 'b' to 'K'
k := b;
return;
C:
assume f(a) != K && f(b) != K; // neither of the two above
call k := Find(a-1, b+1);
return;
}
// This procedure shows one way to call 'Find'
procedure Main() returns (k: int)
ensures f(k) == K;
{
call k := Find(0, 0);
}
|
