VDMでハノイの搭

/*
インドのガンジス河の畔のヴァラナシ（ベナレス）に、世界の中心を表すという
巨大な寺院がある。
そこには青銅の板の上に、長さ1キュビット、太さが蜂の体ほどの3本のダイヤモンドの
針が立てられている。そのうちの1本には、天地創造のときに神が64枚の純金の円盤を
大きい円盤から順に重ねて置いた。
これが「ブラフマーの塔」である。
司祭たちはそこで、昼夜を通して円盤を別の柱に移し替えている。
そして、全ての円盤の移し替えが終わったときに、世界は崩壊し終焉を迎える。
引用：http://ja.wikipedia.org/wiki/ハノイの塔
*/
class ハノイの搭

instance variables
io:IO := new IO();

operations
public ハノイの搭を解く: token*token*token*nat1 ==> ()
ハノイの搭を解く(移動元の柱, 移動先の柱, 空きの柱, 動かす枚数) ==
	if 動かす枚数 = 1 then
		一枚の円盤を移動(移動元の柱, 移動先の柱)
	else (
		ハノイの搭を解く(移動元の柱, 空きの柱, 移動先の柱, 動かす枚数-1);
		一枚の円盤を移動(移動元の柱, 移動先の柱);
		ハノイの搭を解く(空きの柱, 移動先の柱, 移動元の柱, 動かす枚数-1);
	);

private 一枚の円盤を移動:token*token==> ()
一枚の円盤を移動(移動元の柱, 移動先の柱) == 
	def - = io.writeval[token*token](mk_(移動元の柱,移動先の柱)) in skip;


public play:nat ==> ()
play(n) ==
	ハノイの搭を解く(mk_token("移動元の柱"), mk_token("移動先の柱"), mk_token("空きの柱"), n);

-- この操作は呼ばないほうが良い。
-- この操作が終わるとき、世界は崩壊し、終焉を迎えるであろう。
-- その前にVDMToolsがハングする。
public theEndOfTheWorld:() ==> ()
theEndOfTheWorld() ==
	play(64);

end ハノイの搭
/*
cr h := new ハノイの搭()
p h.play(3);
*/