第2回論理的な仕様を記述するために抽象機械を作成する

摘要

ソフトウェアの大規模化につれ,仕様通りの製品ができない,バグが複雑化する,そもそも仕様段階でおかしいことが製品になって から発覚したなどということが頻発しています.そこで,仕様段階から論理的に「正しい」ことを保証し,それを次第にコードへと落 としていく形式手法が注目を集めています.今回は,インターフエース仕様を記述するための「抽象機械」について解説します.