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