source:
CIVL/examples/loop_invariants/dev/plan@
7569720
| Last change on this file since 7569720 was 2fa0abd, checked in by , 8 years ago | |
|---|---|
|
|
| File size: 177 bytes | |
| Rev | Line | |
|---|---|---|
| [2fa0abd] | 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.
