Skip to content

Commit 74525c1

Browse files
SaswatPadhiLong Pham
SaswatPadhi
and
Long Pham
committed
Documentation for decreases clauses
Co-authored-by: Long Pham <[email protected]>
1 parent f0ab57e commit 74525c1

File tree

2 files changed

+184
-6
lines changed

2 files changed

+184
-6
lines changed

‎doc/cprover-manual/contracts-decreases.md

Lines changed: 178 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,179 @@
1-
# Decreases Clause
1+
# Decreases Clauses
22

3-
TODO: Document `__CPROVER_decreases`
3+
A _decreases_ clause specifies a measure that must strictly decrease at every iteration of a loop.
4+
By demonstrating that the measure
5+
1. is bounded from below, and
6+
2. strictly decreases at each iteration,
7+
we can prove termination of loops.
8+
This is because the measure must eventually hit the lower bound
9+
at which point the loop must terminate,
10+
since the measure cannot strictly decrease further.
11+
12+
### Syntax
13+
14+
A one-dimensional (1D) decreases clause for a loop is an arithmetic expression `e`
15+
over the variables visible at the same scope as the loop,
16+
specified as `__CPROVER_decreases(e)`.
17+
18+
Like invariant clauses, decreases clauses may be specified just after the loop guard.
19+
An example of a 1D decreases clause is shown below.
20+
21+
```c
22+
for(int i = 0; i < n; i += 2)
23+
__CPROVER_loop_invariant(0 <= i && i <= n)
24+
__CPROVER_decreases(n - i)
25+
{ ... }
26+
```
27+
28+
Please see the [invariant clauses](contracts-invariants.md) page
29+
for more examples on `for` and `do...while` loops.
30+
31+
To help prove termination of more complex loops,
32+
CBMC also supports multi-dimensional decreases clauses.
33+
A multi-dimensional decreases clause is an [ordered tuple](https://en.wikipedia.org/wiki/Tuple)
34+
of arithmetic expressions, specified as `__CPROVER_decreases(e_1, e_2, ..., e_n)`.
35+
An example of a multi-dimensional decreases clause is given below.
36+
37+
```c
38+
while(i < n)
39+
__CPROVER_loop_invariant(0 <= i && i <= n)
40+
__CPROVER_loop_invariant(0 <= j && j <= n)
41+
__CPROVER_decreases(n - i, n - j)
42+
{
43+
if (j < n)
44+
j++;
45+
else
46+
{
47+
i++;
48+
j = 0;
49+
}
50+
}
51+
```
52+
53+
We extend the strict arithmetic comparison for 1D decreases clauses
54+
to a strict [lexicographic comparison](https://en.wikipedia.org/wiki/Lexicographic_order)
55+
for multi-dimensional decreases clauses.
56+
57+
**Important.**
58+
Like invariant clauses, decreases clauses must be free of side effects,
59+
for example, mutation of local or global variables.
60+
Otherwise, CBMC raises an error message during compilation:
61+
```
62+
Decreases clause is not side-effect free. (at: file main.c line 4 function main)
63+
```
64+
65+
### Semantics
66+
67+
A decreases clause extends the loop abstraction introduced in the [invariants clause](contracts-invariants.md) document.
68+
In addition to the inductiveness check asserted at the end of a single arbitrary iteration,
69+
CBMC would also assert the strict decrement of the measure specified in the decreases clause.
70+
At a high level, in addition to the assumptions and assertions introduced by the invariant clause,
71+
a decreases clause expands to three key steps:
72+
1. At the beginning of the loop body, record the initial value of the measure specified in the decreases clause.
73+
2. At the end of the loop body, record the final value of the measure specified in the decreases clause.
74+
3. After the loop iteration, assert that the final value is strictly smaller than the initial one.
75+
76+
For a 1D decreases clause, we use the strict arithmetic comparison (i.e., `<`).
77+
For a multi-dimensional decreases clause, say `(e_1, ..., e_n)`,
78+
we extend the strict arithmetic comparison to a strict lexicographic comparison.
79+
Formally, given two evaluations `(a_1, ..., a_n)` and `(b_1, ..., b_n)`,
80+
a strict lexicographic comparison, denoted by `(a_1, ..., a_n) ≺ (b_1, ..., b_n)`,
81+
is defined as the predicate:
82+
83+
```c
84+
(a_1 < b_1)
85+
|| (a_1 == b_1 && a_2 < b_2)
86+
|| ...
87+
|| (a_1 == b_1 && ... && a_n < b_n)
88+
```
89+
90+
where `||` and `&&` are Boolean disjunction and conjunction respectively.
91+
92+
As an example, consider our binary search implementation again,
93+
this time with a decreases clause annotation to prove its termination:
94+
95+
```c
96+
int binary_search(int val, int *buf, int size)
97+
{
98+
if(size <= 0 || buf == NULL) return NOT_FOUND;
99+
100+
long lb = 0, ub = size - 1;
101+
long mid = (lb + ub) / 2;
102+
103+
while(lb <= ub)
104+
__CPROVER_loop_invariant(0L <= lb && lb - 1L <= ub && ub < size)
105+
__CPROVER_loop_invariant(mid == (lb + ub) / 2L)
106+
__CPROVER_decreases(ub - lb)
107+
{
108+
if(buf[mid] == val) break;
109+
if(buf[mid] < val)
110+
lb = mid + 1;
111+
else
112+
ub = mid - 1;
113+
mid = (lb + ub) / 2;
114+
}
115+
return lb > ub ? NOT_FOUND : mid;
116+
}
117+
```
118+
119+
The instrumented GOTO program is conceptually similar to the following high-level C program:
120+
121+
```c
122+
int binary_search(int val, int *buf, int size)
123+
{
124+
if(size <= 0 || buf == NULL) return NOT_FOUND;
125+
126+
long lb = 0, ub = size - 1;
127+
long mid = (lb + ub) / 2;
128+
129+
/* 1. assert invariant at loop entry */
130+
assert(0L <= lb && lb - 1L <= ub && ub < size);
131+
assert(mid == (lb + ub) / 2L);
132+
133+
/* 2. create a non-deterministic state for modified variables */
134+
havoc(lb, ub, mid);
135+
136+
/* 3. establish invariant to model state at an arbitrary iteration */
137+
__CPROVER_assume(0L <= lb && lb - 1L <= ub && ub < size)
138+
__CPROVER_assume(mid == (lb + ub) / 2L)
139+
140+
/* 4. perform a single arbitrary iteration (or exit the loop) */
141+
if(lb <= ub)
142+
{
143+
/* 5. declare variables for tracking the loop variant */
144+
int old_measure, new_measure;
145+
146+
/* 6. evaluate the variant at the start of the loop body */
147+
old_measure = ub - lb;
148+
149+
if(buf[mid] == val) break;
150+
if(buf[mid] < val)
151+
lb = mid + 1;
152+
else
153+
ub = mid - 1;
154+
mid = (lb + ub) / 2;
155+
156+
/* 7. assert the invariant to establish inductiveness */
157+
assert(0L <= lb && lb - 1L <= ub && ub < size);
158+
assert(mid == (lb + ub) / 2L);
159+
160+
/* 8. evaluate the variant at the end of the loop body */
161+
new_measure = ub - lb;
162+
163+
/* 9. assert the decreases clause */
164+
assert(new_measure < old_measure);
165+
166+
/* 10. terminate this symbolic execution path; similar to "exit" */
167+
__CPROVER_assume(false);
168+
}
169+
return lb > ub ? NOT_FOUND : mid;
170+
}
171+
```
172+
173+
The instrumented code points (5), (6), (8), and (9) are specific to the decreases clause.
174+
175+
**Important.**
176+
Decreases clauses work in conjunction with [loop invariants](contract-invariants.md),
177+
which model an arbitrary loop iteration at which the decreases clause is checked.
178+
If a decreases clause is annotated on a loop without an invariant clause,
179+
then the weakest possible invariant (i.e, `true`) is used to model an arbitrary iteration.

‎doc/cprover-manual/contracts-invariant.md renamed to ‎doc/cprover-manual/contracts-invariants.md

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
# Invariant Clause
1+
# Invariant Clauses
22

33
An _invariant_ clause specifies a property that must be preserved
44
by every iteration of a loop.
@@ -46,11 +46,14 @@ __CPROVER_loop_invariant(i <= n);
4646

4747
**Important.** Invariant clauses must be free of _side effects_,
4848
for example, mutation of local or global variables.
49-
49+
Otherwise, CBMC raises an error message during compilation:
50+
```
51+
Loop invariant is not side-effect free. (at: file main.c line 4 function main)
52+
```
5053

5154
### Semantics
5255

53-
The loop invariant clause expands to several assumptions and assertions:
56+
A loop invariant clause expands to several assumptions and assertions:
5457
1. The invariant is _asserted_ just before the first iteration.
5558
2. The invariant is _assumed_ on a non-deterministic state to model a non-deterministic iteration.
5659
3. The invariant is finally _asserted_ again to establish its inductiveness.
@@ -77,7 +80,6 @@ int binary_search(int val, int *buf, int size)
7780
while(lb <= ub)
7881
__CPROVER_loop_invariant(0L <= lb && lb - 1L <= ub && ub < size)
7982
__CPROVER_loop_invariant(mid == (lb + ub) / 2L)
80-
__CPROVER_decreases(ub - lb)
8183
{
8284
if(buf[mid] == val) break;
8385
if(buf[mid] < val)

0 commit comments

Comments
 (0)