source:
CIVL/mods/dev.civl.com/examples/arrayLambda/arrayLambda3.cvl@
cb4d4f4
| Last change on this file since cb4d4f4 was aad342c, checked in by , 3 years ago | |
|---|---|
|
|
| File size: 298 bytes | |
| Rev | Line | |
|---|---|---|
| [8760ca1] | 1 | $input int n; |
| 2 | $assume(n > 0); | |
| 3 | ||
| 4 | int b[2 * n]; | |
| 5 | ||
| 6 | int main() { | |
| 7 | int a[n] = (int[n])$lambda(int i) 1; | |
| 8 | ||
| 9 | b = (int[2*n])$lambda(int i)(i%2==0 ? a[i/2] : b[i]); | |
| 10 | $assert($forall (int i | 0 <= i && i < 2*n && i%2 == 0) b[i] == 1); | |
| 11 | $assert($forall (int i | 0 <= i && i < 2*n && i%2 != 0) b[i] == 0); | |
| 12 | } |
Note:
See TracBrowser
for help on using the repository browser.
