\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}