正しい仕様のみつけ方 – Alloy – 大村伸一 2005 年 10 月 26 日 目次 1 動機 2 2 複雑な論理 3 3 Alloy って何？ 5 4 文献 7 1 1 動機 プログラムを作ることは簡単だが、ちゃんとしたプログラムを作る

正しい仕様のみつけ方 – Alloy – 大村伸一 2005 年 10 月 26 日 目次 1 動機 2 2 複雑な論理 3 3 Alloy って何？ 5 4 文献 7 1 1 動機 プログラムを作ることは簡単だが、ちゃんとしたプログラムを作ることはとても難しい。「ちゃんとした」 というのは、そのプログラムが、プログラムを作ってくれと依頼した人の求めているものであることを客観的 に示せることや、それがコストや作成期間の点で依頼した人の要求を満たしていること、などと考えたい。 ちゃんとしたプログラムを作ることの前提となるのは必要十分な仕様の存在だ。作成したプログラムの妥当 性を客観的に示すには、曖昧さも矛盾もなく依頼者の意図を明確にかつ不足なくあらわした仕様が不可欠だ。 それがなければ、できあがったプログラムについて何も言うことはできないだろう。*1 それほど重要な仕様について、依頼者の意