フォーマルメソッド：形式仕様

システム開発において、「何を開発するのか」は常に重要な問題です。 システムの機能仕様を日本語などの自然言語で記述すると、

• 読み解くためには背景知識が暗黙的に要求される
• 同じ記述で複数の解釈が可能な、曖昧な表現が混入する
• いわゆる「てにをは」や表記の揺れのような、表現上の問題に時間や労力がかかってしまう
• 要点を拾い出すことが難しい
• 具体的な動作は、それぞれの読み手が想像することしかできない
• 仕様の一部を変更した時の影響がわからない

といった問題が出てきます。 その結果、仕様には合意していたものの、

• ここの動作は、こんな意図ではなかった
• ここを実装していて、意味が読み取れなかった
• 仕様の中で矛盾した記述があって、どちらが正しいのかわからない

といったトラブルが発生します。
形式仕様でそれを解決しませんか？
形式仕様はこれまで、数学的な証明などの専門知識が必要だというイメージから難しいと敬遠されることがありました。

先端技術研究所では、カジュアルな仕様記述、ライブな仕様記述環境、フレキシブルなツールで、VDMを中心とした形式仕様をより広い領域に適用可能にすることを目指した研究を行っています。

a LIVE IDE for VDM-SL based on Pharo Smalltalk

ViennaTalk