\def\COMMENT#1{\{\parbox[t]{\codewidth}{\rm #1\}}}
\def\ASSERT#1{\{\mbox{\rm #1}\}}
\def\PROGRAM{{\bf pro}\tab{\bf gram\ }}
\def\ENDPROGRAM{\untab{\bf end}}
\def\USES{{\bf uses\ }\tab}
\def\ENDUSES{\untab{\bf end}}
\def\MODULE{{\bf mod}\tab{\bf ule\ }}
\def\ENDMODULE{\untab{\bf end}}
\def\SPECIFICATION{{\bf spe}\tab{\bf cification\ }}
\def\ENDSPECIFICATION{\untab{\bf end}}
\def\IMPLEMENTATION{{\bf imp}\tab{\bf lementation\ }}
\def\ENDIMPLEMENTATION{\untab{\bf end}}
\def\IMPORT{{\bf imp}\tab{\bf orts\ }}
\def\ENDIMPORT{\untab{\bf end}}
\def\TYPE{{\bf type\ }\tab}
\def\ENDTYPE{\untab}
\def\VAR{{\bf var\ }\tab}
\def\ENDVAR{\untab}
\def\CONST{{\bf const\ }\tab}
\def\ENDCONST{\untab}
\def\ARRAY{{\bf array\ }}
\def\RECORD{\tab{\bf rec}\tab{\bf ord\ }}
\def\ENDRECORD{\untab{\bf end}$\-$}
\def\BEGIN{}
\def\IF{{\bf if }\tab\ \ \tab}
\def\ELSE{\untab\untab [\!]$\>$}
\def\ENDIF{\untab\untab {\bf fi}}
\def\THEN{\ \longrightarrow\ \ \tab}
\def\SKIP{\emptyset}
\def\WHILE{{\bf whi}\tab{\bf le\ }}
\def\ENDWHILE{\untab{\bf end}}
\def\DO{{\bf\ do\ }}
\def\DDO{{\bf do\ }\tab}
\def\ENDDO{\untab{\bf end}}
\def\FORALL{{\bf for}\tab{\bf\ all\ }}
\def\FOR{{\bf for}\tab\ }
\def\ENDFOR{\untab{\bf end}}
\def\ENDFORALL{\untab{\bf end}}
\def\PARALLEL{{\bf\ parallel\ }}
\def\REPEAT{{\bf rep}\tab{\bf eat\ }}
\def\UNTIL{\untab{\bf until\ }}
\def\AND{\mathbin{\hbox{\bf and}}}
\def\OR{\mathbin{\hbox{\bf or}}}
\def\NOT{\mathop{\hbox{\bf not}}}
\def\CAT{\mathbin{\&}}
\def\OF{{\bf\ of\ }}
\def\IN{{\bf\ in\ }}
\def\DIV{\mathbin{\hbox{\bf div}}}
\def\MOD{\mathbin{\hbox{\bf mod}}}
\def\PROCEDURE{{\bf pro}\tab{\bf cedure\ }}
\def\ENDPROCEDURE{\untab{\bf end}}
\def\FUNCTION{{\bf fun}\tab{\bf ction\ }}
\def\ENDFUNCTION{\untab{\bf end}}
\def\RETURNS{{\bf return\ }}
\def\INP{{\bf in\ }}
\def\OUTP{{\bf out\ }}
\def\INOUTP{{\bf in/out\ }}
\def\PRIVATE{{\bf private\ }}