source: CIVL/examples/loop_invariants/dev/plan@ 397ae5f

main test-branch
Last change on this file since 397ae5f was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago

Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@5704 fb995dde-84ed-4084-dfe6-e5aef3e2452c

  • Property mode set to 100644
File size: 177 bytes
Line 
1loop init;
2assert( invari );
3if (cond)
4 while(true) {
5 assume_push(cond && invari);
6 body;
7 increment;
8 assert
9 havoc
10 if (!cond) break;
11 assume_pop();
12 }
Note: See TracBrowser for help on using the repository browser.