An Example

Program division
   declare $x,y,z,k$: integer
   initially $x,y,z,k\; =\; 0,M,N,1$
   assign
      $z,k$ :=
            $2*z$, $2*k$ if $y$ $>=$ $2*z$ ~
            $N,1$ if
   [] $x,y$ := $x+k,\; y-z$ if $y$ $>=$ $z$
end {division}

• Specification
  • $x*N+y\; =\; M$ and $0$ holds in fixed point.
  • fixed point is reached eventually.