WHILE STATEMENT

while cond loop S; end loop;

Proof Rule

{I and cond} S {I}
_____________________________________________
{I}while cond loop S;end loop;{I and not cond}

where I is the loop invariant

Example:

{x >= 0}
while x> 0 loop
x := x-1;
end loop;
{x = 0}

where {x >=0} is the loop invariant