変わるものと変わらぬものがある。
ソフトウェアの開発現場での開発手法は、ここ20数年、大きく変わってきた。昔は構造化プログラミングで、そのあと設計工程まで視野に入れた複合設計になり、構造化設計や構造化分析が後に続いた。そして、今はオブジェクト指向分析・設計・プログラミングである。もちろん、これらの間には、抽象データ型や情報隠蔽といった一貫した考え方が背景にはあるのだが、手法そのものあるいは記法から見ると、かなり変化していて、開発現場のソフトウェア技術者を惑わしている。
一方、変わらぬものがある。形式手法(Formal Method)である。20年以上前から、数学をベースにソフトウェアを開発すべきだとして、この手法は発展してきた。20年ほど前から、この手法に対して「数学など現実のシステムには役立たない」と言う反論があった。しかし、今や反形式手法論は根拠を失った。形式手法は完全な実用域に達していて、現実のシステム開発に使われていて、効果が証明されているからである。
そもそも、「数学など現実のシステムには役立たない」というのがおかしい。なぜなら、「プログラムは数学である」から「プログラムなど現実のシステムには役立たない」ということになるからである。
現在の商用プログラミング言語の場合、作成したプログラムは良い性質を持った数学系にはならないのだが、数学系には違いない。従って、プログラムを作るまでのどこかの工程で、「数学で記述できない」現実の世界をモデル化して「数学系として記述する」ことが必要になる。現在は、これをプログラミング工程で行っている。
これで良いのだろうか?良くないことは明らかだろう。日本のソフトウェアはもはや公害源となった。2000年問題なるソフトウェアの一連の欠陥も、そのひとつの現象にすぎない。このままでは、ソフトウェアを原因とした大惨事が起こるであろう。
形式手法は、数学系への変換を要求分析工程から行うことを主張する。これができれば、プログラミング工程まではすでに発見された3000近い変換規則を用いる「段階的洗練」によって、従来の手法よりかなり正確にプログラムに変換していくことができる。また、この過程の一部を証明することも可能となっていて、高信頼性ソフトウェアを作成するのに適した手法となっている。手法を支援するツール群も、すでにB-Toolkit, CafeOBJ, RAISE Tool, VDMToolsなどが提供されていて、欧州や米国では大規模なシステムの構築にも供されている。
では、なぜ日本では普及していないか?
理由は単純である。日本語の良い教科書が非常に少ない、形式手法を教えている大学が少ない、その結果として、形式手法を理解する人が少ない、産業界に普及していない、というだけのことである。いわば、10年前のオブジェクト指向技術、15年前のUNIXと同じ状態なのである。
であるならば、今、やるべきことはっきりしている。
ソフトウェア大惨事が起こりうる事態となっていることを社会に警告し、高信頼性ソフトウェア作成を当然のこととする姿勢を社会に浸透させ、日本語の良い教科書を作成し、形式手法を教える場を増やし、形式手法を理解する人間を増やさなければならない。
このような目的のために、ソフトウェア技術者協会(SEA)の中に、sigfm (Special Interest Group on Formal Method)を作ることを提案する。
sigfmは、上記目的に添って以下の活動を行う。
なお、古来より、日本ではこのような活動に酒肴が付き物であるが、sigfmもこの伝統を守る。
佐原伸 2000年3月3日