source:
CIVL/examples/focus/simpleFocusOrdered.cvl
| Last change on this file was 6d5b8a3, checked in by , 8 months ago | |
|---|---|
|
|
| File size: 321 bytes | |
| Rev | Line | |
|---|---|---|
| [6d5b8a3] | 1 | #pragma CIVL ACSL |
| 2 | $input int N; | |
| 3 | $assume(0 < N); | |
| 4 | int a[N]; | |
| 5 | ||
| 6 | int main() { | |
| 7 | /*@ loop assigns a[0..N-1]; | |
| 8 | @ focus F+{0..1} | a[F..F+1]; | |
| 9 | @*/ | |
| 10 | for (int i = 0; i < N; i++) { | |
| 11 | a[i] = i; | |
| 12 | } | |
| 13 | ||
| 14 | //@ focus ordered(<, F : 0..N-1 | a[F]); | |
| 15 | ||
| 16 | //@ focus F; | |
| 17 | $assert($forall(int i:1..N-2) a[0] < a[i] && a[i] < a[N-1]); | |
| 18 | } |
Note:
See TracBrowser
for help on using the repository browser.
