VDMを深掘りする
ソートの仕様を例に — 「どう計算するか」ではなく「何が得られれば良いか」を書く形式的仕様記述
VDMとは
VDM（Vienna Development Method）は、1970年代のIBMウィーン研究所におけるプログラミング言語意味論の研究に起源を持つ、最も歴史の長いモデル指向形式手法のひとつです。仕様記述言語 VDM-SL は ISO 標準（ISO/IEC 13817-1:1996）として規格化されており、オブジェクト指向拡張の VDM++、分散・リアルタイム拡張の VDM-RT へと発展しています。
VDMの実践上の強みは、仕様を「実行できる」形でも書けることです。数学的に厳密でありながら、実行可能なスタイル（後述の陽仕様）で書いた仕様はインタプリタで動かして挙動を確かめられるため（仕様アニメーション）、仕様そのものの誤りを実装前に発見できます。日本でも、ICカードファームウェア開発への大規模適用などの実績があります。
代表的なツール：Overture（統合開発環境）、VDMJ（コマンドライン処理系）、ViennaTalk
例題：ソートを「仕様」として書く
「リストを昇順に並べ替える」— 誰もが知るこの処理を、形式的な仕様として書くとどうなるでしょうか。重要なのは、ソートの仕様はマージソートかクイックソートかというアルゴリズムには一切言及しない、ということです。仕様が定義すべきなのは「入力に対して、どんな出力が得られれば良いのか」— それだけです。
VDMでは、この「何が得られれば良いか」を事後条件（postcondition）として書きます。本体（アルゴリズム）を持たず、事前・事後条件だけで関数を定義するこの書き方は陰仕様（implicit specification）と呼ばれ、VDMによる仕様記述の基本形です。
Sort (l : seq of int) r : seq of int post IsPermutation(r, l) and IsOrdered(r);
読み下すと「Sort は整数列 l を受け取り、整数列 r を返す。ただし r は l の並べ替え（順列）であり、かつ昇順に整列している」。これがソートの仕様のすべてです。なお事前条件（pre）は書かれていません — どんな整数列でも入力として受け付けるためです。
IsOrdered : seq of int -> bool IsOrdered(l) == forall i, j in set inds l & i > j => l(i) >= l(j); IsPermutation : seq of int * seq of int -> bool IsPermutation(l1, l2) == forall e in set (elems l1 union elems l2) & card {i | i in set inds l1 & l1(i) = e} = card {i | i in set inds l2 & l2(i) = e};
事後条件に現れる2つの述語も、VDMの関数として定義します。IsOrdered は「添字が後ろなら値は前の要素以上（昇順）」であること、IsPermutation は「どの値についても、2つの列での出現回数が一致する（同じ要素の並べ替えである）」ことを表します。
仕様の急所：順列条件を忘れると
もし事後条件が IsOrdered(r) だけだったら、「常に空リストを返す」「常に [1, 2, 3] を返す」ような実装まで仕様を満たしてしまいます。IsPermutation が「要素を勝手に捨てない・増やさない・書き換えない」ことを保証しているのです。何を書くかと同じくらい、何が欠けると壊れるかを考えることが、仕様記述の急所です。
陰仕様と陽仕様
VDMの関数には2つの書き方があります。事前・事後条件だけで「満たすべき性質」を定める陰仕様と、本体（計算手順）を与える陽仕様（explicit specification）です。開発ではまず陰仕様で性質を固定し、のちに陽仕様・実装へと段階的に詳細化していくのが基本の流れです。
| 観点 | 陰仕様（implicit） | 陽仕様（explicit） |
|---|---|---|
| 記述するもの | 満たすべき性質（事前・事後条件） | 計算の手順（アルゴリズム） |
| 実行 | 直接は実行できない | インタプリタで実行できる（仕様アニメーション） |
| アルゴリズム | 決めない（実装者に委ねる） | ひとつに決める |
| 主な役割 | 正しさの定義・契約 | プロトタイプ・実行可能モデル |
また、陽仕様の形を取りながら本体を未定義のまま残す「is not yet specified」という書き方もあります。「この関数の中身はまだ決めない」ことを、型チェックが通る形で明示的に残せます。
Sort : seq of int -> seq of int Sort(l) == is not yet specified;
陰仕様は実行できません。しかしそれは欠陥ではなく本質です。アルゴリズムを決めていないからこそ、挿入ソートでもマージソートでもクイックソートでも、事後条件を満たす限りどんな実装も「正しい」と判定できる — 陰仕様は、特定の実装から独立した中立の判定基準として機能します。
陽仕様の例：1つの仕様、3つの実装
Overtureプロジェクトの公式サンプル「sort」（Peter Gorm Larsen, 2010）には、同じソート仕様に対する複数の陽仕様が収められています。どれも実行可能で、そしてどれも冒頭の陰仕様の事後条件を満たします。
① 仕様をほぼそのまま実行する：順列から選ぶ
Sort : seq of int -> seq of int Sort(l) == let r in set Permutations(l) be st IsOrdered(r) in r;
「l の順列のうち、整列しているものを選んで返す」— 事後条件の構造をそのまま写し取った陽仕様です。let ... be st ...（〜を満たすものをひとつ選ぶ）という非決定的選択で書かれています（Permutations は l のすべての順列の集合を返す補助関数 — 定義は省略）。順列は n! 通りあるため実用性能はありませんが、仕様と実装の中間形がどんな姿かを教えてくれます。
② 挿入ソート
DoSorting : seq of int -> seq of int DoSorting(l) == if l = [] then [] else InsertSorted(hd l, DoSorting(tl l)); InsertSorted : int * seq of int -> seq of int InsertSorted(i, l) == cases true : (l = []) -> [i], (i <= hd l) -> [i] ^ l, others -> [hd l] ^ InsertSorted(i, tl l) end;
「残りをソートした結果に、先頭要素を正しい位置へ挿入する」という再帰的な定義です。
③ マージソート
MergeSorter : seq of int -> seq of int MergeSorter(l) == cases l : [], [-] -> l, others -> let l1 ^ l2 in set {l} be st abs (len l1 - len l2) < 2 in Merge(MergeSorter(l1), MergeSorter(l2)) end; Merge : seq of int * seq of int -> seq of int Merge(l1, l2) == cases mk_(l1, l2) : mk_([], l), mk_(l, []) -> l, others -> if hd l1 <= hd l2 then [hd l1] ^ Merge(tl l1, l2) else [hd l2] ^ Merge(l1, tl l2) end;
リストをほぼ半分に分け、それぞれをソートして併合する、分割統治の定義です。ここでも let ... be st ... が「長さの差が2未満になる分割を選ぶ」という形で現れます。
実行してみる
陽仕様は VDMJ / Overture のインタプリタでそのまま実行できます。実装を書く前に、仕様の段階で挙動を確かめられる — これが仕様アニメーションです。
> print DoSorting([3, 1, 66, 11, 5, 3, 99]) = [1, 3, 3, 5, 11, 66, 99]
順列選択・挿入ソート・マージソート — 3つの陽仕様はすべて、同じ陰仕様の事後条件を満たします。つまり陰仕様は「正しいソートとは何か」の定義であり、どのアルゴリズムを選ぶかは性能や文脈の問題であって、正しさの問題ではありません。この「何を」と「どう」の分離こそが、形式的仕様記述の本質です。
検証への接続
事後条件は単なるドキュメントではなく、検証の装置です。VDMでは陽仕様にも同じ事前・事後条件を併記でき、VDMJ は実行時にそれらを自動チェックするため、陽仕様（や仕様から書き起こした実装）が性質に違反すれば、その場で検出されます。
さらに「この陽仕様は事後条件を本当に満たすか」という問いは、証明責務（Proof Obligation）として機械的に生成し、証明することができます。実行やテストが「試した入力について正しい」ことしか示せないのに対し、証明は「すべての入力について正しい」ことを保証します。
本ページのコード例は、Overture プロジェクト公式サンプル集の VDM++ モデル「sort」（Peter Gorm Larsen, 2010）を、解説用に VDM-SL スタイルへ書き改めたものです（クラス構造と measure 節は省略）。
出典：Overture Examples — sort (VDM++) ↗