仕様から設計へ

ソートの仕様に規模と時間の要求を加え、設計調査・設計書・実装・仕様由来のテストまでを一気通貫でたどる

仕様を精緻化する：事前条件と非機能要求

前ページの Sort 仕様は「何が得られれば良いか」を定めましたが、入力の規模も許される実行時間も述べていません。現実の開発では、この非機能要求こそが設計を左右します。そこでまず、事前条件（pre）に想定される入力規模を定めます。ここでは列の長さを最大 10^7 とします。

もうひとつの要求「実行時間 5 秒以内」は、VDM-SL では直接記述できません — VDM-SL の関数には時間という概念がないためです。記述できない要求を消してしまうのではなく、コメントとして仕様に添えて設計工程へ引き継ぎます（時間そのものを形式的に扱いたい場合は、リアルタイム拡張の VDM-RT や、時間オートマトンに基づく UPPAAL のようなツールの領分になります）。

Sort (l : seq of int) r : seq of int pre len l <= 10**7 post IsPermutation(r, l) and IsOrdered(r); -- 非機能要求（VDM-SL では実行時間を直接記述できない）: -- len l = 10**7 の入力に対し、実行時間は 5 秒以内であること。

事前条件は「呼び出し側が守るべき約束」です。len l <= 10^7 を pre に置くことで、契約の適用範囲が明示され、実装は 10^7 を超える入力について責任を負いません。一方、コメントの時間要求は形式検証の対象外ですが、仕様書の一部として設計・テストにトレースされます。

設計調査：仕様を満たせるかを見積もる

設計とは、仕様が固定しなかった「どう」を決めることです。アルゴリズムはバブルソートで良いのか、クイックソートが必要か。言語は C++ が必要か、JavaScript で十分か。要求（n = 10^7、5 秒以内）に照らして、まず比較回数のオーダーを見積もります。

アルゴリズム	比較回数のオーダー	n = 10^7 での概算
バブルソート	O(n²)	n²/2 ≈ 5×10^13 回
クイック / マージソート	O(n log n)	n log₂ n ≈ 2.3×10^8 回

差はおよそ 20 万倍です。CPU が 1 秒に処理できる単純演算はおおむね 10^8〜10^9 回ですから、この時点で「バブルソートは言語を問わず絶望的、O(n log n) ならどの主要言語でも射程内」という当たりがつきます。見積もりを実測で裏付けます。

参考実測

Node.js v26 / Apple Silicon 開発機での参考値です。実測値は環境に依存するため、計測条件ごと設計書に記録します。

方式	実測時間
Int32Array(10^7).sort()（TypedArray・数値ソート）	約 0.15 秒
Array(10^7).sort((a, b) => a - b)（通常配列＋比較関数）	約 1.6 秒
バブルソート（n = 3×10^4 の実測 0.35 秒を n² で外挿）	約 3.9×10^4 秒 ≈ 11 時間

結論は二つです。第一に、決定的なのはアルゴリズムです — バブルソートは 4 桁足りず、どの言語を選んでも回収できません。第二に、O(n log n) を選べば JavaScript で十分です（0.15〜1.6 秒 ≪ 5 秒）。C++ はさらに余裕を生みますが、この要求では必須ではありません。言語選定は性能ではなく、チームのスタックや運用環境という文脈で決められます。

設計書に落とす

調査結果を設計書として残します。現在広く使われている形式のひとつが、Google などで普及した Design Doc です — 自然言語で、背景・目標と非目標・設計・検討した代替案・テスト計画を 1 つの文書にまとめます。個々の決定を軽量に記録する ADR（Architecture Decision Record）も普及していますが、ここでは全体を見渡せる Design Doc 形式のサンプルを示します。

概要

VDM 仕様 Sort（pre: len l <= 10^7、post: 順列かつ昇順、非機能: 10^7 要素で 5 秒以内）を満たす実装の設計。標準ライブラリの O(n log n) ソートを TypedArray 上で用いる。

背景

ソート処理の契約は VDM-SL の陰仕様として確定済み。アルゴリズムと実装言語は仕様で固定されておらず、非機能要求（実行時間）を満たすように設計で選定する。

目標 / 非目標

目標：事後条件（順列・昇順）の充足。n = 10^7 の入力を 5 秒以内に処理。事前条件に違反する入力の明示的な拒否。

非目標：安定ソート（仕様が要求していない）。10^7 を超える入力への対応。並列化・外部メモリソート。

設計

アルゴリズム — 比較ソートの理論下限は Ω(n log n)。バブルソート O(n²) は n = 10^7 で約 5×10^13 回の比較となり、実測外挿で約 11 時間かかるため棄却。仕様はアルゴリズムを固定しないため、実績のある標準ライブラリのソートを採用する（V8 では通常配列の sort は TimSort、TypedArray の既定の sort は C++ 実装のイントロソート系 — いずれも O(n log n)）。

言語 — 参考実測では JavaScript でも Int32Array.sort() が約 0.15 秒、比較関数付き Array.sort でも約 1.6 秒と、いずれも 5 秒を大きく下回る。C++ はさらに余裕を生むがこの要求では必須ではなく、運用スタック（Node.js）に合わせて JavaScript を採用する。

データ表現 — VDM の seq of int を Int32Array に写像する（値域を 32bit 整数と仮定し、仕様との対応として明記する）。ボックス化された要素と比較関数のオーバーヘッドを避ける。

検討した代替案

