\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鮟堤キ壹Ξ繝吶Ν蛟、 : [縲碁サ堤キ壹Ξ繝吶Ν蛟、縲江 := nil; operations -- 繝ゥ繧、繝ウ逶」隕門宛蠕。繧ッ繝ゥ繧ケ縺ィ驥崎、�@縺ヲ縺�k謫堺ス懊�縺溘a蜑企勁 -- VDM險倩ソー譎ゅ↓菫ョ豁」 /* public 繝ゥ繧、繝ウ迥カ諷九r蛻、螳壹☆繧� : () ==> 繝ゥ繧、繝ウ迥カ諷� 繝ゥ繧、繝ウ迥カ諷九r蛻、螳壹☆繧�() == is not yet specified; */ public 鮟堤キ壹Ξ繝吶Ν蛟、繧定ェュ縺ソ蜿悶k : () ==> [縲碁サ堤キ壹Ξ繝吶Ν蛟、縲江 鮟堤キ壹Ξ繝吶Ν蛟、繧定ェュ縺ソ蜿悶k() == return i鮟堤キ壹Ξ繝吶Ν蛟、; -- 繝�せ繝育畑謫堺ス� public 鮟堤キ壹Ξ繝吶Ν繧貞、繧偵そ繝�ヨ縺吶k : 縲碁サ堤キ壹Ξ繝吶Ν蛟、縲� ==> () 鮟堤キ壹Ξ繝吶Ν繧貞、繧偵そ繝�ヨ縺吶k(a鮟堤キ壹Ξ繝吶Ν蛟、) == i鮟堤キ壹Ξ繝吶Ν蛟、 := a鮟堤キ壹Ξ繝吶Ν蛟、; end 縲悟�繧サ繝ウ繧オ繝シ縲� \end{vdm_al} \begin{rtinfo} [縲悟�繧サ繝ウ繧オ繝シ縲江{vdm.tc}[縲悟�繧サ繝ウ繧オ繝シ縲江 \end{rtinfo}