-
Notifications
You must be signed in to change notification settings - Fork 2
/
findmin.ucl
44 lines (39 loc) · 849 Bytes
/
findmin.ucl
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
module main
{
// array we will be searching in.
const arr : [integer]integer;
// size of array.
const n : integer;
// loop index.
var i : integer;
// was the value found?
var min : integer;
// has the search finished
var done : boolean;
init {
assume (n > 0);
i = 0;
done = false;
min = arr[0];
}
next {
if (i < n) {
if (arr[i] < min) {
min' = arr[i];
}
i' = i + 1;
done' = (i' == n);
}
}
// TODO: add invariants to prove property.
invariant min_final:
(done) ==> (forall (j : integer) :: (j >= 0 && j < n) ==> min <= arr[j]);
invariant min_final_exists:
(done) ==> (exists (j : integer) :: j >= 0 && j < n && arr[j] == min);
control {
v = induction;
check;
print_results;
v.print_cex(i, n, arr[i], min, done);
}
}