「VDM」の版間の差分
削除された内容 追加された内容
編集の要約なし |
編集の要約なし |
||
21行目:
主な仕様記述言語の1つである「VDM-SL（Vienna Development Method - Specification Language）」は、もともとプログラミング言語の研究であるウィーン定義言語（Vienna Definition Language）の流れをくみ、欧州では現在まで40年以上も研究・実用が継続されています。日本ではようやく大規模な事例が出てきたという段階であり、かなり後れを取っています。
※形式手法の必要性とメリット
形式手法が古くから研究されてきた分野であると前述しましたが、なぜいまになって取り上げられているのでしょうか。
海外では長い間、人工衛星や航空機、原子炉の制御といったミッションクリティカルなシステムにおいて形式手法が利用されてきました。もちろん今後も形式手法は欠かせない技術です。
■自然言語におけるあいまいさ
さて、皆さんはどのような仕様書を作成しているのでしょうか。CDプレーヤのディスク取り出し機能を例に、少し考えてみましょう。
まず、「CDのEJECTボタンが押されたらCDを排出する」という仕様を書き、次に「再生中の場合は停止して」「停止中の場合は……」などと書いてだんだん条件が複雑化。文章だけでは分かりにくくなったので表を添付する、という感じでしょうか。ここまで書いて次は設計です。UMLで状態遷移図とシーケンス図を描いて、いよいよ実装に入ります。
プログラマーは、「再生中とは何か」「シーク中は再生中か」を考えます。優秀なエンジニアは条件をまとめて仕様作成者とコミットするでしょう。人によってはそのような状態を考えずに実装します。結果として、製品の仕様に作成者たちも分からない状態ができてしまいます。私はいままでそういう現場を見てきました。
では、形式手法ではない方法、つまり自然言語では厳密な仕様は記述できないのかというと、不可能ではないと思います。ただし、自然言語ではどのような記述も許されてしまい、一意に解釈できる記述を行うのは困難です。仮に自然言語で厳密な仕様を記述できたとしても、理解しにくい冗長な表現になってしまうでしょう。また、ルールのない記法において、仕様が正しいことを証明する手段はありません。
自然言語で仕様を記述した場合、仕様自体にあいまいさが入り込む可能性が高く、第三者が開発・検証を行ったり、検証を自動化するのは困難です。形式仕様記述では数学的な表記ができるよう記法が定義されており、論理的な記述により事象を明確に定義することができます。
| |||