形式手法 - 正しいソフトウェアを書くために
ニュースとかでは, オープンソースについて次のように説明しています.
ソフトウェアの設計書であるソースコードを公開し・・・・・
世間では「ソースコード＝設計書」なのですが, ソースコードだけではシステムの概要が分からないので, ソースコードとは別に設計書という名目でソフトウェアの概要を説明した資料が求められます. ただ, この設計書の作成は掛けた時間の割に成果が乏しいと感じています.
通常はソースコードを書く前に設計書を作成しますが, 時間を掛けてもろくな文書になりません. 書いている時はこれで完璧とばかりに自信満々なのですが, 実装を始めると誤り, 矛盾, 検討不足が次々と現れます.
このようなことになる理由は, 設計書の記述内容を検証する仕組みが無いためです. 日本語で書くドキュメントですから, 書き手が意図しない文章の多義性があったり, 暗黙の前提が読み手に欠けていたり, 同じ言葉でも人によって定義が微妙にずれていたりします. このような誤りは, 実装を始めないと表面化しません.
その解決策として形式手法を導入しようと勉強を始めています.
一般に, 形式手法ではソフトウェアの仕様を論理学と述語論理を用いて記述します. 数式を用いて仕様を記述するので, 矛盾点などをプログラムを使って検証できます.
形式手法にもいろいろとあり, VDM(Vienna Development Method)が有名です. VDMは1960年代から70年代にかけて, IBMのウィーン研究所で開発された手法です. 50年前から仕様記述が問題になっていたのです.
最近, 形式手法を調べていてTLA+を見つけました. TLA+はAWSの開発チームが採用しており効果を発揮しているようです.
AWSの開発チームから論文が出ているので, これを読み解くところから始めます. 論文はこちらです.
私は英語が得意ではありませんので, 英語の勉強を兼ねますので進捗は遅くなりそうです.