16.2.8 while Statements
- V is definitely assigned after
while (
e)
S iff V is definitely assigned after e when false and V is definitely assigned before every break
statement that may exit the while
statement.
- V is definitely assigned before e iff V is definitely assigned before the
while
statement.
- V is definitely assigned before S iff V is definitely assigned after e when true.