\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 繝ゥ繧、繝ウ迥カ諷九r蛻、螳壹☆繧� : () ==> 縲後Λ繧、繝ウ迥カ諷九� 繝ゥ繧、繝ウ迥カ諷九r蛻、螳壹☆繧�() == cases i蜈峨そ繝ウ繧オ繝シ.鮟堤キ壹Ξ繝吶Ν蛟、繧定ェュ縺ソ蜿悶k(): <鮟帝明蛟、莉・荳�> -> return <鮟�>, <逋ス髢セ蛟、莉・荳�> -> return <逋ス>, others -> return <荳肴�> end pre i蜈峨そ繝ウ繧オ繝シ.鮟堤キ壹Ξ繝吶Ν蛟、繧定ェュ縺ソ蜿悶k() <> nil post cases mk_(i蜈峨そ繝ウ繧オ繝シ.鮟堤キ壹Ξ繝吶Ν蛟、繧定ェュ縺ソ蜿悶k(), RESULT): mk_(<鮟帝明蛟、莉・荳�>, <鮟�>) -> true, mk_(<逋ス髢セ蛟、莉・荳�>, <逋ス>) -> true, mk_(-, <荳肴�>) -> true, others -> false end; -- 繝�せ繝育畑謫堺ス� public 鮟堤キ壹Ξ繝吶Ν繧貞、繧偵そ繝�ヨ縺吶k : 縲悟�繧サ繝ウ繧オ繝シ縲港縲碁サ堤キ壹Ξ繝吶Ν蛟、縲� ==> () 鮟堤キ壹Ξ繝吶Ν繧貞、繧偵そ繝�ヨ縺吶k(a鮟堤キ壹Ξ繝吶Ν蛟、) == i蜈峨そ繝ウ繧オ繝シ.鮟堤キ壹Ξ繝吶Ν繧貞、繧偵そ繝�ヨ縺吶k(a鮟堤キ壹Ξ繝吶Ν蛟、); end 縲後Λ繧、繝ウ逶」隕門宛蠕。縲� \end{vdm_al} \begin{rtinfo} [縲後Λ繧、繝ウ逶」隕門宛蠕。縲江{vdm.tc}[縲後Λ繧、繝ウ逶」隕門宛蠕。縲江 \end{rtinfo}