While Statement

Jump to bottom Edit New page

zarevucky edited this page Dec 27, 2014 · 3 revisions

while (_guard_) {
    // body
}

Annotations:

while (_guard_)
    invariant all i (_expr_)
    invariant(_expr_)
    loop_bound(_expr_)
{
    // body
}

Semantics/analysis notes

See Loop Analysis