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.
New to topics? Read the docs here!