Alloy

ヤギ、キャベツ、狼

前回に続いて、抽象によるソフトウェア設計−Alloyではじめる形式手法− の練習問題を考える。 A.3.5 「ヤギ、キャベツ、狼」一人の農夫が、一頭のヤギと、一玉のキャベツと、一匹の狼を川の向こう側に運びたい。しかし彼のボートには一度に一つしか載せるスペ…

驚くような三段論法

「抽象によるソフトウェア設計」を読んだ。 内容が難しい上にAlloyの記述形式に馴染めないので、読むのに時間が掛かった。 説明のための例としてアドレス帳を取り上げているのだが、アドレス帳の仕様記述には何の興味も湧かないので退屈だった。説明する側か…