\begin{vdm_al} -- -- THIS FILE IS AUTOMATICALLY GENERATED!! -- -- Generated at 10-Nov-08 by the UML-VDM++ Link -- class 「ライン監視制御」 types public 「ライン状態」 = <黒> | <白> | <不明>; instance variables private iライン状態 : 「ライン状態」; private i光センサー : 「光センサー」; operations public 「ライン監視制御」 : () ==> 「ライン監視制御」 「ライン監視制御」() == i光センサー := new 「光センサー」(); public ライン状態を判定する : () ==> 「ライン状態」 ライン状態を判定する() == cases i光センサー.黒線レベル値を読み取る(): <黒閾値以下> -> return <黒>, <白閾値以上> -> return <白>, others -> return <不明> end pre i光センサー.黒線レベル値を読み取る() <> nil post cases mk_(i光センサー.黒線レベル値を読み取る(), RESULT): mk_(<黒閾値以下>, <黒>) -> true, mk_(<白閾値以上>, <白>) -> true, mk_(-, <不明>) -> true, others -> false end; -- テスト用操作 public 黒線レベルを値をセットする : 「光センサー」`「黒線レベル値」 ==> () 黒線レベルを値をセットする(a黒線レベル値) == i光センサー.黒線レベルを値をセットする(a黒線レベル値); end 「ライン監視制御」 \end{vdm_al} \begin{rtinfo} [「ライン監視制御」]{vdm.tc}[「ライン監視制御」] \end{rtinfo}