source:
CIVL/examples/loop_invariants/dev/plan@
deb6be2
| Last change on this file since deb6be2 was 9a23317, checked in by , 9 years ago | |
|---|---|
|
|
| File size: 177 bytes | |
| Rev | Line | |
|---|---|---|
| [9a23317] | 1 | loop init; |
| 2 | assert( invari ); | |
| 3 | if (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.
