豆寄席第18回『形式仕様技術の活用～仕様の位置付けとVDMによる厳密な記述』参加レポート

2022年07月13日イベント報告

北　博文

2022年5月30日に豆寄席第18回として、『形式仕様技術の活用～仕様の位置付けとVDMによる厳密な記述』を開催しました。
本セミナーではデザイナーズデン代表取締役社長の酒匂寛さんにご講演頂きました。
本稿では講演の内容を、豆寄席の参加レポートとしてご紹介します。
VDMについては初心者なのですが、仕様書の書き方や形式的な事、その意味には関心があり、非常に興味深い内容でした。
以下では、いくつかの印象深かったスライドを選んで、わたしの観点になってしまいますが、コメントや自分なりの学びについて書いていきたいと思います。

課題・仕様・設計

まず、形式仕様技術の説明に入る前にそもそも仕様とは何かについてお話しいただきました。酒匂さん曰く、システム開発には3つの視点があります。

利用者の視点、利用者と開発者の視点、開発者の視点の3つ
「課題」は利用者の視点、「仕様」は利用者と開発者の視点、「設計」は開発者の視点が求められます。仕様は課題と設計をつなぐもので、課題をどのように定式化すれば実現するかが書かれています。その実現方法として展開されたのが設計です。
仕様が曖昧であると、問題が発生します。日常生活や日々の仕事でも、例えば誰かに何かをお願いした際に、思っていたことと違うフィードバックが返ってくることがあります。また、何かをお願いされた際に、ふわっとしたお願いを頼まれた。よく確認すると何か違うと思うような機会はよくあると思います。システム開発においてはなおさら、仕様が曖昧であると、利用者と開発者のコミュニケーションの際のさまざまな局面で弊害が起こることは容易に想像がつきます。仕様は必要なレベルで厳密に記述した方が品質の高いシステムが開発できると納得できる解説でした。

さらに、仕様がきちんと存在している事で、課題と設計の間のトレーサビリティが取れます。
課題を通じて、仕様と設計のトレーサビリティがはっきりしていると、どこを保守して、どこを改善しないといけないかもすぐにわかります。要求管理や要求変更にも柔軟に対応できそうだと思いました。
当然、仕様がしっかりできていれば、課題と設計の間のトレーサビリティが取れます。よくある課題から設計に落ちるという事はなく、仕様を経由して設計に落ちます。これを行うことで、要素間の対応関係がはっきりします。仕様の記述も自然言語であったり、UMLの図だったり、個人同士のメモであったりすることもあります。ＵＭＬは自然言語よりは若干形式的ですが、それでも大事な部分で曖昧さが残ってしまいます。そこで、VDMを活用することで、厳密な仕様の記述が可能になり、この問題を解消できます。

日本語の表記の曖昧さ

「誰でも休日が好きだ」にはどんな意味があるだろうか？このように6通りの意味が列挙されます。「誰でも休日が好きだ」と自然言語で書いた場合、1つの表現に複数の表現の可能性がどうしても生まれてしまいます。経験や感覚的には、自然言語が曖昧であることはわかっていましたが、このように説明されると自然言語がいかに曖昧か非常に納得しました。

一方、VDMで記述することで、6通りの異なる意味をそれぞれ区別された6種類の仕様記述として明確に意図を表現可能になります。ここで大事なことはやはり、顧客からヒアリングをする際に聞き出したいのは、形式的な言語ではなく、顧客からの思いや意味だということです。意思疎通の際も形式的な言語を読んでいるのではなく、心を読んでいるはずです。顧客からの課題が設計に反映されないようでは意味がないと思っています。そうした顧客の意図・意味をきちんと汲み取って表わす際のVDMの表現力の高さ、厳密さに感心しました。

さらに、VDMを使用することでテストができ、型の検査が簡単にできます。
仕様をVDMで書くことで、実際に手を動かして開発やテストを行う前に、仕様の間違いを早期に発見できます。さらに正当性の検証がなされているので、精度の高いインプットで設計を始められます。VDMの使用により、手戻りが少ない開発が可能になり、品質の向上につながると思いました。

さいごにVDMを使って形式仕様記述を行った実際のプロジェクトの事例をご紹介いただいた。