source: CIVL/mods/dev.civl.com/examples/arrayLambda/arrayLambda3.cvl@ bc0fbae

main test-branch
Last change on this file since bc0fbae was aad342c, checked in by Stephen Siegel <siegel@…>, 3 years ago

Performing huge refactor to incorporate ABC, GMC, and SARL into CIVL repo and use Java modules.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5664 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 298 bytes
Line 
1$input int n;
2$assume(n > 0);
3
4int b[2 * n];
5
6int 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.