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

types
  public 「電源ボタン状態」 = <ON> | <OFF>;

instance variables
  private i電源ボタン状態 : 「電源ボタン状態」 := <OFF>;

operations
  public 電源ボタンを押す : () ==> ()
  電源ボタンを押す() ==
    if i電源ボタン状態 = <ON> then
      i電源ボタン状態 := <OFF>
    else
      i電源ボタン状態 := <ON>
  post i電源ボタン状態 <> i電源ボタン状態~;
  
  public ボタン状態を得る : () ==> 「電源ボタン状態」
  ボタン状態を得る() == return i電源ボタン状態;


end 「電源ボタン」
\end{vdm_al}

\begin{rtinfo}
  [「電源ボタン」]{vdm.tc}[「電源ボタン」]
\end{rtinfo}