While loop
= While loop
A while loop tests a Boolean condition before each iteration and repeats its body while that condition is true. A <loop invariant> is established initially and preserved by every iteration; a <loop variant> decreases in a well-founded order to prove <algorithm termination>. The invariant together with the false exit guard establishes the <postcondition>.