自然言語の仕様と曖昧さの境界

ここまで、VDM の陰仕様を起点に設計・実装・テストへ降り（第1部・第2部）、仕様を書かない TDD の前提を確かめました（第3部）。最後に、実務で最も普通のやり方 — 自然言語の仕様書 — と比べます。同じソートの仕様を、自然言語で書いてみます。

一見、何の問題もない仕様です。しかし「ソートされている」とは具体的に何でしょうか。昇順でしょうか、降順でしょうか。重複した要素は保存されるのでしょうか。そもそも出力は入力の並べ替えでなければならないのでしょうか。よく見れば「大きさ」も曖昧です — 列の長さなのか、値の大きさなのか。この仕様書の中に、それらを辿る手がかりはありません。読み手は TDD のときと同じように、書き手の意図を常識で推察するしかありません。

VDM の仕様で「ソートされている」に当たるのは、事後条件の IsPermutation(r, l) と IsOrdered(r) でした。この語の意味が曖昧に感じられたら、定義を辿ることができます。

IsOrdered の中に現れる forall / inds / l(i) は、VDM-SL の言語仕様（ISO/IEC 13817-1）で意味が定義された言語要素です。つまり仕様に現れるどの語も、辿っていけば最終的に厳密な定義へ行き着きます。途中で行き止まりになる語 — 定義されないまま使われる語 — が存在しないのです。

ソートは誰にとってもほぼ自明な処理です。だからこの例では、自然言語との差は小さく見えます。しかし、文化によって定義が変わる概念になると、同じ曖昧さが大きな差になります。たとえば、次のような要求を考えてみてください。

「社会通念上問題がある」とは、具体的に何を指すのでしょうか。国によって、業界によって、個人によって解釈は異なります。人間のチームなら「常識で分かるだろう」で進むかもしれません — 前ページで見た、文化と常識の共有という暗黙の前提です。しかし解釈が分かれた瞬間、この仕様は互いに矛盾する複数の実装を、同時に「正しい」と認めてしまいます。

自然言語でも、脚注や用語集を重ねることで厳密さに近づけることはできます。しかし「どの部分に曖昧さが残っているのか」を客観的に検証する手段がありません。曖昧さは文章のあちこちに散らばったまま、監査できないのです。

同じ要求を VDM で書いてみます。「社会通念上問題がある」という表現を、参照可能な定義に置き換えます。

漠然としていた表現は not (name in set blocked) という厳密な述語になり、blocked が何を指すか — 組織 A が分類リスト α として公開する組織名の集合 — は、注記としてこの 1 箇所に記録されます。形式化の中では、blocked は与えられた集合として扱われます。もちろん、これで曖昧さがゼロになったわけではありません。リスト α の中身が妥当か、更新はいつ反映されるのか — それは形式化の外側に残ります。

重要なのは、残った曖昧さが blocked という 1 つの名前に局所化されたことです。仕様のどこまでが厳密で、どこから先が外部への参照なのか — その境界を、誰でも客観的に指し示せます。レビューの問いは「この文章のどこかに曖昧さはないか」という漠然としたものから、「リスト α の定義と運用は妥当か」という具体的なものに変わります。