「プログラムの強力検査器」でコードそのものを検証
開発をする立場からすれば、擬似コードではなく実際のプログラムコードを対象に、同様に強力な検査をしてほしくなります。なぜなら、プログラムコードは最終成果物でありその品質を担保したいからです。
「プログラムの強力検査器」の技術はもちろん追求されており、テストでは見つからないような不具合を探す、あるいは不具合がないことをテストよりも高く確信するためのツールが存在します。とはいえ、「擬似コード」が対象の場合と比べると、できないことや制限事項が生じる場合もあります。
なお、正確には「網羅的テストが可能な擬似コード」とは異なる仕組みで実現されていることもありますが、ここでは「テストよりも強力、あるいはテストとは違う観点をうまく扱える検査」ということでまとめてしまいます。
【事例】モバイルアプリ開発で活躍するプログラム検査器
Facebookでのモバイルアプリ開発サイクルにおいて、「プログラムの強力検査器」を使う工程を、「これまで通り」のプロセスに埋め込むことが可能なツールが開発されています。これは「Infer」というツールで、開発していた会社をFacebookが買収し、Objective-C版を開発するなどモバイルアプリ向けに整備されています。
具体的なプロセスとしては、新規機能や不具合修正などのコード変更がプログラマによって行われると、自動的に再帰テストが行われた後、他のエンジニアによるレビューが行われます。この際のレビューコメントなどは、共同作業ツールで管理されています。Inferによるレビューは、エンジニアによるレビューと同じタイミングで並行して実行され、その結果は、同じく共同作業ツールでレビューコメントとして管理されます。流行の言い方をすると「Inferという人工知能レビュアーが1人混ざっている」ということです。開発スピードが重要視されるモバイルアプリという領域のため、リリース間隔（2週間など）をより短くする必要があります。そこで、この「プログラムの強力検査器」が使われます。
この仕組みを導入した際の留意点としては、ツールに対するエンジニアの信頼を育てることでした。そこで最初は、エンジニアが悩んでいる最も重要な問題だけに集中して利用し、その後利用方法を改善していくことで対応しました。
【専門用語での補足】さまざまなプログラム解析を実現する技術
ここで紹介した技術には、内部の仕組みなどによって異なる名前が付いています。「網羅的テストが可能な擬似コード」と同じ仕組みを使っている場合は、「ソフトウェアモデル検査」と呼ばれ、Java PathFinder（Javaコード用）やCBMC（C Bounded Model Checker、Cコード用）といったツールがよく知られています。前述の通り、プログラムコードに対しては「網羅的テスト」を行うことが現実的に不可能であるため、例えばステップ数の上限など一定の制限を設けた上で「網羅的テスト」を実施します。
一方で、プログラムを動作させずにツールにコードを読みこませて、「うまくいくようになっているぞ」と説明を試みることで、正常に動作しないことが明確な部分や、正常であることが断言できない部分を洗い出すというアプローチもあり、こちらは「静的解析」と呼ばれます。Inferの解説では人工知能と表現しましたが、最近流行の機械学習などとは異なる人工知能技術として、自動推論（自動証明）の技術などが用いられています。例えば、ESC2/Java（Javaコード用）やFrama-C（Cコード用）、Spec Explorer（C#コード用）などのツールがあります。
上流工程をサポートする「ルールチェック付き仕様記述」
「網羅的テストが可能な擬似コード」においては、設計の中でも検査したい部分を擬似コードとして書き出していました。一般に、仕様書や設計書において擬似コードを使う理由は、網羅的テストをするためではなく、厳密で明確な記述を行うためです。例えば、IF-THEN-ELSEやWHILEの制御構造、あるいはAND、OR、NOTなどの論理記号とカッコを用いることで、厳密な記述（あいまいさがなく、複数の解釈が発生しない記述）となります。つまり、記述に関する「ルール」を決め、その遵守をチェックすることで、厳密で明確な表現になるということです。記述ルールの決め方によっては、ツールによる自動処理ができるようになり、さらには前述の通りテストまでも可能になります。
この擬似コードのよい部分を、仕様書や設計書の記述でもっと活用するのが「ルールチェック付き仕様記述」の技術です。これらの文書は、実装やテスト、以後の保守すべてにおいて、さまざまな人がよりどころとするからです。仕様書や設計書におけるあいまいさや誤り・抜けが、統合テストになってから、さらには運用時に見つかった場合、大きな手戻りコストが引き起こされます。オフショア開発など、仕様書や設計書が他の組織との連携のよりどころになっている場合はなおさらです。
「ルールチェック付き仕様記述」においては、ある記述範囲を特定のルールに従って記述し、すべてチェックします。例えば、利用者とシステムとの相互作用、システム内の各部品のインターフェースなどです。記述のすべてが、意味が厳密に定まった構文に従って行われるため、日本語で自由に書いた場合のように、複数の解釈が可能な記述にはなりません。また、機械処理が可能なので、未定義要素や、型定義が合わない計算などは容易に検出可能です。あとは記述のルール（記述言語）とその支援ツール次第ですが、シミュレーション、静的解析、前述の「網羅的テスト」などさまざまなチェックが可能になります。さらに、テスト対象となる項目の自動抽出、構造の可視化、メトリクス測定など、アイディア次第でさまざまな現場のプラクティスを自動化することもできるようになります。
重要なのは、この事例を「擬似コード」ではなく「仕様記述」と表現している点です。擬似コードは、実際のプログラムコードと比べると抽象的に書くもので、詳細を含まず重要な部分だけに集中できるようにします。この点は仕様書や設計書において重要ですが、「コード」というと基本的には手順を表すものに限られてしまいます。仕様書や設計書においては、「実行結果は小さい順に並んでいる」「毎日朝8時の時点では集計ファイル作成が完了している」といったように、望ましい状態を要件として記述します。逆にいうと、実装詳細を書く手間はとりたくない、そもそも実装詳細を決めつけるべきではない、ということです。このため、プログラミング言語とは似て非なる、望ましい状態を表現するのに適した記述ルール（言語）を用いることになります。
【事例】ICチップで「ルールチェック付き仕様記述」を利用
フェリカネットワークスにおけるICチップの開発では、外部仕様の記述にこの「ルールチェック付き仕様記述」を用いてきました。日本語の資料も用いますが、それらは参考資料であって、何かあったときに確認すべき情報は「ルールチェック付き仕様記述」となります。
この記述は、複数の設計・実装チーム、テストチーム、そしてサーバサイドアプリケーションを開発するパートナーなどにも共有されます。つまり、多くの開発者が記述ルール（言語）を把握して、厳密な仕様記述を読んでいるということです。
その結果、テスト工程にて発見される不具合のうち、仕様記述に起因するものの割合は非常に低くなっています。特に、記述不足や不明確な記述、記述の誤りに起因する不具合はなくなりました。
【専門用語での補足】仕様を厳密に記述する技術
ここで「ルールチェック付き仕様記述」と呼んだ技術は、専門用語では「形式仕様記述」といいます。「仕様記述」という名前ではありますが、実際には設計書と呼ぶべき内容を表現、チェックする際に使われることもあります。
フェリカネットワークスで用いた手法はVDM（Vienna Development Method）というものです。リスト2に例を示しました。コメントや日本語の記述は参考になるでしょう。invによって常に満たすべき不変条件を記述し、preとpostである操作の前後に満たすべき条件が記述されています。cardは直後の集合の要素数を返す関数です。
class イベント参加登録管理システム
登録済みユーザ集合 : set of 「ユーザ識別子」;
定員 : nat1;
inv card 登録済みユーザ集合 <= 定員 // システム状態の制約
抽選登録する : set of 「ユーザ識別子」 ==> 「ユーザ識別子」
抽選登録する(引数ユーザ集合) == is not yet specified
pre // 操作実行の前提となる事前条件
card 登録済みユーザ集合 < 定員 // 定員未満のときのみ受付
post
登録済みユーザ集合 = 登録済みユーザ集合~ union {RESULT}
and RESULT in set 引数ユーザ集合
and RESULT not in set 登録済みユーザ集合~;
// 事後条件：実行後には、引数の中から未登録の人が1人
//登録されていることをもって正しい操作だと判断する
VDMにおいて現在提供されている言語や支援ツールは、比較的エンジニアが馴染みやすいものになっています。CやJavaなどのプログラミング言語に近い言語を使い、インタプリタ実行してみることで仕様のチェックを行います。仕様をシミュレーションしテストするということです。専門用語では「アニメーション」ともいいます。
このほか、次項で紹介する「B-Method」、外部環境なども含めシステム全体を記述する「Event-B」、仕様を満たす具体例を生成できる強力なツールがある「Alloy」など、多くの手法（言語とツール）があります。