バブルソート — 棄却。速度が 4 桁不足し、言語をどう選んでも回収できない。

自作クイックソート — 棄却。標準実装で要求を満たせるため、最悪計算量 O(n²) と実装バグのリスクに見合わない。

C++（std::sort）— 保留。性能余裕は大きいが運用スタックに合わない。要求が n = 10^8 級に伸びた時点で再検討する。

テスト計画

事後条件をオラクル化したプロパティベーステスト。事前条件の境界値（長さ 0、1、10^7）と違反入力のテスト。時間要求に対応する性能テスト（n = 10^7 を 5 秒以内）。

リスク

32bit 範囲外の値を含む入力（pre に値域を追記して仕様へ還流させ、入力検証を追加する）。実行環境による性能変動（計測条件を記録し、性能テストは CI の専用ジョブで実行する）。

ポイントは、設計書のどの判断も仕様の行にトレースできることです。アルゴリズム選定は事後条件ではなく時間コメントから、データ表現は seq of int から、入力ガードは事前条件から、それぞれ導かれています。

実装

設計書の決定をコードに落とします。仕様がアルゴリズムを固定しないおかげで、実装は標準ライブラリのソートを呼ぶだけの薄いものになります。事前条件は入力ガードとして実装に現れます。

// 設計判断: 標準ライブラリの O(n log n) ソートを TypedArray 上で使う function sortLargeSequence(input) { // pre: len l <= 10**7 — 事前条件は入力ガードになる if (input.length > 10 ** 7) { throw new RangeError('precondition violated: len l <= 10^7'); } // seq of int を Int32Array に写像（32bit 整数を仮定 — 設計書に明記） const r = Int32Array.from(input); r.sort(); // TypedArray の sort は数値昇順・O(n log n) return r; }

仕様の pre がそのまま先頭のガードに、設計書のデータ表現の決定が Int32Array.from に対応しています。実装のどの行も、仕様か設計書のどこかを指しています。なお、32bit という値域の仮定は、仕様の seq of int より狭い契約です。厳密には pre に値域を追記して仕様へ還流させるべきもの — 設計判断が仕様を精緻化する、逆向きのトレーサビリティです。

仕様から導かれたテストで検証する

最後に、出来上がったコードを仕様に立ち返って検証します。テストは仕様から機械的に導けます。まず、事後条件の 2 つの述語をそのままテストオラクル（正解判定器）として書き写します。

// 事後条件の 2 述語を、そのままテストオラクルに写し取る const isOrdered = (r) => r.every((v, i) => i === 0 || r[i - 1] <= v); const isPermutation = (r, l) => { if (r.length !== l.length) return false; const count = new Map(); for (const x of l) count.set(x, (count.get(x) ?? 0) + 1); for (const x of r) { const c = count.get(x); if (!c) return false; count.set(x, c - 1); } return true; };

このオラクルを使い、プロパティベーステスト（fast-check など）でランダムな入力に対して事後条件を検査します。事前条件はガードのテストに、コメントの時間要求はそのまま性能テストになります。なお fc.integer() の既定の生成範囲は 32bit 整数で、データ表現の仮定と揃っています。

// post → プロパティベーステスト: ランダム入力で事後条件を検査 test('post: IsPermutation(r, l) and IsOrdered(r)', () => { fc.assert( fc.property(fc.array(fc.integer()), (l) => { const r = [...sortLargeSequence(l)]; return isOrdered(r) && isPermutation(r, l); }) ); }); // pre → 境界: ちょうど 10^7 は許容、超過は拒否 test('pre: len l <= 10^7', () => { expect(() => sortLargeSequence(new Int32Array(10 ** 7))).not.toThrow(); // length だけ持つ配列様オブジェクトで、巨大な配列の確保を避ける expect(() => sortLargeSequence({ length: 10 ** 7 + 1 })) .toThrow(RangeError); }); // 時間コメント → 性能テスト test('perf: 10^7 elements within 5 s', () => { const l = Int32Array.from({ length: 10 ** 7 }, () => (Math.random() * 2 ** 31) | 0); const t0 = performance.now(); sortLargeSequence(l); expect(performance.now() - t0).toBeLessThan(5000); });

仕様とテストの対応

仕様の要素	導かれるテスト
pre len l <= 10^7	入力ガードの境界値テスト（10^7 ちょうどは許容、超過は拒否。長さ 0・1 の小さな列はプロパティテストが生成）
post IsPermutation(r, l) and IsOrdered(r)	事後条件をオラクル化したプロパティベーステスト
コメント：10^7 要素で 5 秒以内	性能テスト（n = 10^7 を実測し 5 秒未満を検査）
すべての入力に対する保証	テストでは到達できない — 前ページで見た証明責務・証明の領分

正直な注意をひとつ。テストが示すのは「試した入力について事後条件が成り立った」ことであり、証明ではありません。プロパティベーステストはその差を大きく縮めますが、すべての入力に対する保証が必要なら、証明責務を証明する道に進むことになります。

まとめ：一気通貫のトレーサビリティ

仕様が「何を」を固定し、設計調査が「どう」を数字で選び、設計書が判断と根拠を残し、実装が設計を写し、テストが仕様に立ち返って検証します。どの成果物も仕様にトレースできる — これが、形式的仕様を起点にした開発の骨格です。IID の formal-agent-contracts プラグインは、この流れをマルチエージェント開発のエージェント間契約に適用しています。