VDM

VDM（Vienna Development Method）は、IBMのウィーン研究所で1960年代から70年代にかけて開発された形式手法。

その仕様記述言語VDM-SLは1996年にISO標準（ISO_IEC_13817-1）となっている。VDM-SLをオブジェクト指向拡張したVDM++も、欧州連合ESPRIT計画のAFRODITEプロジェクトで開発された。

形式手法とは、1970年代から始められたプログラム開発手法の1つで、論理学や離散数学などが基礎になっています。プログラムの正しさに関する数学的な証明体系として整理された理論をベースとし、形式仕様記述やモデル検査へと研究対象を発展させてきています。最初は取りあえず、「品質向上のための手法（ツール）」ととらえてもよいでしょう。

　形式手法は、システムの大規模化・複雑化から、上流工程での品質改善手段として最近日本でも注目を集めるようになりました。また、海外では規格・標準において形式手法を推奨もしくは必須とするものが現れ、日本企業も真剣に取り組まざるを得ない状況になってきました。 　形式手法には多種多様な側面があります。本稿では、形式手法の最も重要な要素である仕様を厳密に記述することを主目的にする仕様記述部分モデルを検証することを主目的にする形式検証部分を簡単に紹介した後、仕様記述部分である形式仕様記述について説明します。

■形式仕様記述（形式的仕様記述） 　「形式仕様記述」は、仕様の厳密な定義を目的としています。

　システムが「仕様」として定義され、これが開発のベースとなる現在の開発スタイルにおいて、仕様作成者の意図を正しくシステムに反映させるには、仕様作成者がシステムを直接開発・検証するか、正しい仕様と対比してシステムを開発・検証する必要があります。しかし、仮に仕様作成者がすべての開発・検証を行ったとしても、仕様自体に矛盾や未定義事項があれば、システムが正しく振る舞うことを保証できません。 　そこで、矛盾がなく論理的に正しい仕様を作成するために考案されたのが形式仕様記述です。形式仕様記述を行うための「仕様記述言語」には、VDM-SL、VDM++、RAISE/RSL、Z、B、Clear、OBJ、CafeOBJ、CASL、LOTOSなどがあります（注）。

注：VDM-SLは1996年に、Zは2002年にISOにて標準化されています。

　主な仕様記述言語の1つである「VDM-SL（Vienna Development Method - Specification Language）」は、もともとプログラミング言語の研究であるウィーン定義言語（Vienna Definition Language）の流れをくみ、欧州では現在まで40年以上も研究・実用が継続されています。日本ではようやく大規模な事例が出てきたという段階であり、かなり後れを取っています。