source: CIVL/mods/dev.civl.com/examples/arrayLambda/arrayLambda2.cvl@ cb4d4f4

main test-branch
Last change on this file since cb4d4f4 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: 401 bytes
Line 
1$input int n;
2$assume(n > 0);
3
4int b[3*n][3*n];
5
6int main() {
7 int a[n][n] = (int[n][n])$lambda(int i,j) i*n+j;
8
9 b = (int[3*n][3*n])$lambda(int i,j) n<=i&&i<2*n&&n<=j&&j<2*n ? a[i-n][j-n] : b[i][j];
10 $assert($forall (int i:n..2*n-1) $forall (int j:n..2*n-1) b[i][j] == a[i-n][j-n]);
11 $assert($forall (int i, j | (0<=i&&i<n) || (2*n<=i&&i<3*n) || (0<=j&&j<n) || (2*n<=j&&j<3*n)) b[i][j] == 0);
12}
Note: See TracBrowser for help on using the repository browser.