Example

Let P = `` while$(x\geq1)\;\{x := x + 1\}$''. If the input is $x\geq1$ then $x$ is increased each time the body of the loop is applied so the exit condition $\lnot(x \geq 1) \Leftrightarrow (x < 1)$ is never satisfied. For example, if $x=1$ initially, then the vector $(1)$ evolves as follows:

$$(1),(2),(3),(4),...$$

and does not stop. So $P$ is not defined when $x\geq1$. For $x < 1$, the entry condition is never satisfied so the output is $x$: $(x),(x)$