IF Note

and, in general, a note on conditional assignment notation

   [IF] = 

      [ if R >= Y then Q := Q+1 ; R := R-Y endif ] =

      ( R >= Y --> Q,R := Q+1,R-Y ) | ( R < Y --> ident )

The second clause is important... don't leave it out... AND, don't get confused. An alternate to write the function [IF] is

    ( R >= Y --> Q,R := Q+1,R-Y ) | ( )

If you choose this notation, don't forget that the second clause is not the identity function. It is the identity function restricted to domain elements where ( R < Y ). If you forget, and treat it as identity, your trace tables will get fouled up.