\begin{vdm_al}
--
-- THIS FILE IS AUTOMATICALLY GENERATED!!
--
-- Generated at 10-Nov-08 by the UML-VDM++ Link
--
class 「モーター」

instance variables
  private iモーター状態 : token := mk_token(0);

operations
  public 停止する : () ==> ()
  停止する() ==
    iモーター状態 := mk_token(0)
  post iモーター状態 = mk_token(0);

  public 回転する : token ==> ()
  回転する(a回転速度) ==
    iモーター状態 := mk_token(a回転速度)
  -- この事前条件はVDM記述時に追加した
  pre a回転速度 <> mk_token(0)
  post iモーター状態 <> mk_token(0);

end 「モーター」
\end{vdm_al}

\begin{rtinfo}
  [「モーター」]{vdm.tc}[「モーター」]
\end{rtinfo}