豆寄席第18回『形式仕様技術の活用～仕様の位置付けとVDMによる厳密な記述』参加レポート
こんにちは！豆蔵note編集室です！
今回は豆寄席レポートをご紹介します。
What's 豆寄席？
豆寄席は、豆蔵が毎月社員向けに行なっている技術イベントです。是非この場を皆さんとの交流の場として活用したい！そんな声をもとにオープンな場として提供する事に致しました。豆寄席では、豆蔵の技術的知見、開発スタイル、開発の楽しさ等を皆さんと一緒にお話しさせていただいております。connpassを通じて無料のオンラインセミナーとして開放中です！是非お気軽にご参加ください＾＾
テーマ：形式仕様技術の活用～仕様の位置付けとVDMによる厳密な記述
本講演ではまず開発プロセス全体の中での仕様の位置付けを確認したあと、主に厳密な仕様記述方法の一例（VDMファミリー）をご紹介し、そうした厳密な記述が開発プロセス全体へ及ぼす影響についてお話しします。仕様と設計の違いにも触れる予定です。また講演の後半ではこれまで手掛けてきた書籍の紹介を行いながら開発プロセス全体との関係を改めてご説明します。
以下、豆寄席レポート
北 博文
2022年5月30日に豆寄席第18回として、『形式仕様技術の活用～仕様の位置付けとVDMによる厳密な記述』を開催しました。
本セミナーではデザイナーズデン代表取締役社長の酒匂寛さんにご講演頂きました。
本稿では講演の内容を、豆寄席の参加レポートとしてご紹介します。
VDMについては初心者なのですが、仕様書の書き方や形式的な事、その意味には関心があり、非常に興味深い内容でした。
以下では、いくつかの印象深かったスライドを選んで、わたしの観点になってしまいますが、コメントや自分なりの学びについて書いていきたいと思います。
課題・仕様・設計
まず、形式仕様技術の説明に入る前にそもそも仕様とは何かについてお話しいただきました。酒匂さん曰く、システム開発には3つの視点があります。
利用者の視点、利用者と開発者の視点、開発者の視点の3つ
「課題」は利用者の視点、「仕様」は利用者と開発者の視点、「設計」は開発者の視点が求められます。仕様は課題と設計をつなぐもので、課題をどのように定式化すれば実現するかが書かれています。その実現方法として展開されたのが設計です。
仕様が曖昧であると、問題が発生します。日常生活や日々の仕事でも、例えば誰かに何かをお願いした際に、思っていたことと違うフィードバックが返ってくることがあります。また、何かをお願いされた際に、ふわっとしたお願いを頼まれた。よく確認すると何か違うと思うような機会はよくあると思います。システム開発においてはなおさら、仕様が曖昧であると、利用者と開発者のコミュニケーションの際のさまざまな局面で弊害が起こることは容易に想像がつきます。仕様は必要なレベルで厳密に記述した方が品質の高いシステムが開発できると納得できる解説でした。
さらに、仕様がきちんと存在している事で、課題と設計の間のトレーサビリティが取れます。
課題を通じて、仕様と設計のトレーサビリティがはっきりしていると、どこを保守して、どこを改善しないといけないかもすぐにわかります。要求管理や要求変更にも柔軟に対応できそうだと思いました。
当然、仕様がしっかりできていれば、課題と設計の間のトレーサビリティが取れます。よくある課題から設計に落ちるという事はなく、仕様を経由して設計に落ちます。これを行うことで、要素間の対応関係がはっきりします。仕様の記述も自然言語であったり、UMLの図だったり、個人同士のメモであったりすることもあります。ＵＭＬは自然言語よりは若干形式的ですが、それでも大事な部分で曖昧さが残ってしまいます。そこで、VDMを活用することで、厳密な仕様の記述が可能になり、この問題を解消できます。
日本語の表記の曖昧さ
「誰でも休日が好きだ」にはどんな意味があるだろうか？このように6通りの意味が列挙されます。「誰でも休日が好きだ」と自然言語で書いた場合、1つの表現に複数の表現の可能性がどうしても生まれてしまいます。経験や感覚的には、自然言語が曖昧であることはわかっていましたが、このように説明されると自然言語がいかに曖昧か非常に納得しました。
一方、VDMで記述することで、6通りの異なる意味をそれぞれ区別された6種類の仕様記述として明確に意図を表現可能になります。ここで大事なことはやはり、顧客からヒアリングをする際に聞き出したいのは、形式的な言語ではなく、顧客からの思いや意味だということです。意思疎通の際も形式的な言語を読んでいるのではなく、心を読んでいるはずです。顧客からの課題が設計に反映されないようでは意味がないと思っています。そうした顧客の意図・意味をきちんと汲み取って表わす際のVDMの表現力の高さ、厳密さに感心しました。
さらに、VDMを使用することでテストができ、型の検査が簡単にできます。
仕様をVDMで書くことで、実際に手を動かして開発やテストを行う前に、仕様の間違いを早期に発見できます。さらに正当性の検証がなされているので、精度の高いインプットで設計を始められます。VDMの使用により、手戻りが少ない開発が可能になり、品質の向上につながると思いました。
さいごにVDMを使って形式仕様記述を行った実際のプロジェクトの事例をご紹介いただいた。
形式仕様プロジェクト事例
VDMは実際に実績のある手法です。
Whatに関する記述はVDMで可能ですが、Whyの部分に関しては日本語での補足がいります。
仕様の記述要素
仕様の三要素は構造、機能、振舞に分類されます。
機能仕様の構成
事前条件、不変条件、事後条件を構成することによって、機能仕様を構成することができます。とても曖昧な課題が仕様に落ち、3つに分類された仕様の構成要素が、形式的に検査できるという方法はとてもシンプルで個人的には非常に興味深い内容でした。
妥当性確認と正当性検証
仕様と課題との間の確認をするのが、妥当性確認。仕様に対して、設計が正しく行われているかの検査が正当性検証。厳密な仕様をすることで厳密なチェックが可能になるということがわかりました。
まとめ
常に自明でない設計が、仕様と対応付けられているか常に確認できているのが形式仕様技術を使用する一つの利点と言えるでしょう。
登壇して頂いた酒匂さんはソフトウェアに関する訳書、著書も多く、
私はソフトウェア要求と仕様とVDM++の本に興味を持ちました。ぜひ読んでみたいと思います。また機会があれば、学習し、活用できればと思います。
豆蔵では形式手法を学ぶための講座をご用意しております。興味のある方は是非お問い合わせください。
最後に
今回の豆寄席レポートはいかがでしたでしょうか？
豆寄席は月に一度オンラインにて実施しておりますので、ご都合の宜しい時に是非ご参加ください！
※転載元の情報は上記執筆時点の情報です。
上記執筆後に転載元の情報が修正されることがあります。