★★★☆☆ "プログラム仕様記述論"

「最近知った技術だが、歴史は古いそうな。」

• "プログラム仕様記述論"

プログラムの正しさと云うのはなかなか難しい問題だ。「言われた通りに作りました。」「仕様書に書いてある通りに作りました。」と言ったところで、それが事実かどうかは分からないし、仕様書の記述が曖昧なことも少なくない。そこで、厳密な仕様記述と、その記述に沿った振る舞いであることを保証する仕掛けとなるのが、形式手法と呼ばれるもので、何十年も前から存在するものだそうな。

学術的には面白いと思うだが、長い歴史の割に一般に普及していないばかりか、あまり認知もされていない現実から考えて、今後も大ブレイクする可能性は低そうだ。ただ、正しいとは何か、厳密な記述と、漏れのない仕様がどういものなのかを認知できることは必要なので、教養として一読されことは決して無駄にはならないだろう。

プログラム仕様記述論 (IT Text)