While

if $\alpha$ is a test and $P$ a piece of code (both on $X$), then while$(\alpha)\;\{P\}$ is a piece of code. We call $P$ the ``body of the loop''. Given input state $x$, the output is obtained by applying $P$ until $\alpha$ is no longer satisfied, the answer is the value of $x$ at the point where this occurs (which may be immediately!)

Note: while$(\alpha)\;\{P\}$ may not terminate for some input states: The ``exit condition'' $\lnot \alpha$ may never be achieved