モダナイゼーションでは、旧システムと新システムのコードが一致していること自体を正しさの基準にはできない。言語、フレームワーク、アーキテクチャ、データ構造、実行環境を変えるなら、同じ業務を実現していても実装構造は変わる。一方、古い認証方式や現在は不要な制約まで忠実に再現すれば、刷新によって解消するはずだった技術的な制約も新システムへ持ち込むことになる。
そのため、モダナイゼーションでは、旧システムに存在する性質を一括して保存するのではなく、何を保存し、何を意図的に変更するのかを先に分ける必要がある。業務計算、データの意味、外部との契約などは保存対象になり得る一方、内部構造、認証方式、性能特性などは新しい目標へ変更する対象になり得る。
この区別を行わないままコード変換だけを高速化すると、新コードがコンパイルでき、テストが通り、起動したとしても、それだけでは変換の正しさを判定できない。旧システムに存在した業務規則を失っているかもしれず、逆に廃止すべき古い挙動を忠実に再現しているかもしれない。
この問題に対する有力な検証方法の一つが、既存コードから仕様を復元し、変換後コードからも同じ形式の仕様を作り、両者を比較する方法である。旧コードと新コードの構造が異なっていても、入力条件、業務規則、状態遷移、データ更新、出力、例外といった共通の観点へ写せば、実装の字面ではなく保存すべき意味を比較できる。
ただし、この一致をシステム全体の等価性の証明とみなすことはできない。比較モデルに含めなかった情報、抽出器が共通して見落とした差異、実行環境との相互作用、データ移行、性能、可用性、セキュリティなどは別の観測面に残る。新旧コードから仕様を生成して比較する方法は、モダナイゼーションにおける非常に良い検証レイヤーである一方、それ単独を等価性の証明とみなすべきではない。本稿では、その保証範囲を分解し、どの検証を組み合わせればモダナイゼーションの正しさをより正確に主張できるかを整理する。
1. モダナイゼーションで「正しい」とは何を意味するのか
ソフトウェアの再構築では、reverse engineering、restructuring、reengineering といった異なる操作が古くから区別されてきた。Chikofsky と Cross は、既存資産から設計情報を回収すること、外部仕様を保ちながら内部構造を変えること、既存システムを分析して新しい形へ再構成することを別の概念として整理している[1]。この区別は、既存システムへ手を加える操作が一種類ではないことを示している。
reverse engineering では、主として既存システムを調べ、その構造や設計をより高い抽象度で理解する。ここでは、対象を理解すること自体が中心になる。restructuring では、外部から観測される振る舞いをできるだけ保ちながら、内部表現や構造を変更する。reengineering まで広げると、既存システムを分析したうえで、新しい要求や構造を取り込みながら再構成する。モダナイゼーションでは、この三つに相当する活動が一つの工程内に混在することがある。
例えば、古い業務システムを新しい言語へ移すとき、まずコードを解析して現行仕様を復元する。この部分は reverse engineering に近い。次に、同じ業務処理を新しい言語やフレームワークへ移し替える。この部分では、外部の意味を保ちながら内部構造を変更する restructuring の性質が強くなる。さらに、認証方式を変更し、クラウド向けの構成へ変え、新しい運用要件を追加するなら、旧システムの単純な再現を超えて reengineering の領域へ入る。
この三つを区別すると、「旧システムと同じであること」をモダナイゼーション全体の成功条件にできない理由が明確になる。理解する工程では、現行システムが実際に何をしているかをできるだけ正確に取り出したい。保存する工程では、選んだ性質を新しい実装でも維持したい。変更する工程では、旧システムと異なること自体が目標になる。
AI を使ったモダナイゼーションでも、この構造は変わらない。コード生成だけが高速になっても、どの挙動を保存するかを決める工程、変換後の挙動を検証する工程、非機能要件や運用条件を確認する工程まで自動的に同じ比率で短縮されるわけではないことは既稿でも整理した[2]。実装時間が短くなるほど、むしろ「何を正しいと判定するか」が工程上の制約として目立つようになる。
ここで、旧システムを \(C_{\mathrm{old}}\)、新システムを \(C_{\mathrm{new}}\) とする。モダナイゼーションでは、通常、両者の実装は異なる。
\[
C_{\mathrm{old}} \neq C_{\mathrm{new}}
\]
\(C_{\mathrm{old}}\) と \(C_{\mathrm{new}}\) は、単なるソースファイルの文字列ではなく、コード、ライブラリ、構成、配置などを含む実装として考える。この不一致は、モダナイゼーションの失敗を表しているわけではない。言語やフレームワークを変えればコードは変わる。モノリスを複数サービスへ分割すればプロセス構成も変わる。データベース製品や実行基盤を変えれば構成情報も変わる。
そのため、正しさを次の同一性として定義することはできない。
\[
C_{\mathrm{old}} = C_{\mathrm{new}}
\]
この式を要求すれば、内部構造を変えるモダナイゼーションそのものが不可能になる。一方で、「違っていてよい」とだけ定義すれば、保存すべき業務規則やデータ意味まで失われても成功と判定できてしまう。必要なのは、システム全体を同一か非同一かで判定することではなく、比較対象となる性質を分解することである。
例えば、システムが持つ一つの性質を \(\phi\) とする。\(\phi\) は、税額計算、注文状態の遷移、顧客データの参照関係、応答時間など、検証したい対象を一つ取り出す関数だと考えればよい。
\[
\phi(C)
\]
同じシステム \(C\) でも、選ぶ \(\phi\) によって観測するものは異なる。税額計算を観測すれば旧新で一致させたいかもしれない。応答時間を観測すれば、旧システムと同じ値ではなく、より短い値を要求するかもしれない。認証方式なら、旧方式との一致そのものを避けたい場合もある。
この構造は、プログラムの正しさを構文上の一致ではなく、プログラムが満たすべき論理的な性質として記述する Hoare の公理的意味論とも接続する[3]。Hoare 論理では、プログラムの文字列が別のプログラムと同じかを調べるのではなく、実行前に成立する条件と、実行後に成立すべき条件の関係としてプログラムを捉える。
モダナイゼーションでも同じ方向の分解が必要になる。旧コードと新コードが同じかを一度に問うのではなく、何を保存するのか、何を変更するのか、それぞれについてどの関係が成立すれば正しいと言えるのかを先に定義する。ここを定義できて初めて、仕様比較、実行比較、データ検証、非機能試験といった後続の検証へ「何を確認するための検証なのか」という役割を与えられる。
2. 保存する性質と意図的に変える性質を分ける
モダナイゼーションで最初に決める必要があるのは、旧システムから何をそのまま持ってくるかではなく、どの性質を保存対象とし、どの性質を変更対象とするかである。既存コードには、業務上不可欠な規則と、現在の実装方式に由来する構造と、過去の制約によって残った処理が同時に含まれている。それらを一括して「現行仕様」とみなし、新システムへ再現すると、保存すべき業務意味だけでなく、刷新によって除去するはずだった制約まで引き継ぐことになる。
例えば請求システムを刷新するとき、同じ商品、税率、数量から算出される税込金額は、新旧で同じ結果になることが求められる。一方、認証方式については、旧システムがパスワードだけで認証していたからといって、その挙動を忠実に再現することが正しいとは限らない。データベースについても、旧システムの顧客テーブルと契約テーブルを同じ形で残す必要はないが、ある契約がどの顧客に属するかという意味まで変われば業務データが壊れる。
同じ「旧システムとの差」であっても、税額計算の差は欠陥になり得る一方、認証方式や内部構造の差は刷新の成果になり得る。この違いを先に定義しなければ、差分を検出できても、その差分を不具合として直すべきか、意図した変更として受け入れるべきかを判定できない。
| 性質 | 旧システムとの関係 | 検証で確認すること |
|---|---|---|
| 業務計算結果 | 原則として意味を保存する。 | 同じ業務条件に対して、丸め規則など明示された変更を除き、必要な結果が一致することを確認する。 |
| データの意味 | 物理的な表現が変わっても意味を保存する。 | 識別子、参照関係、単位、精度、履歴など、業務上の意味が移行後も成立することを確認する。 |
| 外部インターフェース | 完全一致ではなく互換性を保存する場合がある。 | 既存の利用側が依存する入力、出力、エラー条件などが、定めた互換性の範囲で維持されることを確認する。 |
| 内部アーキテクチャ | 意図的に変更できる。 | 旧構造を再現したかではなく、新しい設計上の制約や分割方針を満たすことを確認する。 |
| 性能 | 一致ではなく新しい目標値を要求できる。 | 応答時間、処理量、資源消費などが、定義した負荷条件の下で受入基準を満たすことを確認する。 |
| セキュリティ | 旧挙動を保存せず、より高い要求へ変更する場合がある。 | 認証、認可、暗号化、依存関係、脆弱性対策などが、新しいセキュリティ要件を満たすことを確認する。 |
この分類では、「保存する」と「同じ実装を残す」ことも区別しなければならない。例えば外部 API を保存対象にしたとしても、内部のクラス構造やデータベースアクセス方式まで旧システムと同じにする必要はない。保存対象になるのは、利用側から見た入力条件、返却値、エラー契約などであり、その契約をどのような内部構造で実現するかは変更対象になり得る。保存の単位を実装ではなく性質として定義することで、内部を刷新しながら必要な互換性を維持できる。
逆に、既存コードから読み取れる挙動だからといって、自動的に保存対象になるわけでもない。長期間運用されたシステムには、過去の製品制約に対する回避処理、すでに不要になった制度対応、現在は使われていない例外処理、不具合でありながら外部システムが依存している挙動が混在する。既稿では、AI を使って既存システムを再構築する場合でも、「現行コードが何をしているか」を抽出することと、「そのうち何を将来も仕様として採用するか」を決めることは別の工程であり、この仕様選択と検証が自動化の境界として残ることを整理した[4]。
この関係を数式で整理する。システムが持つ検証対象の性質を \(\phi_1,\phi_2,\ldots,\phi_n\) とし、旧システムを \(C_{\mathrm{old}}\)、新システムを \(C_{\mathrm{new}}\) とする。各 \(\phi_i\) は、システム全体から特定の性質だけを取り出す関数である。
\[
\phi_i(C)
\]
例えば、\(\phi_1(C)\) を税額計算規則、\(\phi_2(C)\) を顧客と契約の対応関係、\(\phi_3(C)\) を公開 API の振る舞い、\(\phi_4(C)\) を応答時間と考えることができる。同じシステム \(C\) を観測していても、どの \(\phi_i\) を選ぶかによって比較する性質は異なる。
検証対象となる性質の番号集合を \(I\) とし、そのうち旧システムから保存する性質を \(I_{\mathrm{preserve}}\)、意図的に変更する性質を \(I_{\mathrm{change}}\) とする。
\[
I = I_{\mathrm{preserve}} \cup I_{\mathrm{change}}
\]
\[
I_{\mathrm{preserve}} \cap I_{\mathrm{change}} = \varnothing
\]
一つ目の式は、検証対象となる性質を保存側と変更側へ分類することを表す。二つ目の式は、一つの性質を同時に「旧システムと同じ関係を求める対象」と「新しい基準へ変更する対象」に置かないことを表す。この区別が曖昧だと、例えば性能について旧システムとの一致を要求しながら同時に改善も要求するといった、判定基準そのものの矛盾が生じる。
保存する性質についても、すべてに単純な値の一致を要求するわけではない。それぞれの性質に対して、旧新の間で成立すべき関係を \(R_i\) と定義する。
\[
\forall i\in I_{\mathrm{preserve}},\quad R_i \left( \phi_i(C_{\mathrm{old}}), \phi_i(C_{\mathrm{new}}) \right)
\]
\(\forall\) は、保存対象に含まれるすべての性質について条件を確認することを表す。\(R_i\) は、その性質に固有の保存条件である。金額計算なら数値の一致を要求できる。浮動小数点計算なら一定の誤差以内という関係になるかもしれない。公開 API なら、HTTP 応答の文字列が完全一致することではなく、既存クライアントが必要とする契約を満たすことを \(R_i\) とできる。
つまり、「保存」とは単一の等号ではない。
\[
R_i \neq R_j
\]
となる場合がある。性質によって保存の意味が異なるからである。金額、状態遷移、API、データ、処理順序をすべて一つの等価関係で比較すると、必要以上に厳しい比較と、逆に不十分な比較が同時に生じる。
変更対象については、旧システムとの関係ではなく、新システムが満たすべき受入条件を定義する。性質 \(j\) に対する許容範囲を \(A_j\) とすると、必要なのは次の条件である。
\[
\forall j\in I_{\mathrm{change}},\quad \phi_j(C_{\mathrm{new}}) \in A_j
\]
\(A_j\) は、新システムで受け入れられる値や状態の集合を表す。例えば性能について、通常負荷時の応答時間の 95 パーセンタイルを 500 ミリ秒以下と定めるなら、500 ミリ秒以下という範囲が \(A_j\) になる。認証方式について、多要素認証を必須と定めるなら、多要素認証を備えた状態だけを \(A_j\) に含めることになる。
この場合、旧システムの性能が 800 ミリ秒、新システムが 450 ミリ秒だったとき、両者は一致していない。しかし 500 ミリ秒以下という受入条件を満たしているなら、その差は失敗ではなく意図した改善である。変更対象に旧システムとの等価性ではなく \(A_j\) を使う理由は、刷新によって生じるべき差異まで不具合として扱わないためである。
保存条件と変更条件を合わせると、モダナイゼーションの正しさの基本形は次のようになる。
\[
\mathrm{CorrectModernization} = \left[ \bigwedge_{i\in I_{\mathrm{preserve}}} R_i \left( \phi_i(C_{\mathrm{old}}), \phi_i(C_{\mathrm{new}}) \right) \right] \land \left[ \bigwedge_{j\in I_{\mathrm{change}}} \phi_j(C_{\mathrm{new}}) \in A_j \right]
\]
\(\bigwedge\) は、列挙された条件がすべて成立することを意味する。左側は「保存すると決めたすべての性質について、それぞれに定めた保存関係が成立する」ことを表す。右側は「変更すると決めたすべての性質について、新システムがそれぞれの受入条件を満たす」ことを表す。そして中央の \(\land\) は、その両方が必要であることを示す。
言葉に戻せば、正しいモダナイゼーションとは、旧システムをできるだけ忠実に再現することではない。保存すると判断した性質について必要な互換性を維持し、変更すると判断した性質について新しい目標を満たすことである。どの性質をどちらへ分類し、それぞれにどの \(R_i\) または \(A_j\) を与えるかを決められなければ、後続で仕様差分やテスト結果を得ても、その差を成功と失敗のどちらに分類すべきかを判定できない。
この分解を済ませると、次に必要なことも決まる。保存対象については、新旧の実装構造が異なっていても同じ性質を比較できる表現が必要になる。そこで、旧コードと新コードを直接比較するのではなく、双方から共通の意味表現を取り出して比較する検証へ進む。
3. 異なる実装を共通の意味表現へ写して比較する
保存する性質を決めたとしても、旧コードと新コードの差分をそのまま比較すればよいとは限らない。モダナイゼーションでは、保存したいのは実装形式ではなく、その実装が実現している意味だからである。COBOL から Java へ移す場合、巨大な手続き型プログラムを複数のサービスへ分割する場合、データベース中心の同期処理をイベント駆動へ変える場合では、同じ業務規則を実現していても、関数、クラス、データ構造、呼び出し順序、プロセス境界は大きく変わる。
例えば、旧システムでは「注文確定」という一つの処理の中で、在庫確認、金額確定、決済、在庫減算、履歴保存を順番に実行していたとする。新システムでは、注文サービス、在庫サービス、決済サービスがそれぞれ別のプロセスとして動作し、イベントを介して状態を更新するかもしれない。旧コードの一つの関数に対応する新コードの一つの関数は存在せず、旧コードの 1 行と新コードの 1 行を対応付けることもできない。
しかし、実装の対応が失われても、業務上の意味まで失われたとは限らない。注文を確定できる前提条件、在庫不足時に確定を拒否する規則、決済失敗時に成功状態へ進めない条件、確定済み注文について在庫数量を減らす規則などは、実装形式が変わっても比較できる。コードの構造が変わるほど、比較対象を構文から意味へ移す必要が生じる。
この違いを明確にするため、あるシステム \(C\) が持つ意味全体を \(\Sigma(C)\) と表す。\(\Sigma(C)\) は、一つの文書や一つの関数を意味するのではない。そのシステムが、どの入力と状態の下で、どの規則に従い、どの状態へ遷移し、どの出力や副作用を生むかという振る舞い全体を表す。
\[
\Sigma(C)
\]
例えば注文システムなら、通常時の注文確定だけでなく、在庫不足、決済失敗、重複要求、外部サービス停止などの条件まで含めた振る舞いが \(\Sigma(C)\) の一部になる。理想的には、旧システムと新システムの \(\Sigma\) を直接比較できればよい。しかし現実のシステムでは、その意味全体を有限の文書へ完全に展開することは難しい。入力空間、状態空間、外部依存、例外経路が大きく、実行時にしか現れない条件も存在するからである。
そこで、比較したい意味だけを取り出す抽象化を導入する。意味全体から比較に必要な情報を選択する操作を \(\alpha\) とし、実際に比較する仕様または意味モデルを \(S(C)\) とする。
\[
S(C) = \alpha \left( \Sigma(C) \right)
\]
この式には三つの段階がある。まず \(\Sigma(C)\) がシステムの意味全体を表す。次に \(\alpha\) が、その中から今回の検証で必要な性質を取り出す。最後に \(S(C)\) が、新旧比較へ実際に使う意味モデルになる。
例えば、ソースコードの変数名、クラス名、メソッド分割、内部ライブラリの種類は、業務意味を比較するだけなら \(\alpha\) によって捨てられる。一方、注文を確定できる条件、状態遷移、データ更新、例外条件は保存対象に関係するため \(S(C)\) に残す。この選別によって、実装形式が異なる二つのシステムを同じ比較面へ持ち込める。
比較用の意味モデル \(M\) を、例えば次の要素から構成する。
\[
M= \{ I,R,S_t,D,O,E,X \}
\]
| 記号 | 意味 | 注文処理での具体例 |
|---|---|---|
| \(I\) | 処理を開始できる入力と前提条件を表す。 | 注文番号が存在し、注文状態が未確定であり、要求された商品が注文に含まれていることを表す。 |
| \(R\) | 業務規則や判定規則を表す。 | 必要数量を満たす在庫がない商品を含む注文は確定できないことを表す。 |
| \(S_t\) | 処理前後の状態と、その遷移条件を表す。 | 未確定から確定済みへ遷移し、決済失敗時には失敗状態へ遷移することを表す。 |
| \(D\) | 永続データの意味と更新規則を表す。 | 注文確定後に対象商品の在庫数量を減算し、確定日時と注文履歴を保存することを表す。 |
| \(O\) | 処理結果として外部へ返す値を表す。 | 注文番号、確定金額、処理結果を返すことを表す。 |
| \(E\) | 異常条件と、そのときに許容される結果を表す。 | 決済に失敗した場合は注文確定成功として返さず、定義した失敗状態を返すことを表す。 |
| \(X\) | システム外部へ発生させる副作用を表す。 | 決済サービスへの要求、通知イベントの発行、外部監査ログの記録などを表す。 |
このモデルを使うと、旧システムが一つの関数で処理していたか、新システムが複数サービスで処理しているかという構造上の差をいったん脇へ置ける。比較するのは、「在庫不足時に確定を拒否するか」「決済失敗後にどの状態へ進むか」「確定時にどのデータを更新するか」といった意味上の項目である。
旧システムと新システムについて、それぞれ同じ抽象化を行えば、比較対象は次の二つになる。
\[
S(C_{\mathrm{old}}) = \alpha \left( \Sigma(C_{\mathrm{old}}) \right)
\]
\[
S(C_{\mathrm{new}}) = \alpha \left( \Sigma(C_{\mathrm{new}}) \right)
\]
そして、保存対象について必要な対応があるかを次の形で確認する。
\[
S(C_{\mathrm{old}}) \stackrel{?}{\equiv} S(C_{\mathrm{new}})
\]
この \(\equiv\) は、生成された仕様書の文章、章構成、項目順が同じであることを意味しない。比較したいのは文書表現ではなく、その文書が表している意味である。例えば、旧仕様に「在庫数が要求数未満なら注文を確定しない」と書かれ、新仕様に「利用可能在庫が注文数量を満たさない場合は確定処理を拒否する」と書かれていても、同じ条件と結果を表しているなら意味上は対応する。
逆に、文章表現が似ていても、条件の境界が異なれば等価とは言えない。「在庫数が要求数未満」と「在庫数が要求数以下」では、在庫数と要求数が等しい場合の挙動が変わる。仕様比較を有効な検証にするには、自然言語の類似度ではなく、条件、状態、結果の対応関係まで比較する必要がある。
この違いは、仕様書を比較に使うときに特に重要になる。人間向け文書として読みやすいことと、機械的または半機械的に意味を比較できることは同じではない。例えば次の二つの記述を考える。
| 表現 | 内容 |
|---|---|
| 旧仕様 | 在庫が注文数量以上存在する場合に限り注文を確定する。 |
| 新仕様 | 利用可能在庫が要求数に満たない場合は注文確定を拒否する。 |
文章としては異なるが、在庫数量を \(q_s\)、注文数量を \(q_o\) とすれば、旧仕様は次の条件である。
\[
q_s \ge q_o
\]
新仕様の拒否条件は、
\[
q_s < q_o
\]
であり、その否定条件は、
\[
\neg \left( q_s<q_o \right) \iff q_s\ge q_o
\]
となる。このように、表面上は異なる記述でも、同じ論理条件へ正規化すれば意味上の一致を確認できる。共通意味表現を導入する価値は、単に仕様書同士を並べることではなく、異なる記述や実装を比較可能な条件へ変換できる点にある。
この構造は、実際のソフトウェアモダナイゼーション研究にも現れる。Iosif-Lazăr らは、構造化された C++ コードを宣言的な構成モデルへ変換する産業事例で、元のコードと変換後モデルが同じ構成結果を許すことを正しさの基準とし、各変換結果を translation validation と記号実行で検証した[5]。元コードと生成されたモデルの表現形式は異なるが、両者が許容する結果を共通の意味条件へ落とすことで比較している。
この事例から一般化できるのは、「仕様書を生成すること」そのものが検証になるわけではないという点である。検証として価値を持つのは、旧実装と新実装から同じ観点の意味を取り出し、その意味について差異を判定できる構造を作ることである。
人間が読む仕様書は、その意味モデルを表現する一つの媒体になり得る。しかし検証上は、中間表現として捉える方が役割を明確にできる。旧コード、新コード、場合によっては設計書やテスト結果といった異なる成果物を、同じ意味項目へ写し、その間に矛盾がないかを確認するための比較面である。
この方法を使えば、実装構造が変わるほど比較不能になるという問題を避けられる。ソースコード上の対応が消えても、保存すべき意味について対応を取り直せるからである。一方で、意味全体 \(\Sigma(C)\) から比較モデル \(S(C)\) を作るときには、必ず抽象化 \(\alpha\) が入る。何を残し、何を捨てるかを選んでいる以上、抽象化で失われた情報は後から仕様比較だけでは確認できない。
共通意味表現は、異なる実装を比較可能にするために必要であると同時に、検証できる範囲を限定する境界にもなる。次に確認すべきなのは、この意味モデルの一致がどこまで変換の正しさを支えられ、どこから先は別の検証が必要になるかである。
4. 仕様比較は非常に良い検証レイヤーである
変換後の成果物について、変換前と変換後の意味を比較して正しさを確認する発想は、コンパイラ分野で translation validation として研究されてきた。Pnueli、Shtrichman、Siegel は、コード生成器やコンパイラそのものが、対象となるすべての入力に対して常に正しい変換を行うことを先に証明するのではなく、実際に一回の変換が行われるたびに、その変換結果が元のプログラムの意味を保存しているかを検証する考え方を示した[6]。
ここで区別すべきなのは、「変換器が正しい」という命題と、「今回得られた変換結果が正しい」という命題である。旧プログラムを \(C_{\mathrm{old}}\)、変換器を \(T\)、変換後プログラムを \(C_{\mathrm{new}}\) とすると、変換そのものは次のように表せる。
\[
C_{\mathrm{new}} = T(C_{\mathrm{old}})
\]
変換器そのものを証明する方法では、対象とする入力領域 \(D\) のすべてについて、\(T\) が意味保存を行うことを示す。意味を \(\Sigma\) で表すなら、理想化すると次のような命題になる。
\[
\forall C\in D,\quad \Sigma(T(C)) \equiv \Sigma(C)
\]
この式が成立すれば、前提条件の範囲内にある任意のプログラム \(C\) を \(T\) で変換しても、その意味が保存されるという一般的な保証を与えられる。変換規則が十分に形式化され、対象範囲も明確である場合には強い保証になる。
一方、translation validation では、変換器 \(T\) 全体についてこの普遍命題を証明することを必須としない。実際に得られた一組の旧新成果物について、必要な意味保存条件が成立するかをその都度確認する。
\[
C_{\mathrm{new}} = T(C_{\mathrm{old}})
\]
という変換が得られたあとで、
\[
V \left( C_{\mathrm{old}}, C_{\mathrm{new}} \right) = \mathrm{true}
\]
となるかを検証する。\(V\) は変換結果を検査する検証器である。ここで確認しているのは、「\(T\) は常に正しい」という命題ではなく、「今回の \(C_{\mathrm{old}}\rightarrow C_{\mathrm{new}}\) は、定義した保存条件を満たした」という命題である。
| 方式 | 証明・検証する対象 | 得られる保証 | 適用上の特徴 |
|---|---|---|---|
| 変換器そのものを証明する | 変換器 \(T\) が、定義された入力範囲で意味保存を行うことを証明する。 | 前提条件の範囲内では、個々の変換結果へ一般的な保証を与えられる。 | 変換規則と意味論を十分に形式化できる場合に適している。 |
| 変換結果ごとに検証する | 実際に得られた \(C_{\mathrm{old}}\rightarrow C_{\mathrm{new}}\) が保存条件を満たしたかを検証する。 | 検証に成功した個々の成果物について、定義した条件の範囲で保証を与えられる。 | 変換方法や対象が案件ごとに異なっていても、成果物単位で適用できる。 |
Necula は GNU C コンパイラの最適化について、この考え方を実装へ持ち込んだ。最適化前後の中間表現を比較し、コンパイラが行った各変換について意味保存が成立しているかを検証する仕組みを構築した[7]。コンパイラ全体のすべての最適化について事前に完全証明するのではなく、実際に生成された変換結果を検証対象にすることで、既存の複雑なコンパイラへ検証を追加できる。
Alive2 はこの方向をさらに発展させ、LLVM IR の最適化について SMT ソルバーを利用した bounded translation validation を実装している[8]。例えば最適化前の式と最適化後の式について、定義された意味論の下で、後者が前者では許されない振る舞いを新たに導入していないかを調べる。実際の LLVM が生成する変換を対象に検査できるため、理論上の変換規則だけでなく、実装された最適化処理に含まれる不具合も検出できる。
ただし、Alive2 の bounded という語が示すように、この方法にも検証範囲がある。例えばループ展開などについて探索範囲へ上限を置けば、その上限を超えた実行でのみ現れる差異は検出できない場合がある。translation validation は「検証器を通ったから数学的にあらゆる振る舞いが等価である」という方式ではなく、検証器が形式化し探索できる範囲で変換結果を検査する方式である。この制約は、後でモダナイゼーションへ適用するときにもそのまま残る。
一方、CompCert は別の保証の作り方を採っている。CompCert では Coq を用いて、コンパイラの各変換段階がソースプログラムの意味を保存することを形式証明し、最終的な生成コードまで意味保存をつなげている[9]。概念的には、CompCert が「変換器を信頼できる根拠を構築する」方向であるのに対し、translation validation は「変換器を全面的には信頼せず、出力された成果物を別途検査する」方向にある。
この違いはモダナイゼーションを考えるときに大きい。コンパイラでは、入力言語、出力言語、変換規則、意味論を比較的明確に定義できる。一方、既存業務システムのモダナイゼーションでは、対象ごとに利用言語、フレームワーク、データ構造、外部システム、暗黙の業務規則が異なる。さらに、一つの刷新の中でも、機械的なコード変換、設計変更、人手による修正、生成 AI による再実装が混在する場合がある。
このような工程全体について、「変換器 \(T\) は常に意味を保存する」と一つの形式体系で証明するのは難しい。そもそも \(T\) 自体が一つの固定プログラムではなく、複数のツール、人間の判断、生成処理、手作業の修正を含む工程になっている場合がある。
そこで、保証の単位を変換工程そのものから、実際に得られた成果物へ移す。旧システムから抽出した意味モデルを \(S(C_{\mathrm{old}})\)、新システムから抽出した意味モデルを \(S(C_{\mathrm{new}})\) とすれば、個々のモダナイゼーション結果について次を確認する。
\[
V_{\mathrm{spec}} = \left[ S(C_{\mathrm{old}}) \equiv S(C_{\mathrm{new}}) \right]
\]
\(V_{\mathrm{spec}}\) は、仕様または意味モデル上の検証結果を表す。このとき変換主体が何であったかは、比較そのものの前提ではなくなる。人間が書き換えたコードでも、決定的な変換ツールが生成したコードでも、生成 AI が作ったコードでも、最終的に同じ比較面へ写して保存対象を検査できる。
この構造には、モダナイゼーションで特に有用な性質がある。変換を実行する機構と、その変換を評価する機構を分離できることである。例えば生成 AI が旧コードを読み、新コードを生成したとしても、「生成 AI が高性能だから正しい」という信頼に依存する必要はない。生成された成果物から改めて意味モデルを作り、旧システム側の意味モデルと比較することで、生成工程の外側に検証面を置ける。
さらに、変換途中の実装形式へ依存しない。旧システムでは一つの関数だった処理が新システムでは五つのサービスへ分割されていても、注文確定条件、決済条件、在庫更新条件といった意味へ正規化できれば比較できる。モダナイゼーションによってコード差分が大きくなるほど、構文上の一致ではなく意味上の一致を検査するこの方式の価値が高くなる。
このため、旧コードから仕様を復元し、新コードからも同じ形式の仕様を作って比較する方法は、モダナイゼーションにおける非常に良い検証レイヤーと評価できる。特定の変換ツールが正しいことを信頼の起点にせず、実際に得られた変換結果について、保存すべき意味が残っているかを確認できるからである。
ただし、translation validation から導ける保証も、検証器が確認した命題の範囲を超えない。モダナイゼーションで仕様比較を行った場合、得られる証拠は「比較用の意味モデル上で、定義した保存条件が成立した」というものである。
\[
V_{\mathrm{spec}} = \mathrm{true}
\]
だからといって、直ちに、
\[
\Sigma(C_{\mathrm{old}}) = \Sigma(C_{\mathrm{new}})
\]
とは言えない。前章で定義した \(S(C)=\alpha(\Sigma(C))\) には抽象化 \(\alpha\) が含まれており、意味全体から比較対象だけを取り出しているからである。
つまり、この検証レイヤーの強みと限界は同じ構造から生じる。実装詳細を捨てるから、全く異なる実装を比較できる。一方で、捨てた情報については比較できない。仕様比較を強い検証として利用するには、「一致した」という結果だけを見るのではなく、その比較モデルが何を表現し、何を表現していないかまで含めて保証範囲を定義する必要がある。
仕様比較をモダナイゼーションの等価性証明そのものとみなせない理由は、ここから具体的に導ける。意味モデルへの抽象化で失われる情報、同じ抽出器による共通の誤り、実行環境に依存する振る舞いなどは、仕様比較が成功しても残り得る。次に、この検証レイヤーが見落とし得る差異を分解する。
5. 仕様が一致しても、実装が等価だとは限らない
前章までで、新旧システムを共通の意味表現へ写して比較する方法が、モダナイゼーションにおける有効な検証レイヤーになることを確認した。しかし、この方法から導ける保証には明確な境界がある。仕様比較で一致したという事実は、「比較に用いた意味モデルの範囲で差異が検出されなかった」ことを示すのであって、旧システムと新システムのあらゆる振る舞いが等価であることを直接意味しない。
この境界が生じる原因は一つではない。第一に、コードから意味モデルへ変換するときに情報を捨てる。第二に、その意味モデルを作る抽出器自体が誤る可能性がある。第三に、静的なモデルでは実行環境との相互作用をすべて表せない。第四に、旧システムで実際に依存されている挙動と、文書や設計者が想定した仕様が一致しないことがある。さらに、データ移行や性能、可用性、セキュリティには、機能仕様とは別の正しさが存在する。
これらは同じ問題の言い換えではない。どの失敗経路によって仕様比較が誤った安心を与えるのかを分けて考える必要がある。
5.1 抽象化で捨てた情報は比較結果から復元できない
仕様比較の最も基本的な限界は、比較可能にするための抽象化そのものから生じる。第 3 章では、システム全体の意味を \(\Sigma(C)\)、そこから比較対象となる意味だけを取り出す抽象化を \(\alpha\)、実際に比較する意味モデルを \(S(C)\) として、次のように定義した。
\[
S(C) = \alpha \left( \Sigma(C) \right)
\]
\(\Sigma(C)\) には、入力、状態遷移、データ更新、外部副作用、実行順序、障害時の振る舞いなど、システムが持つ意味全体が含まれる。一方、\(S(C)\) はそのうち比較に必要だと判断した情報だけを保持する。
この情報削減は欠点ではなく、仕様比較を成立させるために必要な操作である。旧システムの変数名、クラス構造、関数分割、新システムのサービス構成といった実装差をすべて残せば、異なる技術で作られた二つのシステムを同じ座標系へ持ち込めない。意味を比較するためには、比較対象ではない構造を捨てる必要がある。
しかし、抽象化によって捨てた情報の中に、本来は保存すべき性質が混ざれば、その差異も消える。異なる二つの意味を \(m_1\)、\(m_2\) とする。
\[
m_1 \neq m_2
\]
それにもかかわらず、抽象化後に、
\[
\alpha(m_1) = \alpha(m_2)
\]
となる場合がある。\(\alpha\) が複数の異なる意味を同じ表現へまとめる多対一の写像だからである。
この性質を旧新システムへ当てはめると、本来の意味が異なっていても、比較モデルだけは一致する場合がある。
\[
\Sigma(C_{\mathrm{old}}) \neq \Sigma(C_{\mathrm{new}})
\]
であるにもかかわらず、
\[
S(C_{\mathrm{old}}) = S(C_{\mathrm{new}})
\]
となり得る。つまり、仕様モデルが一致していても、意味全体が異なる場合がある。
\[
S(C_{\mathrm{old}}) = S(C_{\mathrm{new}}),\qquad \Sigma(C_{\mathrm{old}}) \neq \Sigma(C_{\mathrm{new}})
\]
具体例として、注文確定と在庫減算を考える。仕様モデルに次の二つだけが書かれているとする。
| 仕様項目 | 内容 |
|---|---|
| 注文確定条件 | 必要な在庫が存在する場合に注文を確定できる。 |
| 在庫更新 | 注文確定後に対象商品の在庫数量を減算する。 |
旧システムでは、注文確定と在庫減算を一つのデータベーストランザクションで処理しているとする。新システムでは、注文確定を先にコミットし、その後に別処理として在庫を減算するとする。正常に最後まで処理された場合だけを見れば、どちらも「注文を確定し、在庫を減らす」ので、仕様モデルは一致する。
しかし、注文確定の直後、在庫減算の直前で障害が起きると差が現れる。旧システムはトランザクション全体を取り消し、注文も在庫も元の状態へ戻る。新システムでは、注文だけ確定済みで在庫が減っていない状態が残る可能性がある。
つまり、正常系の業務規則は同じでも、障害時の状態遷移は異なる。仕様モデルにトランザクション境界が含まれていなければ、この差は比較できない。
同じ構造は、次のような性質にも現れる。
| 抽象化から落ちやすい性質 | 差異が現れる例 |
|---|---|
| ロック | 同時更新時に一方では整合性を保ち、もう一方では 更新消失が発生する。 |
| 処理順序 | 決済後に在庫を確保するか、在庫確保後に決済するかで障害時の状態が変わる。 |
| タイムアウト | 外部サービスが遅延したとき、一方だけ再試行や中断が発生する。 |
| リトライ | 非冪等な外部処理が複数回実行される可能性が生じる。 |
| 数値表現 | 浮動小数点と十進数型の違いによって、境界値で丸め結果が変わる。 |
| NULL | 未設定、空文字列、ゼロ値を同一視するかどうかで業務判定が変わる。 |
| 時刻 | タイムゾーンや夏時間の扱いによって日付境界の判定が変わる。 |
| 外部副作用 | 通知、決済、イベント発行の回数や順序が異なる。 |
比較可能な範囲を \(\mathrm{Scope}(S)\) とすると、仕様比較が直接保証できる範囲は、このモデルが保持する情報の範囲を超えない。
\[
\mathrm{VerificationScope}_{\mathrm{spec}} \subseteq \mathrm{Scope}(S)
\]
この式は、「仕様書をもっと詳しくすればすべて解決する」という意味でもない。仕様を詳細化すれば \(\mathrm{Scope}(S)\) を広げることはできる。しかし、項目数を増やしただけで、必要な性質がすべて入ったと保証できるわけではない。比較モデルが何を表現し、何を捨てたかを明示して初めて、仕様一致という結果の保証範囲を説明できる。
5.2 同じ抽出器を使うと共通モードの誤りが起こり得る
抽象化する項目を適切に選んでも、もう一つの誤りが残る。コードから意味モデルを作る抽出器自体が、コードを正しく理解するとは限らない。
理想的に取り出したい意味モデルを \(S^{*}(C)\)、実際の解析器や生成 AI が出力した意味モデルを \(\widehat{S}(C)\) とする。
抽出器が完全なら、すべての対象について、
\[
\widehat{S}(C) = S^{*}(C)
\]
となる。しかし現実には、条件分岐を読み落とす、例外経路を通常経路へ統合する、暗黙のデフォルト値を見落とす、非同期処理の完了条件を誤解するといった誤りが起こり得る。
ここで、新旧システムの仕様を同じ抽出器で作る場合を考える。同じ解析規則、同じ生成 AI、同じプロンプト、同じ後処理を双方へ使えば、二つの抽出誤りは独立とは限らない。同じ種類のコードを同じ理由で誤解する可能性があるからである。
本来は、
\[
S^{*}(C_{\mathrm{old}}) \neq S^{*}(C_{\mathrm{new}})
\]
であるにもかかわらず、抽出結果では、
\[
\widehat{S}(C_{\mathrm{old}}) = \widehat{S}(C_{\mathrm{new}})
\]
となる場合がある。この状態を偽一致と考えると、事象 \(F\) は次のように表せる。
\[
F = \left\{ \widehat{S}(C_{\mathrm{old}}) = \widehat{S}(C_{\mathrm{new}}) \right\} \land \left\{ S^{*}(C_{\mathrm{old}}) \neq S^{*}(C_{\mathrm{new}}) \right\}
\]
例えば、旧コードでは「決済成功後に在庫を確定する」、新コードでは「在庫確定後に決済する」とする。この違いは、決済失敗時や在庫確保失敗時の状態へ影響するため、保存対象に含めるべき意味差かもしれない。
しかし抽出器が、どちらのコードからも単に「決済処理と在庫更新を行う」という仕様だけを生成したとする。
| 対象 | 実際の意味 | 抽出結果 |
|---|---|---|
| 旧システム | 決済成功後に在庫を確定する。 | 決済処理と在庫更新を行う。 |
| 新システム | 在庫確定後に決済する。 | 決済処理と在庫更新を行う。 |
この場合、仕様比較は一致する。しかし、新旧それぞれについて独立に正しさが確認されたわけではない。同じ抽出器が、意味のある順序差を双方から消しただけである。
この性質は、検証工程を分離しただけでは自動的に解消しない。コード変換と仕様抽出を別工程にしても、その二つが同じ基盤モデル、同じ解析規則、同じ誤った前提を共有すれば、誤りも相関する可能性がある。
仕様比較をより強い証拠にするには、同じ誤りを共有しにくい経路を追加する必要がある。例えば、重要な状態遷移だけは人間が確定した要件と照合する、静的解析とは別に実行結果を比較する、トランザクション境界をデータベース側から検査する、といった方法である。
ここで求められる独立性は、「別のツールを二つ使えばよい」という形式的なものではない。二つの検証経路が、同じ失敗原因によって同時に誤る可能性をどれだけ減らせるかが重要になる。
5.3 静的な仕様は実行環境との相互作用を完全には表さない
抽出した仕様がコードの意味を正しく表していたとしても、実際のシステム挙動には実行環境が関与する。入力を \(x\)、実行環境を \(e\)、その条件で外部から観測される振る舞いを \(B(C,x,e)\) とする。
\[
B(C,x,e)
\]
\(e\) には、データベースの分離レベル、外部 API の応答、スレッドやプロセスの実行順序、ネットワーク遅延、利用可能な CPU やメモリー、時刻、ファイルシステムの性質などが含まれる。
同じコードであっても、\(e\) が変われば結果が変わることがある。モダナイゼーションでは実行基盤そのものを変える場合が多いため、この影響は無視できない。
仕様モデルが一致していても、
\[
S(C_{\mathrm{old}}) = S(C_{\mathrm{new}})
\]
ある入力 \(x\) と環境 \(e\) について、
\[
B(C_{\mathrm{old}},x,e) \neq B(C_{\mathrm{new}},x,e)
\]
となる可能性がある。
例えば、旧システムでは一つのアプリケーションプロセスが一台のデータベースへ順番に更新していたとする。この構造では、同じ顧客に対する二つの要求が事実上直列化されていたかもしれない。新システムを複数ノードへ分散し、同じ顧客情報を同時に更新できるようにすると、業務規則の仕様自体は変えていなくても、競合更新という新しい状態が現れる。
この差は、「顧客情報を更新できる」という静的な機能仕様だけでは見えない。どの順序で実行され、同時実行時にどの状態が許されるかまでモデルに含めるか、実環境で並行実行を観測する必要がある。
静的な仕様比較と実行時検証が補完関係にある理由はここにある。仕様比較は、コード全体から規則や状態遷移を広く抽出して比較できる。一方、実行時検証は、特定の入力、状態、環境の組み合わせで実際に起きた結果を直接観測できる。前者は広い意味構造を扱いやすく、後者は環境との相互作用を観測できる。
どちらか一方をもう一方の代替とみなすと、それぞれが観測できない領域が残る。
5.4 文書化された仕様と実際に依存されている挙動は一致しない
モダナイゼーションでは、比較対象となる「旧システムの正しい意味」をどこから取るかという問題もある。長期間運用されたシステムでは、文書に書かれた仕様、開発者が意図した仕様、現在のコードが実際に行っている処理、利用者や外部システムが依存している挙動が一致しないことがある。
文書化された仕様を \(M_{\mathrm{documented}}\)、設計上意図された仕様を \(M_{\mathrm{intended}}\)、実際に観測される振る舞いを \(B_{\mathrm{actual}}\) とすると、次のような関係が成立し得る。
\[
M_{\mathrm{documented}} \neq B_{\mathrm{actual}}
\]
さらに、
\[
M_{\mathrm{intended}} \neq B_{\mathrm{actual}}
\]
となる場合もある。
例えば、本来は入力エラーとするはずの文字列を、旧実装が長年にわたり自動補正していたとする。設計書には補正処理が書かれておらず、開発者から見れば不具合に近い挙動かもしれない。しかし外部システムがその補正を前提に不正確な値を送り続けているなら、新システムで突然エラーへ変更すると業務障害になる。
このとき選択肢は少なくとも三つある。
| 判断 | 意味 | 必要な対応 |
|---|---|---|
| 保存する | 現行利用側との互換性を優先して旧挙動を残す。 | 旧挙動を保存対象として明示し、仕様とテストへ取り込む。 |
| 段階的に廃止する | 一時的に互換性を維持しながら利用側を修正する。 | 移行期間、警告、利用側改修、廃止条件を定義する。 |
| 修正する | 旧挙動を不具合として扱い、新システムでは正しい仕様へ変える。 | 旧新差を意図的変更として管理し、新しい受入条件を定義する。 |
コードから仕様を復元する技術は、このような実挙動を発見するために有用である。文書にない分岐や例外処理を、コードという実装事実から取り出せるからである。しかし、抽出された挙動が将来も保存すべきかどうかは、抽出処理だけでは決められない。
既稿で整理したように、ここには仕様選択の問題が残る[4]。業務上の意味、利用側の依存、制度や契約上の要件、障害リスク、移行コストを踏まえて、「存在する挙動」と「保存する仕様」を分ける必要がある。
この違いを無視すると、二つの逆方向の失敗が起こる。一つは、旧コードに存在したという理由だけで不要な負債まで忠実に移植すること。もう一つは、文書にないという理由だけで、実際には利用側が依存している互換動作を削除することである。
5.5 仕様比較の一致はデータ移行や非機能品質を自動的には含まない
仕様比較でどこまで保証できるかは、「仕様」という語に何を含めたかにも左右される。例えば、コードから業務規則だけを抽出した機能仕様が一致したとしても、データ移行、性能、可用性、セキュリティまで一致または改善したことにはならない。
請求処理の計算式が旧新で一致していても、移行時に顧客と契約の対応関係を一部誤れば、正しい計算式を誤った顧客データへ適用することになる。処理結果が同じでも、旧システムが 200 ミリ秒で返していた処理に 5 秒かかるようになれば、オンライン処理として成立しない可能性がある。認証結果が旧システムと同じでも、旧システム自体が現在のセキュリティ要求を満たしていないなら、一致は成功条件にならない。
この違いを整理すると、仕様比較が対象とする意味と、モダナイゼーション全体で必要な検証対象には次のような関係がある。
| 検証対象 | 仕様比較だけで確認できる範囲 | 別途必要になる検証 |
|---|---|---|
| 業務規則 | 意味モデルへ十分に表現されていれば、新旧の規則差を比較できる。 | 境界条件や実環境での結果を実行試験で補完する。 |
| データ移行 | データ意味や変換規則をモデル化すれば一部を比較できる。 | 実データ件数、参照整合性、不変条件、変換後内容を検証する。 |
| 性能 | 目標値を仕様として記述することはできる。 | 実際の負荷条件で応答時間、処理量、資源使用量を測定する。 |
| 可用性 | 障害時の期待動作を仕様化できる。 | 障害注入、切り替え、復旧などを実環境で確認する。 |
| セキュリティ | 認証、認可などの要求を意味モデルへ含められる。 | 脅威分析、構成確認、依存関係検査、脆弱性検証などを行う。 |
この表から分かるのは、仕様比較が狭いということではない。意味モデルへ何を含めるかによって、仕様比較で扱える対象は広げられる。しかし、性能なら実際に時間を測る必要があり、データ移行なら移行されたデータそのものを検査する必要がある。ある性質を文章やモデルへ記述できることと、その性質が実システムで成立したことを確認することは別である。
そのため、仕様比較を中心的な検証レイヤーとして採用しても、モダナイゼーション全体を一つの仕様一致判定へ集約することはできない。
5.6 仕様比較が保証する範囲を限定して表現する
ここまでの失敗経路をまとめると、仕様比較について「一致した」「一致しなかった」という二値だけを報告するのでは不十分である。少なくとも、何を比較モデルへ含めたか、どの抽出器を使ったか、どの比較関係を検査したか、どの性質を別の検証へ回したかを併せて示す必要がある。
仕様比較による検証結果を \(V_{\mathrm{spec}}\) とすると、次のように書くことができる。
\[
V_{\mathrm{spec}} = \mathrm{true}
\]
この一つの値だけから、
\[
\Sigma(C_{\mathrm{old}}) = \Sigma(C_{\mathrm{new}})
\]
を導くことはできない。\(V_{\mathrm{spec}}\) が成立するのは、抽象化 \(\alpha\)、抽出器 \(\widehat{S}\)、比較規則、対象とした性質の集合という前提の上だからである。
より正確には、仕様比較で主張できるのは、「定義した意味モデルと比較規則の範囲で、保存対象について差異が検出されなかった」ということである。
この限定は、仕様比較の価値を弱めるものではない。むしろ、何を保証したのかを明確にすることで、仕様比較を他の検証と正しく組み合わせられるようになる。
仕様比較は、実装構造が大きく変わるモダナイゼーションでも、新旧を意味レベルで比較できるという点で強い。一方、抽象化で落ちた情報、抽出器が共通して見落とした差異、実行環境との相互作用、暗黙の既存挙動、データや非機能品質は、その比較結果の外側に残る。
このため、仕様比較を等価性証明そのものとして扱うのではなく、何を保存したかを確認する一つの強い証拠として位置づける必要がある。次の段階では、仕様比較とは異なる観測経路として、旧システムと新システムを実際に動かし、その振る舞いを比較する。
6. 実行結果を新旧で比較する検証が別に必要になる
仕様比較では、コードから取り出した意味モデルを新旧で比較する。これに対して実行比較では、旧システムと新システムを実際に動かし、そのとき外部から観測された振る舞いを比較する。前章で見たように、仕様モデルには抽象化による情報損失があり、実行環境との相互作用も完全には含められない。そこで、仕様から意味を推定する経路とは別に、実際に発生した結果を直接観測する経路を持つ。
この考え方に近い代表的な方法が差分テスト（differential testing）である。McKeeman は、同じ入力を比較可能な複数の実装へ与え、その出力差や異常終了から不具合候補を検出する方法を整理した[10]。一つの実装について「正しい出力」を最初からすべて用意するのではなく、同じ問題を解く複数の実装の差を利用する。
モダナイゼーションでは、この構造を旧システムと新システムの比較へ使える。例えば同じ注文要求を両方へ与え、返却された注文番号や金額だけでなく、処理後のデータベース状態、発生したイベント、外部サービスへの呼び出し、例外まで比較する。旧新で同じ意味を保存する必要があるなら、観測可能な結果についても定義した対応関係が成立するはずである。
入力を \(x\)、システムを \(C\)、実行条件を \(e\) とし、その実行から観測できる結果を \(B(C,x,e)\) とする。
\[
B(C,x,e)
\]
\(e\) は、データベースの初期状態、外部サービスの応答、同時実行数、時刻、利用可能な資源など、結果へ影響する実行条件を表す。同じ入力 \(x\) だけを与えても、初期状態や外部環境が違えば比較条件が揃わないため、実行比較では \(x\) と \(e\) の両方を管理する必要がある。
さらに、\(B(C,x,e)\) を一つの返却値だけで表す必要はない。観測対象を複数の成分に分解できる。
\[
B(C,x,e) = \left( O, D’, E, X \right)
\]
\(O\) は外部出力、\(D’\) は処理後の永続状態、\(E\) は例外や終了状態、\(X\) は外部副作用を表す。例えば注文処理なら、HTTP のレスポンスが同じでも、旧システムだけ通知イベントを 1 回送り、新システムが 2 回送っていれば、振る舞い全体は同じではない。
| 観測対象 | 比較内容 | 差異が問題になる例 |
|---|---|---|
| 返却値 | 金額、状態、エラーコードなどの外部出力が、保存条件として定めた関係を満たすことを確認する。 | 旧システムでは税額が 1,100 円なのに、新システムでは丸め順序の違いで 1,099 円になる。 |
| 永続状態 | 処理後の注文、在庫、履歴、残高などが意味上対応することを確認する。 | レスポンスは成功でも、新システムだけ在庫減算が行われていない。 |
| 例外・終了状態 | 異常入力や外部障害で、許容されたエラーや状態遷移になることを確認する。 | 旧システムは決済失敗として終了するが、新システムは注文成功として確定する。 |
| 外部副作用 | 決済、通知、イベント発行などが必要な回数と順序で行われることを確認する。 | リトライ処理によって、新システムだけ決済要求を重複送信する。 |
ここでも、比較条件は常に単純な完全一致とは限らない。例えば新システムで内部 ID の形式を変更した場合、返却された ID 文字列は旧システムと一致しない。それでも、その ID が同じ業務上の対象を識別し、後続操作に使えるなら互換性を保っている場合がある。
そこで、実行結果の比較にも、観測対象ごとの関係 \(R_B\) を置く方が正確である。
\[
R_B \left( B(C_{\mathrm{old}},x,e), B(C_{\mathrm{new}},x,e) \right)
\]
\(R_B\) は、旧新の観測結果について成立すべき関係を表す。金額なら一致、識別子なら対応表を介した同一対象性、イベントなら種類と回数の一致、性能まで含めるなら許容範囲内というように定義できる。
理想的には、入力と実行条件の全領域についてこの関係を確認したい。入力領域を \(D\)、実行条件の領域を \(E\) とすると、保存対象について完全な動的等価性を主張するには、概念的には次が必要になる。
\[
\forall x\in D,\; \forall e\in E,\quad R_B \left( B(C_{\mathrm{old}},x,e), B(C_{\mathrm{new}},x,e) \right)
\]
しかし、現実のシステムで \(D\times E\) のすべてを実行することは通常できない。入力値だけでも膨大であり、そこへ初期データ、障害条件、同時実行数、外部サービス応答などを組み合わせれば、状態空間はさらに増える。
実際に確認できるのは、選択した有限のテスト集合である。入力と実行条件の組を、
\[
T \subset D\times E
\]
とする。実行比較で直接確認できるのは、次の範囲である。
\[
\forall (x,e)\in T,\quad R_B \left( B(C_{\mathrm{old}},x,e), B(C_{\mathrm{new}},x,e) \right)
\]
この式が示しているのは、実際に試した条件について新旧の関係を確認したということである。未実行の条件についてまで同じ関係が成立すると直接証明したわけではない。一般化して書けば、確認できた命題は次の範囲に限定される。
\[
\forall (x,e)\in T,\quad P(x,e)
\]
例えば、通常の注文、在庫不足、決済失敗まで試してすべて一致したとしても、「同じ商品へ 100 件の注文が同時に到着する」という条件を試していなければ、その状況で競合が起きないとは言えない。仕様比較では並行処理のモデル化が不足し、実行比較でも同時実行試験をしていなければ、その差異は両方の検証から漏れることになる。
このため、テスト集合 \(T\) の設計自体が検証強度を左右する。正常系を多く並べるだけではなく、仕様比較で失われやすい境界を意識して条件を選ぶ必要がある。
| テスト条件 | 狙い |
|---|---|
| 境界値 | 数量、金額、日付、最大長など、条件分岐の境界で旧新の判定が変わらないかを確認する。 |
| 異常系 | 入力不正、外部サービス失敗、データ不整合などで同じ失敗規則を保つかを確認する。 |
| 途中障害 | トランザクション途中や外部呼び出し途中で失敗させ、状態の残り方を確認する。 |
| 並行実行 | ロック、競合、冪等性、イベント重複など、通常の逐次試験では見えない差異を確認する。 |
| 履歴データ | 現行システムで実際に発生した特殊な入力や過去の不具合条件を再現し、互換性を確認する。 |
実行比較には、もう一つ根本的な問題がある。結果を観測できることと、その結果を正しいと判定できることは同じではない。Weyuker は、出力の正しさを判定する正解判定基準（オラクル）が存在しない、または判定に必要な計算が現実的でないプログラムを論じた[11]。Barr らも、テスト実行結果と「期待される正しい結果」をどのように結び付けるかという オラクル問題を体系的に整理している[12]。
モダナイゼーションでは、旧システムそのものを正解判定基準として使えるように見える。旧システムへ入力 \(x\) を与えた結果を、
\[
O(x) = B(C_{\mathrm{old}},x,e)
\]
として、新システムが同じ結果を返すか確認すればよいからである。この方法は、互換性の確認には非常に有効である。期待値を人手で大量に作らなくても、現行システムの実挙動を基準にできる。
しかし、旧システムを正解判定基準にすると、旧システム自身の誤りも基準になる。本来修正すべき不具合について、
\[
B(C_{\mathrm{old}},x,e) = \mathrm{wrong}
\]
であれば、新システムへ単純な一致を要求すると、
\[
B(C_{\mathrm{new}},x,e) = \mathrm{wrong}
\]
まで要求することになる。
例えば、旧システムが特定の境界値だけ税率計算を誤っている場合、旧新の差分テストは、新システムがその不具合を修正すると「差異あり」と判定する。この差異は実装上は意図した改善である可能性がある。旧新比較で差を検出することと、その差を不具合と判定することは別工程になる。
この構造は、第 2 章で保存対象と変更対象を分けた理由へ戻る。保存対象 \(I_{\mathrm{preserve}}\) に属する性質なら、旧新の差は原則として調査対象になる。一方、意図的変更対象 \(I_{\mathrm{change}}\) に属する性質なら、新システムが旧挙動と異なること自体は問題ではなく、新しい受入条件 \(A_j\) を満たすかを確認する必要がある。
したがって、実行比較の判定も単純な、
\[
B(C_{\mathrm{old}},x,e) = B(C_{\mathrm{new}},x,e)
\]
だけでは表せない。保存対象については旧新の必要な関係を確認し、変更対象については新システムが新しい受入条件を満たすかを確認する。
実行比較を検証結果 \(V_{\mathrm{behavior}}\) とすると、その意味は概念的には次のように整理できる。
\[
V_{\mathrm{behavior}} = \left[ \bigwedge_{(x,e)\in T_{\mathrm{preserve}}} R_B \left( B(C_{\mathrm{old}},x,e), B(C_{\mathrm{new}},x,e) \right) \right] \land \left[ \bigwedge_{(x,e)\in T_{\mathrm{change}}} B(C_{\mathrm{new}},x,e) \in A_B \right]
\]
\(T_{\mathrm{preserve}}\) は旧新互換性を確認するテスト条件、\(T_{\mathrm{change}}\) は意図的変更について新しい受入条件を確認するテスト条件である。\(A_B\) は、新しい振る舞いとして許容される範囲を表す。
この式を言葉で表せば、実行比較では「旧システムと同じ結果だったか」だけを確認するのではなく、「保存すると決めた挙動は必要な意味で対応し、変更すると決めた挙動は新しい要求へ入ったか」を有限の実行条件について確認するということである。
既稿では、AI が用意されたテストをすべて通したとしても、そのテストが観測していない性質まで正しいとは主張できないことを整理した[13]。モダナイゼーションでも同じ制約がある。実行比較は、仕様抽出器とは異なる経路から実際の振る舞いを観測できるため、仕様比較を補完する強い証拠になる。しかし、有限のテスト集合、実行環境、観測項目、正解判定基準という前提の範囲を超えて、システム全体の完全な等価性を証明するものではない。
仕様比較と実行比較は、それぞれ異なる死角を持つ。仕様比較は広いコード範囲から意味を抽出できるが、抽象化で情報を失う。実行比較は実際の状態変化や副作用を直接観測できるが、実行した条件にしか証拠を与えられない。二つを重ねる価値は、同じことを二度確認するところにはなく、一方が見落とす差異をもう一方が観測できるところにある。
そして、実行結果が新旧で一致していても、もう一つ独立して確認しなければならない対象がある。モダナイゼーションでは、プログラムだけでなく、長年蓄積されたデータそのものを新しい構造へ移す場合がある。次に、コードの意味保存とは別に、データと状態の変換をどのように検証するかを見る。
7. データと状態はコードとは別の変換として検証する
モダナイゼーションでは、プログラムだけでなく、そのプログラムが処理してきた永続データも新しい構造へ移すことがある。テーブルを統合する、識別子体系を変更する、文字列で保持していた区分値を列挙型へ変える、日時をローカル時刻からタイムゾーン付きへ変える、複数テーブルへ分散していた情報を一つの集約へまとめるといった変更である。
このとき、コード変換とデータ変換は別の正しさを持つ。新しいプログラムが旧システムと同じ業務規則を正しく実装していても、その入力となる移行済みデータが壊れていれば、新システムは正しい業務状態から処理を開始できない。逆に、データが完全に移行されていても、新コードがそのデータを異なる意味で解釈すれば結果は変わる。
旧データ全体を \(D_{\mathrm{old}}\)、新データ全体を \(D_{\mathrm{new}}\)、データ移行処理を \(T_D\) とすると、移行は次の写像として表せる。
\[
T_D: D_{\mathrm{old}} \rightarrow D_{\mathrm{new}}
\]
実際の移行結果については、
\[
D_{\mathrm{new}} = T_D(D_{\mathrm{old}})
\]
となる。ここで確認したいのは、\(T_D\) がデータをコピーしたかどうかだけではない。旧データが持っていた業務上の意味を、新しい表現の中で必要な範囲だけ保存できたかである。
例えば、旧システムに顧客が 1 万件あり、移行後にも 1 万件の顧客が存在したとする。
\[
|D_{\mathrm{old}}| = |D_{\mathrm{new}}| = 10000
\]
件数だけを見れば一致している。しかし、顧客 A の契約が顧客 B へ誤って付け替えられていても件数は変わらない。請求履歴の金額が別の顧客へ紐付いていても、総レコード数だけなら一致する。つまり、件数一致はデータが失われていない可能性を確認する一つの指標にはなるが、意味保存の十分条件にはならない。
\[
|D_{\mathrm{old}}| = |D_{\mathrm{new}}|,\qquad \mathrm{Semantics}(D_{\mathrm{old}}) \neq \mathrm{Semantics}(D_{\mathrm{new}})
\]
この違いを扱うには、データが満たすべき不変条件を定義する必要がある。不変条件とは、保存形式が変わっても業務上成立していなければならない関係である。これを \(I_k\) とする。
\[
I_k(D)
\]
\(I_k\) は、データ集合 \(D\) が一つの条件を満たしているかを表す。例えば、次のような条件を置ける。
| 不変条件 | 意味 | 破壊された場合の影響 |
|---|---|---|
| 参照整合性 | すべての契約が実在する顧客へ紐付いている。 | 存在しない顧客を参照したり、別人の契約として処理されたりする。 |
| 一意性 | 同一の業務上の対象が重複して生成されていない。 | 同じ請求や注文を複数回処理する可能性が生じる。 |
| 金額整合性 | 保存対象となる金額や残高の意味が移行前後で対応している。 | 請求額、残高、集計結果が変わる。 |
| 履歴順序 | イベントや状態変更の時間的な順序が保存されている。 | 実際には解約後の契約が有効だったように再構成される可能性がある。 |
| 状態整合性 | 注文済み、決済済み、取消済みなどの状態間に矛盾がない。 | 同じ取引が同時に成功状態と取消状態を持つなど、後続処理が成立しなくなる。 |
表現形式が変わっても同じ不変条件をそのまま適用できるなら、旧新データについて次を確認できる。
\[
\forall k,\quad I_k(D_{\mathrm{old}}) \equiv I_k(D_{\mathrm{new}})
\]
例えば、「すべての契約は存在する顧客を参照する」という条件は、テーブル構造が変わっても意味自体は変わらない。旧側で成立していた参照整合性が、新側でも成立していることを確認できる。
ただし、モダナイゼーションではデータ表現自体を変更することが多いため、旧新へ同じ条件式をそのまま適用できるとは限らない。旧システムでは顧客 ID を数値で持ち、新システムでは UUID へ変える場合、ID の値そのものは一致しない。必要なのは、旧 ID と新 ID が同じ顧客を指していることである。
この場合、旧表現から新表現への意味変換を \(T_k\) とし、次のように比較する。
\[
I_k(D_{\mathrm{new}}) = T_k \left( I_k(D_{\mathrm{old}}) \right)
\]
ここで \(T_k\) は、データそのものを移す \(T_D\) とは役割が異なる。\(T_D\) は実際のデータ変換処理であり、\(T_k\) は旧側で表現されていた意味を、新しい表現へどう対応させるかを表す。
例えば、旧システムで金額を円単位の整数として、
\[
amount_{\mathrm{old}} = 1000
\]
と保持していたとする。新システムでは、通貨と最小単位を分けて、
\[
amount_{\mathrm{new}} = (\mathrm{JPY},1000)
\]
と保持するかもしれない。値の構造は一致しないが、金銭的な意味は同じである。この場合、旧表現を新表現へ写す関係を定義すれば、文字列表現や列構造に依存せず比較できる。
日時変換では、さらに注意が必要になる。旧システムがタイムゾーン情報を持たず、
\[
2026{-}09{-}08\ 10{:}00
\]
という値だけを保存していたとする。新システムで UTC へ正規化して、
\[
2026{-}09{-}08\ 01{:}00\mathrm{Z}
\]
と保存するなら、文字列は異なる。しかし旧値が日本標準時であるという前提を含めれば、同一時刻を表している。
一方、その前提を誤って UTC と解釈して変換すれば、9 時間ずれた時刻が生成される。レコード件数も変わらず、型変換も成功しているため、単純な移行完了判定では検出できない。データ移行の正しさは、形式変換が成功したことではなく、業務上の意味が新表現へ正しく写されたことにある。
状態を持つデータでは、個々の値だけでなく複数項目間の関係を見る必要がある。注文に、注文状態 \(s_o\)、決済状態 \(s_p\)、在庫引当状態 \(s_i\) があるとする。例えば「注文が確定済みなら決済も成功済みでなければならない」という業務条件を、次のように定義できる。
\[
s_o = \mathrm{confirmed} \Rightarrow s_p = \mathrm{paid}
\]
さらに、「確定済み注文には在庫が引き当てられている」という条件を加えるなら、
\[
s_o = \mathrm{confirmed} \Rightarrow \left( s_p = \mathrm{paid} \land s_i = \mathrm{reserved} \right)
\]
となる。移行後に各列の値が型として正しく変換されていても、この関係が崩れていれば業務状態は保存されていない。例えば注文状態だけが confirmed に移行され、在庫引当状態が未設定なら、新システムは開始直後から矛盾した状態を持つ。
このため、データ移行検証では単一の比較方法だけでは足りない。確認対象に応じて、件数、値、参照、集約値、不変条件を組み合わせる必要がある。
| 検証方法 | 確認できること | 単独では確認できないこと |
|---|---|---|
| 件数比較 | レコードの欠落や過剰生成の一部を検出できる。 | 各レコードの意味、参照関係、値の正しさは保証できない。 |
| チェックサム・ハッシュ | 変換しないデータ領域の内容差異を効率的に検出できる。 | 表現形式が変わるデータでは、そのまま比較できない場合がある。 |
| 対応表による照合 | 旧 ID と新 ID など、表現が変わった対象の対応を確認できる。 | 対応後の複数項目間の業務整合性までは自動的に保証しない。 |
| 集約値比較 | 残高総額、請求総額、件数分布など大域的な差異を検出できる。 | 相殺によって個別レコードの誤りが隠れる場合がある。 |
| 不変条件検証 | 参照整合性、状態関係、業務制約など意味上の破壊を検出できる。 | 定義していない不変条件については検出できない。 |
例えば請求総額だけを比較して、
\[
\sum amount_{\mathrm{old}} = \sum amount_{\mathrm{new}}
\]
となっても、二人の顧客の請求額が入れ替わっていれば総額は一致する。逆にレコード単位の金額がすべて一致しても、顧客との対応を誤れば業務上は破壊されている。複数の検証軸が必要になる理由は、各方法が異なる誤りしか観測できないためである。
Wei と Chen は、データ移行の正しさを検証する方法として checksum principle を提案し、移行元と移行先のデータ内容を検査する必要性を論じている[14]。チェックサムは、大量データについて変換前後の差異を効率的に検出する有力な方法である。ただし、モダナイゼーションでスキーマや値表現そのものを変更する場合には、単純なバイト列一致ではなく、変換後に対応する意味へ正規化してから比較する必要がある。
この点は、コードから仕様を抽出して比較する場合と構造が似ている。旧データと新データをそのまま比較できない場合、双方を比較可能な意味へ正規化する必要がある。ただし、コードの場合は実装構造を捨てて意味モデルを作るのに対し、データ移行では旧表現と新表現の対応規則を明示し、保存すべき値と関係を検証する。
データ移行の検証結果を \(V_{\mathrm{data}}\) とすると、概念的には、保存対象となる不変条件がすべて成立することとして表せる。
\[
V_{\mathrm{data}} = \bigwedge_{k\in K} R_k \left( I_k(D_{\mathrm{old}}), I_k(D_{\mathrm{new}}) \right)
\]
\(K\) は確認する不変条件の集合、\(R_k\) は旧新の不変条件の間に必要な関係である。表現が同じなら \(R_k\) は単純な等価性にできる。表現を変更したなら、対応変換を含んだ関係になる。
この式からも、データ検証の保証範囲は定義した \(K\) を超えないことが分かる。顧客と契約の対応を不変条件へ入れなければ、その破壊は検証対象にならない。データ移行でも、「すべて確認した」という曖昧な表現より、どの不変条件をどの方法で確認したかを明示する方が保証範囲を正確に表せる。
コードの仕様比較、実行結果の比較、データ移行の検証は、それぞれ別の対象を見ている。新旧コードの意味が対応し、同じテストで同じ結果が得られたとしても、移行データに破損があれば本番移行は失敗する。反対に、データが完全でも新コードの意味が変わっていれば正しくない。
このため、\(V_{\mathrm{spec}}\)、\(V_{\mathrm{behavior}}\)、\(V_{\mathrm{data}}\) は互いに代替できない。異なる失敗経路を閉じるための独立した検証義務として扱う必要がある。
そして、コードとデータの意味が保存されていても、まだモダナイゼーション全体の成功条件は満たし切れていない。同じ機能を実現していても、性能が大幅に低下したり、可用性が落ちたり、セキュリティ上の要求を満たさなかったりすれば、刷新の目的そのものを達成できない。次に、機能等価性では表現できない品質特性を検証対象へ加える。
8. 機能が同じでもモダナイゼーションが成功したとは限らない
旧システムと新システムが同じ入力に対して同じ業務結果を返したとしても、それだけでモダナイゼーションが成功したとは言えない。例えば、旧システムでは 300 ミリ秒で完了していた検索が新システムでは 5 秒かかる、単一障害から 1 分で復旧できていた処理が 30 分停止する、古い認証方式をそのまま再現した結果として現在求められるセキュリティ水準を満たさない、といった状態があり得る。機能的な結果が保存されていても、システムとして利用可能な条件まで保存または改善されているとは限らない。
この違いは、機能と品質特性が別の観測対象だから生じる。例えば注文 API が正しい金額を返すことは機能上の性質である。一方、その結果を何ミリ秒以内に返すか、障害時にどれだけ早く復旧できるか、どの程度の同時アクセスを処理できるか、不正利用をどのように防ぐかは別の性質である。同じ業務ロジックを実装していても、アーキテクチャ、配置、データベース、キャッシュ、ネットワーク構成が変われば、これらの性質は大きく変化する。
ISO/IEC 25010:2023 は、ソフトウェア製品の品質を一つの尺度ではなく、複数の品質特性から評価するモデルを定義している[15]。これは、システムの品質を「正しいか、正しくないか」という一つの軸だけでは表現できないことを意味する。また ATAM は、性能、可用性、セキュリティ、変更容易性などの品質属性が相互に影響することを前提に、アーキテクチャ上のトレードオフを分析する方法として設計されている[16]。
例えば、すべての要求について強い同期整合性を要求すれば、障害時にも一貫した状態を保ちやすくなる一方、複数拠点間の通信待ちによって応答時間が増える場合がある。キャッシュを増やせば読み取り性能を改善できるが、更新された値が一時的に反映されない可能性が生じる。サービスを細かく分割すれば変更単位を小さくできる一方、ネットワーク呼び出しと障害点が増える。品質特性は独立した数値ではなく、設計判断を介して相互に結び付いている。
この構造を表すため、システム \(C\) の品質を一つの値ではなく、複数の成分を持つベクトルとして表す。
\[
\mathbf{q}(C) = \left( q_1(C), q_2(C), \ldots, q_m(C) \right)
\]
\(\mathbf{q}(C)\) はシステム全体の品質状態、各 \(q_i(C)\) は一つの品質特性を表す。例えば、
\[
q_1 = q_{\mathrm{functional}}
\]
を機能的互換性、
\[
q_2 = q_{\mathrm{performance}}
\]
を性能、
\[
q_3 = q_{\mathrm{availability}}
\]
を可用性、
\[
q_4 = q_{\mathrm{security}}
\]
をセキュリティと考えることができる。
ここで重要なのは、新旧システムの品質ベクトル全体について単純な等価性を要求しないことである。
\[
\mathbf{q}(C_{\mathrm{new}}) \equiv \mathbf{q}(C_{\mathrm{old}})
\]
を一律に要求すると、性能やセキュリティを改善するモダナイゼーションまで「旧システムと違う」という理由で失敗扱いになる。必要なのは、第 2 章で整理した保存対象と変更対象の考え方を、品質特性にも適用することである。
例えば、業務機能については旧システムとの互換性を求めることができる。
\[
q_{\mathrm{functional}} (C_{\mathrm{new}}) \equiv q_{\mathrm{functional}} (C_{\mathrm{old}})
\]
ここでの \(\equiv\) は、業務結果、状態遷移、外部契約など、保存すると定めた機能について必要な関係が成立することを表す。
一方、性能については、旧システムとの一致よりも新しい目標値を満たすことが適切な場合がある。例えば、検索 API の 95 パーセンタイル応答時間を 500 ミリ秒以下にすることを目標とするなら、
\[
q_{\mathrm{performance}} (C_{\mathrm{new}}) \le 500\ \mathrm{ms}
\]
と定義できる。旧システムが 800 ミリ秒なら、新システムが 450 ミリ秒であることは旧システムとの非一致であるが、モダナイゼーションとしては成功である。
処理量については逆に、大きい方が望ましい尺度になる。1 秒当たりに処理できる要求数を処理量とするなら、
\[
q_{\mathrm{throughput}} (C_{\mathrm{new}}) \ge q_{\mathrm{throughput,target}}
\]
のような条件を置く。応答時間では上限、処理量では下限というように、同じ性能という分類の中でも評価関係は異なる。
可用性も同様である。例えば月間可用性の目標を 99.95% とするなら、
\[
q_{\mathrm{availability}} (C_{\mathrm{new}}) \ge 0.9995
\]
と表現できる。ただし、可用性を一つの数値だけで評価すると不十分な場合もある。平均復旧時間、障害検知時間、切り替え時間、単一障害点の有無など、可用性を構成する複数の性質をさらに分解する必要がある。
例えば平均復旧時間を \(MTTR\) とするなら、
\[
MTTR(C_{\mathrm{new}}) \le MTTR_{\mathrm{target}}
\]
という条件を別に置ける。年間の可用率が目標を満たしていても、一度の障害で数時間停止する設計が業務上受け入れられない場合があるためである。
セキュリティでは、旧システムとの一致がむしろ誤った目標になる場合がある。旧システムがパスワード認証だけを使っていたからといって、新システムでも同じ方式を採用すれば互換性が高い、とは評価できない。脅威、技術、規制、組織の要求が変われば、旧システムにはなかった制約を新システムへ追加する必要がある。
NIST SSDF は、ソフトウェア開発ライフサイクル全体へセキュリティ上のリスク低減策を組み込むことを求めている[17]。これは、セキュリティを完成後に「旧システムと同じか」と比較するだけの属性ではなく、設計、実装、依存関係、構成、検証を通じて満たすべき独立した条件として扱うことを意味する。
例えば認証方式について、新システムでは多要素認証を必須とするとする。この場合、旧システムとの関係は、
\[
q_{\mathrm{authentication}} (C_{\mathrm{new}}) \neq q_{\mathrm{authentication}} (C_{\mathrm{old}})
\]
であってよい。必要なのは、新しい受入条件 \(A_{\mathrm{authentication}}\) に入ることである。
\[
q_{\mathrm{authentication}} (C_{\mathrm{new}}) \in A_{\mathrm{authentication}}
\]
この違いは、モダナイゼーション全体を「旧新等価性」という一語で評価できないことを示している。
| 性質 | 旧システムとの関係 | 代表的な判定条件 |
|---|---|---|
| 業務機能 | 保存対象について互換性を求める。 | 同じ業務条件に対して必要な結果と状態遷移が対応する。 |
| 応答時間 | 旧値との一致ではなく目標以下を求める。 | 95 パーセンタイルが 500 ミリ秒以下などの条件を満たす。 |
| 処理量 | 旧値以上、または新しい目標以上を求める。 | 1 秒当たりの処理件数が要求値以上になる。 |
| 可用性 | 目標水準への改善を求める。 | 可用率、復旧時間、切り替え時間などが受入条件を満たす。 |
| セキュリティ | 旧挙動を保存せず、新しい要求へ変更する場合がある。 | 認証、認可、暗号化、依存関係、脆弱性対策などが要求水準を満たす。 |
さらに、これらの品質特性は個別に目標を設定すれば終わりではない。ある特性を改善するための設計変更が、別の特性を悪化させる場合がある。
例えば、すべてのデータ更新を遠隔拠点へ同期複製してから成功と返す設計を考える。この変更によって、拠点障害時にもデータを失いにくくなり、耐障害性は改善する。一方、各要求で遠隔通信を待つため応答時間は増える。
耐障害性を \(q_{\mathrm{resilience}}\)、応答性能を \(q_{\mathrm{latency}}\) とすれば、ある設計変更 \(\Delta\) によって、
\[
q_{\mathrm{resilience}} (C+\Delta) > q_{\mathrm{resilience}} (C)
\]
となる一方で、
\[
q_{\mathrm{latency}} (C+\Delta) > q_{\mathrm{latency}} (C)
\]
となる可能性がある。応答時間では値が大きいことは悪化を意味するため、一つの設計変更が一方を改善し、もう一方を悪化させている。
ATAM が品質属性間のトレードオフを扱うのは、このような関係を設計段階で確認するためである[16]。モダナイゼーションでは、新しい技術やアーキテクチャを採用したこと自体を改善とみなすのではなく、それによって各品質特性がどの方向へ変わったかを見る必要がある。
この構造を一般化すると、品質特性 \(q_i\) ごとに必要な関係 \(R_i^{q}\) を定義できる。
\[
\forall i\in Q,\quad R_i^{q} \left( q_i(C_{\mathrm{old}}), q_i(C_{\mathrm{new}}) \right)
\]
\(Q\) は評価対象となる品質特性の集合であり、\(R_i^{q}\) はその品質特性に固有の判定関係である。機能なら等価性、応答時間なら上限値、処理量なら下限値、セキュリティなら要求集合への適合というように、同じ関係を使う必要はない。
非機能品質の検証結果を \(V_{\mathrm{nfr}}\) とするなら、概念的には次のように表せる。
\[
V_{\mathrm{nfr}} = \bigwedge_{i\in Q} R_i^{q} \left( q_i(C_{\mathrm{old}}), q_i(C_{\mathrm{new}}) \right)
\]
ただし、変更対象については旧値を参照せず、新しい目標値だけを判定対象にする場合もある。その場合、より一般には、
\[
V_{\mathrm{nfr}} = \bigwedge_{i\in Q} \left[ q_i(C_{\mathrm{new}}) \in A_i^{q} \right]
\]
と表せる。\(A_i^{q}\) は、その品質特性について新システムが満たすべき受入範囲である。
ここでも、要求値を書いただけでは検証にならない。応答時間なら想定負荷で実測する必要があり、可用性なら障害発生と復旧を確認する必要がある。セキュリティなら設計上の要件だけでなく、実装、構成、依存関係、権限制御なども確認する必要がある。品質特性を仕様へ記述することと、その性質が実システムで成立したことを確認することは別である。
このため、機能、データ、性能、可用性、セキュリティを一つの「等価性」という判定へまとめることはできない。保存する性質には保存関係を、改善する性質には新しい目標値を、廃止する性質には不存在や禁止条件を与える必要がある。
モダナイゼーションの成功とは、旧システムの品質ベクトルをそのまま複製することではない。残すと決めた成分を必要な関係で保存し、変えると決めた成分を新しい受入領域へ移し、その間に生じるトレードオフが許容可能であることを確認することである。
ここまでで、仕様比較、実行比較、データ移行検証、非機能品質検証がそれぞれ異なる失敗経路を対象にしていることが分かる。次に必要なのは、これらを個別のチェックとして並べるのではなく、モダナイゼーションの正しさを支える複数の検証レイヤーとして統合することである。
9. 正しさは独立した検証レイヤーから積み上げる
ここまでの議論から、モダナイゼーションの正しさを一つの検査結果だけで判定できない理由が見えてくる。仕様比較は、旧新コードから抽出した意味モデル上の差異を検出する。実行比較は、具体的な入力と実行環境で実際に現れた差異を検出する。データ検証は、永続状態が新しい表現へ正しく移されたかを確認する。性能、可用性、セキュリティなどは、旧システムとの一致ではなく、新しい受入条件を満たすかを確認する。
これらは、一つの正しさを別の方法で重複確認しているわけではない。それぞれが異なる失敗条件を観測している。仕様比較が成功しても、抽象化から落ちたトランザクション境界は残る。実行比較が成功しても、実行しなかった入力や障害条件は残る。データ件数が一致しても、参照関係の破壊は残り得る。機能が一致しても、応答時間やセキュリティ水準が目標を満たすとは限らない。
このため、検証レイヤーを追加する意味は「チェック数を増やすこと」ではなく、異なる失敗経路を閉じることにある。
NIST IR 8397 は、開発者によるソフトウェア検証について、静的解析、ブラックボックス試験、コード構造に基づく試験、過去の試験、ファジングなど、性質の異なる複数の技法を組み合わせることを推奨している[18]。IEEE 1012 も、検証と妥当性確認を試験だけに限定せず、分析、評価、レビュー、検査など複数の活動から構成されるものとして扱っている[19]。複数の技法を使う理由は、同じ対象を何度も確認することではなく、一つの技法が持つ観測限界を別の技法で補うことにある。
| 検証レイヤー | 主に確認すること | 検出しやすい失敗 | 単独では残る死角 |
|---|---|---|---|
| 仕様・意味比較 | 保存対象の業務規則、状態遷移、データ意味、例外条件などが新旧で対応しているかを確認する。 | 分岐条件の欠落、業務規則の変更、状態遷移の差などを広いコード範囲から検出できる。 | 意味モデルに含まれない実行時特性と、抽出器による共通モードの誤りが残る。 |
| 実行比較 | 同じ入力と実行条件で、出力、状態更新、例外、副作用が必要な関係を満たすかを確認する。 | 実際の環境で発生する計算差、状態差、外部副作用、障害時挙動の差などを検出できる。 | 未実行の入力、状態、障害条件と、正解判定の不完全性が残る。 |
| データ検証 | 識別子、参照、履歴、精度、不変条件などが移行前後で意味上対応しているかを確認する。 | 欠落、重複、誤対応、参照整合性破壊、集約値の不一致などを検出できる。 | 新コードの業務規則や実行経路の正しさは直接保証しない。 |
| 非機能検証 | 性能、可用性、復旧性、資源消費などが新しい受入条件を満たすかを確認する。 | 機能結果には現れない応答性能低下、容量不足、復旧時間超過などを検出できる。 | 業務規則やデータ意味の保存は別に確認する必要がある。 |
| セキュリティ検証 | 設計、実装、依存関係、構成、認証、認可などが新しい要求水準を満たすかを確認する。 | 旧システムとの機能互換性では発見できない脆弱な設計や構成を検出できる。 | 業務互換性やデータ移行の正しさは別の検証対象になる。 |
適用する検証レイヤーの集合を \(L\) とし、それぞれの検証結果を \(V_{\ell}\) とする。例えば、
\[
L = \{ \mathrm{spec}, \mathrm{behavior}, \mathrm{data}, \mathrm{nfr}, \mathrm{security} \}
\]
と置くことができる。必要な検証結果がすべて成立することを移行承認の条件に含めるなら、概念的には次のように表せる。
\[
\mathrm{EvidenceSatisfied} = \bigwedge_{\ell\in L} V_{\ell}
\]
\(\bigwedge\) は、採用した検証レイヤーの結果がすべて成立することを表す。仕様比較だけ成功していても、データ検証が失敗していれば \(\mathrm{EvidenceSatisfied}\) は成立しない。性能試験だけが成功していても、保存すべき業務規則が変わっていれば同様である。
ただし、この式を「五つの検証に合格すれば完全な正しさが証明される」と読むことはできない。各 \(V_{\ell}\) には、それぞれの検証を成立させる前提があるからである。
例えば仕様比較では、意味モデルが必要な性質を含み、抽出器が対象コードを正しく解析し、比較規則が必要な差異を検出できるという前提がある。実行比較では、選択した入力と実行環境が確認したい失敗条件を含むという前提がある。性能試験では、与えた負荷が本番利用を適切に代表するという前提がある。
検証レイヤー \(\ell\) の前提条件を \(A_{\ell}\)、そのレイヤーが支える主張を \(G_{\ell}\) とする。検証結果 \(V_{\ell}\) は、前提が成立した条件の下で主張を支える証拠として解釈する。
\[
A_{\ell} \land V_{\ell} \Rightarrow G_{\ell}
\]
つまり、「\(V_{\ell}\) が真である」という結果だけを切り離すのではなく、「どの条件 \(A_{\ell}\) の下で、どの主張 \(G_{\ell}\) を支える結果なのか」を併せて管理する必要がある。
すべての検証を束ねても、この構造は変わらない。
\[
\left( \bigwedge_{\ell\in L} A_{\ell} \right) \land \left( \bigwedge_{\ell\in L} V_{\ell} \right) \Rightarrow \left( \bigwedge_{\ell\in L} G_{\ell} \right)
\]
例えば、実行比較で 10 万件のテストに成功していても、それらがすべて通常系であり、並行更新や外部障害を含んでいなければ、その結果を並行実行時の正しさへ拡張できない。性能試験で目標値を満たしていても、実際のデータ量の 10 分の 1 しか投入していなければ、本番規模で同じ結果になるとは限らない。
このため、検証結果だけでなく、その結果の適用範囲を決める前提も証拠の一部になる。
さらに、複数の検証レイヤーを用意したからといって、それらが自動的に独立した証拠になるわけではない。例えば、同じ生成 AI を使って旧コードから仕様を生成し、新コードからも仕様を生成し、さらにその仕様差分の判定まで同じモデルへ任せた場合を考える。
形式上は、旧仕様の抽出、新仕様の抽出、仕様差分の判定という三つの処理に分かれている。しかし三つが同じ解析能力と同じ誤解を共有していれば、一つの共通原因によって複数の証拠が同時に無効になる可能性がある。検証工程が三つに分かれていることと、三つの証拠が独立していることは同じではない。
ここでいう独立性は、確率論上の完全な統計的独立を要求するという意味ではない。実務上重要なのは、一つの失敗原因が複数の検証を同時に無効化しないよう、観測原理を分けることである。
例えば、次の組み合わせでは失敗原因が異なる。
| 証拠 | 観測方法 | 共通誤りを減らせる理由 |
|---|---|---|
| 仕様比較 | コードを解析して業務規則と状態遷移を抽出する。 | 実行していない経路も静的に確認できる。 |
| 実行比較 | 旧新システムを実際に動かし、状態と副作用を観測する。 | 仕様抽出器が誤読した場合でも、実際の振る舞いとの差として現れる可能性がある。 |
| データ不変条件 | 移行後データそのものへ整合性条件を適用する。 | コードや仕様の解釈とは別に、永続状態の破壊を直接観測できる。 |
| 性能測定 | 実際の負荷を与えて時間と資源消費を測る。 | 機能仕様が同じでも生じる実行基盤上の劣化を直接観測できる。 |
つまり、検証レイヤーを選ぶときには、「何個あるか」よりも「どの失敗原因を別の原理で観測できるか」を見る必要がある。
この関係を、失敗モードの集合 \(F\) と各検証レイヤーが検出できる失敗モード \(F_{\ell}\) を使って表すこともできる。
\[
F_{\ell} \subseteq F
\]
検証レイヤーを増やす目的は、単純に \(|L|\) を大きくすることではない。検出可能な失敗モードの和集合を広げることである。
\[
\bigcup_{\ell\in L} F_{\ell}
\]
例えば同じ静的解析を設定だけ変えて 5 回実行しても、検出できる失敗集合がほとんど同じなら、
\[
F_1 \approx F_2 \approx \cdots \approx F_5
\]
となり、検証回数ほど保証範囲は増えない。一方、静的な仕様比較と実行比較について、互いに一方だけが検出できる失敗が存在するなら、
\[
F_{\mathrm{spec}} \setminus F_{\mathrm{behavior}} \neq \varnothing
\]
かつ、
\[
F_{\mathrm{behavior}} \setminus F_{\mathrm{spec}} \neq \varnothing
\]
となる。この場合、両者を組み合わせることで、どちらか一方だけを使う場合より検出可能な失敗領域を広げられる。
ただし、すべての失敗モードを有限個の検証で完全に覆えるとは限らない。未検出の失敗が残る場合には、
\[
\bigcup_{\ell\in L} F_{\ell} \subseteq F,\qquad \bigcup_{\ell\in L} F_{\ell} \neq F
\]
となる。つまり、複数レイヤーを積み上げても「未知の失敗が存在しない」と証明したことにはならない。この限定を明示したうえで、業務上必要なリスクまでどこまで閉じたかを判断するのが移行承認になる。
ここで、検証結果を単なる合否として保存するだけでは不十分になる。どの証拠が、どの保存条件または変更条件を支えているかを追跡できなければならない。
例えば、第 2 章で定義した保存対象の性質を \(\phi_i\) とすると、それぞれについて必要な主張を \(G_i\) と置ける。
\[
G_i = R_i \left( \phi_i(C_{\mathrm{old}}), \phi_i(C_{\mathrm{new}}) \right)
\]
ある主張 \(G_i\) を、どの証拠 \(E_j\) が支えているかという関係を、
\[
E_j \vdash G_i
\]
と表す。\(\vdash\) は、ここでは「証拠 \(E_j\) が主張 \(G_i\) を支える」という対応関係を表す記号として使う。
例えば、「注文確定条件が保存された」という主張に対しては、旧新仕様の比較結果と境界値の差分テストが証拠になるかもしれない。「顧客と契約の対応が保存された」という主張には、データ移行後の参照整合性検査が必要になる。「95 パーセンタイル応答時間が 500 ミリ秒以下」という主張には、性能試験の測定結果が必要になる。
| 保証したい主張 | 主な証拠 | 残る前提 |
|---|---|---|
| 注文確定条件が保存されている | 仕様差分、境界値テスト、異常系の新旧実行比較などが支える。 | 抽出した条件と選択したテストが必要な業務条件を覆っていることを前提とする。 |
| 移行後も契約が正しい顧客へ紐付く | 対応表照合、参照整合性検証、不変条件検査などが支える。 | 対応規則そのものが正しく定義されていることを前提とする。 |
| 応答時間が目標を満たす | 本番想定データと負荷を使った性能測定が支える。 | 負荷条件と実行環境が本番を十分に代表することを前提とする。 |
| 新しい認証要件を満たす | 設計確認、構成確認、認証試験、権限試験などが支える。 | 採用した脅威モデルと要求が必要な攻撃面を含むことを前提とする。 |
この対応を持つことで、「テストは全部通った」「仕様比較も一致した」という工程単位の報告から、「どの主張について、どの証拠があり、何がまだ未確認なのか」という保証単位の管理へ移れる。
例えば、仕様比較と実行比較が成功していても、データ移行後の参照整合性について証拠がなければ、その主張は未確定のままである。逆に、ある項目について複数の証拠があり、前提条件も明確なら、その項目を後続工程が前提として利用できる状態にできる。
大規模な開発では、この「未確定な主張を証拠によって閉じる」考え方が重要になる。既稿では、AI による大規模開発でも、コードや文書を大量に生成することより、未確定な状態を一件ずつ証拠によって確定し、後続工程が安全に依存できる状態へ変えることが重要だと整理した[20]。
モダナイゼーションでも同じである。仕様差分、テスト結果、移行データの検証結果、性能測定、セキュリティ検証を単なる成果物の一覧として残すだけでは足りない。それぞれが、どの保存条件、どの変更条件、どの移行判断を支えているかを対応付ける必要がある。
この構造まで含めると、移行承認とは「すべての試験項目が緑色になった状態」ではない。必要な主張について、適切な観測原理を持つ証拠がそろい、その証拠の前提と未確認範囲が明示され、残余リスクを受け入れられる状態である。
正しさは、一つの強力な検証によって突然得られるものではない。仕様、実行、データ、非機能、セキュリティという異なる観測面から、互いに異なる失敗経路を閉じ、その証拠を保存対象と変更対象へ対応付けることで積み上がる。
ここまで整理すると、最終的にモダナイゼーションで証明したい命題も変わる。旧システムと新システムがあらゆる意味で「同じ」であることではない。残すと決めた性質が保存され、変えると決めた性質が目標へ到達し、それを支える証拠が必要な範囲でそろっていることである。
10. モダナイゼーションで証明すべきなのは「同じシステム」であることではない
モダナイゼーションについて「旧システムと新システムは等価か」とだけ問うと、判定対象が曖昧になる。ソースコードやアーキテクチャは意図的に変える。性能やセキュリティは改善したい。一方で、業務計算、契約データの意味、外部へ約束したインターフェースなど、変えてはいけない性質もある。旧新が同じことが成功条件になる性質と、異なることが成功条件になる性質が同時に存在する。
必要なのは、システム全体へ一つの等価関係を適用することではない。第 2 章で定義したように、保存対象について必要な関係が成立し、変更対象について新しい受入条件が成立し、その判断を支える証拠がそろっていることである。
保存条件、変更条件、第 9 章で整理した証拠条件を合わせると、モダナイゼーションの正しさは次の構造として表せる。
\[
\mathrm{CorrectModernization} = \left[ \bigwedge_{i\in I_{\mathrm{preserve}}} R_i \left( \phi_i(C_{\mathrm{old}}), \phi_i(C_{\mathrm{new}}) \right) \right] \land \left[ \bigwedge_{j\in I_{\mathrm{change}}} \phi_j(C_{\mathrm{new}}) \in A_j \right] \land \mathrm{EvidenceSatisfied}
\]
第一項は、残すと決めた性質が、それぞれに定めた保存関係を満たすことを表す。第二項は、変えると決めた性質が新しい受入条件へ入ることを表す。第三項は、その二つの判断を仕様比較、実行比較、データ検証、非機能検証、セキュリティ検証などの必要な証拠で支えることを表す。
この中で、新旧コードから仕様を生成して比較する方法が強くするのは、主として意味保存に関する証拠である。COBOL と Java、モノリスと複数サービス、同期処理とイベント駆動のように実装構造が大きく異なっても、保存すると定めた意味を共通形式へ写せば比較できる。このため、仕様比較はモダナイゼーションにおける非常に良い検証レイヤーである。
ただし、その結果をシステム全体の等価性証明へ拡張してはならない。仕様比較が最も正確に示せるのは、「定義した意味モデルと比較規則の範囲で、保存対象について差異が検出されなかった」という範囲である。
実行比較にも有限の入力と環境という境界があり、データ検証にも定義した不変条件という境界がある。性能試験は指定した負荷条件、セキュリティ検証は採用した脅威モデルや検査範囲に依存する。複数の検証を積み上げる目的は、これらの境界を消すことではなく、異なる失敗経路を別の観測方法で閉じ、どの主張をどの証拠が支えているかを明確にすることにある。
生成 AI や自動変換技術によってコード生成が高速になるほど、工程上の制約はコードを書く能力から、保存対象を定義する能力、差異を検出する能力、証拠を評価する能力へ移る。モダナイゼーションで最終的に問われるのは、「古いコードを新しいコードへ書き換えられるか」ではなく、「何を保存し、何を変更し、それぞれについて何をもって正しいと判定するかを定義できるか」である。
正しいモダナイゼーションとは、旧システムと新システムが同じであることではない。残すべき意味が残り、変えるべき性質が意図どおり変わり、その判断を支える証拠が必要な範囲でそろっている状態である。
参考文献
- Elliot J. Chikofsky, James H. Cross II, Reverse Engineering and Design Recovery: A Taxonomy (1990). https://ieeexplore.ieee.org/document/43044/
- id774, AI モダナイゼーションはモデルではなく工程を変える（2026-07-21）. https://blog.id774.net/entry/2026/07/21/5118/
- C. A. R. Hoare, An Axiomatic Basis for Computer Programming (1969). https://doi.org/10.1145/363235.363259
- id774, AI モダナイゼーションはなぜ仕様選択と検証で止まるのか（2026-07-29）. https://blog.id774.net/entry/2026/07/29/5158/
- Alexandru F. Iosif-Lazăr, Ahmad Salim Al-Sibahi, Aleksandar Dimovski, Juha Erik Savolainen, Krzysztof Sierszecki, Andrzej Wasowski, Experiences from Designing and Validating a Software Modernization Transformation (2015). https://doi.org/10.1109/ASE.2015.84
- Amir Pnueli, Ofer Shtrichman, Michael Siegel, Translation Validation for Synchronous Languages (1998). https://doi.org/10.1007/BFb0055057
- George C. Necula, Translation Validation for an Optimizing Compiler (2000). https://doi.org/10.1145/349299.349314
- Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, John Regehr, Alive2: Bounded Translation Validation for LLVM (2021). https://doi.org/10.1145/3453483.3454030
- Xavier Leroy, Formal Verification of a Realistic Compiler (2009). https://doi.org/10.1145/1538788.1538814
- William M. McKeeman, Differential Testing for Software (1998). https://dblp.org/rec/journals/dtj/McKeeman98.html
- Elaine J. Weyuker, On Testing Non-Testable Programs (1982). https://doi.org/10.1093/comjnl/25.4.465
- Earl T. Barr, Mark Harman, Phil McMinn, Muzammil Shahbaz, Shin Yoo, The Oracle Problem in Software Testing: A Survey (2015). https://doi.org/10.1109/TSE.2014.2372785
- id774, AI がテストを通しても、「正しい」とは限らない（2026-09-01）. https://blog.id774.net/entry/2026/09/01/5534/
- Bin Wei, Tennyson X. Chen, Verifying Data Migration Correctness: The Checksum Principle (2014). https://doi.org/10.3768/rtipress.2014.op.0019.1403
- ISO/IEC 25010:2023, Systems and software engineering — Systems and software Quality Requirements and Evaluation (SQuaRE) — Product quality model. https://www.iso.org/standard/78176.html
- Rick Kazman, Mark H. Klein, Mario R. Barbacci, Thomas A. Longstaff, Howard F. Lipson, Jeromy Carriere, The Architecture Tradeoff Analysis Method (1998). https://www.sei.cmu.edu/library/the-architecture-tradeoff-analysis-method/
- NIST, Secure Software Development Framework (SSDF) Version 1.1: Recommendations for Mitigating the Risk of Software Vulnerabilities (2022). https://csrc.nist.gov/pubs/sp/800/218/final
- NIST, Guidelines on Minimum Standards for Developer Verification of Software, NIST IR 8397 (2021). https://csrc.nist.gov/pubs/ir/8397/final
- IEEE Std 1012-2024, IEEE Standard for System, Software, and Hardware Verification and Validation. https://standards.ieee.org/ieee/1012/7324/
- id774, AI による大規模開発では、未確定な状態を一件ずつ閉じる（2026-08-15）. https://blog.id774.net/entry/2026/08/15/5503/