source:
CIVL/examples/languageFeatures/sumExpression.cvl@
367a390
| Last change on this file since 367a390 was b3cd4ba, checked in by , 3 months ago | |
|---|---|
|
|
| File size: 223 bytes | |
| Rev | Line | |
|---|---|---|
| [bd7a43e] | 1 | $input int N; |
| 2 | $assume(N > 0 && N <= 10); | |
| 3 | $input int a[N]; | |
| 4 | ||
| 5 | int main() { | |
| 6 | int sum = 0; | |
| 7 | for (int i = 0; i < N; i++) { | |
| [b3cd4ba] | 8 | sum += a[i] + 1; |
| [bd7a43e] | 9 | } |
| [b3cd4ba] | 10 | $assert(sum == $sum(int t : 0 .. N-1) a[t] + 1); |
| [bd7a43e] | 11 | return 0; |
| 12 | } |
Note:
See TracBrowser
for help on using the repository browser.
