形式手法入門講座

形式手法（Formal Method）～形式的方法とか単に”フォーマル”とも呼ばれます～が、ここにきて（特に組み込み系領域で）注目を集めています。広く話題に上るようになったのは最近ですが、形式手法の誕生は古く（約30年前）、”ソフトウェアエンジニアリング”とほぼ同じ歴史を持っています。ただこれまでは、数学をベースとしているためか、その使用は高い信頼性を求められる一部のドメインや一部の専門家にとどまって、形式手法自身は継続的に発展し、成果を残してきてはいるものの、広く普及するには至りませんでした。しかし、近年、ソフトウェアに一層の品質・信頼性が求められるようになったこと、あるいはまたそういった対象が増えてきたこと、他方、VDMやSpinといったツールが登場し、成功事例が報告されるようなこともあり、その状況は変化しつつあるようです。

形式手法に関する関心が高まるのはもっともであり、歓迎すべきことですが、一方、問題/困ったことも顕在化してきました。一つはきちんとした教育講座がほとんどないことです。ツールの紹介セミナーや事例紹介セミナー、また専門的な場での報告はあるものの、実践視点で体系的に形式手法を教える講座はほとんどありません。第二はツールを中心としたセミナーの”弊害”です。そこでは必然的にツールによる仕様の実行・検証に力点が置かれますが、現在のツールの限界もあり、結果として”プログラミング言語が数学的言語に変わっただけ”とか”中間言語が増えただけ”といった誤解を与えているようです。

こういった状況を受け、本格的な教育講座をと作ったのが本講座です。我々は、ソフトウェアエンジニアであれば形式手法は勉強すべき or 勉強する価値のあるものと考えています。形式手法は、VDM++やZ++といった名前からも推察できるように、オブジェクト指向と相互補完的です。また形式手法の考え方は、一般の仕様作成でも大いに参考になり、仕様の質を向上させてくれるはずです。そしてなにより形式手法はとても楽しいものです。

形式手法に関心をお持ちの方、豆蔵の講座で形式手法の扉を開けてみませんか！