【 形式手法 】(Formal Method)
形式手法とは、曖昧さを排除するために、厳密な規則にしたがってシステムの仕様を決定するための方法。1970年代から始められたプログラム開発手法の1つで、論理学や離散数学などが基礎になっている。プログラムの正しさに関する数学的な証明体系として整理された理論をベースとし、形式仕様記述やモデル検査へと研究対象を発展させてきている。曖昧さを排除して、システムを正確に記述することで、エラーを少なくすることができる。
形式手法は、システムの大規模化・複雑化から、上流工程での品質改善手段として最近日本でも注目を集めるようになった。また、海外では規格・標準において形式手法を推奨もしくは必須とするものが現れ、日本企業も真剣に取り組まざるを得ない状況になってきた。

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

【 VDMTools 】
VDMToolsはデンマークのPeter Gorm Larsen博士が開発したVDM(Vienna Development Method)開発支援ツールであり、Windows・Linux・Mac OS Xで動作する。また、ツール・マニュアル共に日本語化されており、日本の開発現場での使用に向いている。2005年にCSKシステムズがデンマークの開発元から全ての権利を取得し、全世界に向けて提供している。
VDMToolsは、形式技術と実用技術を巧みに統合し、現在は以下の機能を提供する。

1. 仕様の構文、型チェック機能
2. 証明課題生成機能
3. 実行可能仕様のインタープリタとデバッグ機能
4. 実行可能仕様のコードカバレージ計測機能
5. Rational Rose との連動機能
6. VDM-SL、VDM++のドキュメント生成機能
7. 実行可能仕様からJavaやC++へのコード生成機能(オプション)
8. JavaからVDM++への変換機能（オプション）
9. CORBA APIとの連動機能(オプション)