In this note we prove that the weakest liberal precondition of a
  while-loop is equal to the greatest fixpoint of the -- well known --
  function that iterates the weakest liberal precondition of the
  loop's body in the same way the loop itself iterates its body.  The
  proof is performed in an operational framework of an abstract
  machine that executes syntactic programs.

  The purpose of this paper is to justify the choice of a loop's
  predicate-transformer-semantics (see [Wolf99a]) from an operational
  point of view.