目次

はじめに

演繹的検証によって推進される開発に関する一連の記事を続けて、ここではこの方法論を、既に実用的なソフトウェア工学でその地位を確立している最も密接に関連する技術と比較します。プログラムが仕様に適合していることの確認を探す手順と、既に見つかった解決策を検証する手順の両方の記述を形式化することにより、最初の手順を手動で実装し、二番目を自動化することが、完全に自動化された方法よりもいくつかの利点を提供する、実用的な妥協点となり得ることを読者に納得させようとします。

形式的検証技術の特徴と類似点

ソフトウェアの形式的な検証の自動化について議論する際、この分野の状況が極めて広大であり、最も一般的な意味でのみ関連する多くの技術を包含していることに気づかざるを得ません。同時に、専門家でさえ、この包括的な用語を使用し、適用される技術間の重要な方法論的な違いから焦点を逸らし、彼らの共通の目標—プログラマーの明確な仕様で表現された意図に対応するプログラムの観察された振る舞いを数学的に納得のいく形で機械的に確認すること—に焦点を当てます。ソフトウェアの形式的な検証の自動化のアイデアの数学的な本質を正式に強調しようとすると、大まかに言って、いくつかの基本的なオブジェクトに基づいてこれを行うことができます。

  • ある論理のすべての命題を列挙する可算集合$\mathcal{L}$。この論理は、$S = {f : X \rightharpoonup Y \mid l_S}$の形の仕様を記述することができ、ここで$l_S \in \mathcal{L}$。
  • アルゴリズムの正確性証明書を列挙する可算集合$\mathcal{C}$（この概念の意味は後で明らかになります）。
  • 計算可能な関数$\texttt{verify} : P \times \mathcal{L} \times \mathcal{C} \to {\texttt{Proven}, \texttt{Contra}, \texttt{Invalid}}$。任意のプログラム$p \in P$と仕様の記号的表記$l_S \in \mathcal{L}$に対して、$\mathfrak{M}_p \in S \Leftrightarrow \exists c \in \mathcal{C} : \texttt{verify}(p, l_S, c) = \texttt{Proven}$および$\mathfrak{M}_p \notin S \Leftrightarrow \exists c \in \mathcal{C} : \texttt{verify}(p, l_S, c) = \texttt{Contra}$という同値関係が成立します。

実用的に適用可能な方法では、$\texttt{verify}$関数は容易に計算可能でなければならないこと（つまり、最低限でも多項式複雑性クラスに属すること）が指摘されており、その判決は検証されるアルゴリズムの正確性の証拠と見なされるため、一般的に正しいと認められる必要があります。全体像を完成させるためには、アルゴリズムの正確性証明書と呼ばれるものの意味と構築方法を定義する必要があります。この概念の意味は、$\texttt{verify}$関数を、$\mathfrak M_p$が$S$に属するかどうかという非決定性多項式問題の解を多項式時間内でチェックする手順と見なすと明らかになります。ここで$c$はオラクルからのヒントとして機能します。これは、以前使用した平面グラフを4色までの色数で列挙するアルゴリズムの例を用いて最も簡単に説明できます。

  • $\mathfrak{M}$は、チューリング完全な操作セマンティクスを持つ抽象マシン。
  • $p$は、記事「プログラム検証：背景と表記法」（セクション_例：グラフの彩色_[1]）で説明されたプログラム。
  • $l_S$は、任意の平面グラフの彩色の成功を宣言する仕様の記述。
  • $c$は、四色定理の証明を構成する633の構成の列挙。

これらの構成要素が利用可能であれば、4色までの色数を列挙するアルゴリズムの正確性は、比較的簡単な自動推論を通じて機械的に確認できます。したがって、アルゴリズムの正確性証明書は、対応する同値類に属するという事実を数学的に証明する手順の記号的記録、またはこの所属を否定する反例の記録と見なすことができます。現代のエンジニアリング実践では、ほとんどの場合、その検証（$\texttt{verify}$）だけでなく、その生成（$\texttt{evince}$）の自動化を意味するアプローチが主流です。これは、$\mathtt{evince} : P \times \mathcal L_* \rightharpoonup \mathcal C$というヒューリスティックで一般化することができ、$\mathcal L_* \subseteq \mathcal L$であり、任意の$p \in P, l_S \in \mathcal L_*, c \in \mathcal C$に対して、$\mathtt{evince}(p, l_S) = c \Rightarrow \mathtt{verify}(p, l_S, c) \neq \mathtt{Invalid}$が成立します。

例として、ユーリ・G・カルポフによって記述されたモデル検査のメカニズムを考えてみましょう（以下の翻訳は私たちによるものです）[2]、83ページ：

モデル検査は、有限数の状態（クリプキ構造）を持つシステムモデルに関して、時間論理式（CTL*、CTL、LTL）の真偽を検証するためのモデル、技術、およびアルゴリズムを使用する方法論です。クリプキ構造は動的システムの振る舞いを記述し、時間論理はそれらの特性を記述する効率的な形式論です。

検証対象のシステムの変数とパラメータを使用して、開発者が関心を持つ原子的述語—各状態で「真」または「偽」の値を取る論理式—がクリプキ構造内で表現されます。この文脈では、システム状態の「偽」は、入力された論理式に対する反例と見なすことができます。

任意の複雑なヒューリスティック$\texttt{evince}$について、プログラムと仕様の任意の組み合わせに対して一般的な意味でこの問題を解くことができるとは期待すべきではないことを理解する必要があります[3]。停止問題が決定不能であるのと同じ理由で、任意の非自明な仕様に対して、この仕様への適合性の証明書をどのアルゴリズムでも構築できないプログラムが常に存在します。さらに、アルゴリズム的完全性を持たない計算モデルに限定し、仕様言語としての一階述語論理の非自明な断片に限定した場合でも、計算複雑性の観点から、ほとんど常に$\texttt{PSPACE}$困難な問題の領域にとどまります。これは、少しでも非自明なプログラムの自動検証を非常に問題にします。

正確性証明書と検証プロセスにおけるその役割

正確性証明書を数学的な証明手順の記述と見なすことは、残念ながら実用的な応用というよりは理論的な一般化です。なぜなら、現時点のエンジニアリング文化は、その検証（$\texttt{verify}$）だけでなく、その生成（$\texttt{evince}$）の自動化を意味するアプローチが主流だからです。功利的な観点から見ると、証明された信頼性のある正確性証明書の検証手順がある場合、その構築方法はあまり重要ではないように最初は思えるかもしれません。結局のところ、私たちが必要なのは、コードが仕様に適合しているという保証だけです。しかし、アルゴリズムの検証タスクを数学的な観点から検討すると、既存の自動正確性証明書生成方法には、多くの重要で、そしておそらく克服できない欠点があることが明らかになります。

第一に、証明を見つけるタスクとそれを確認するタスクとの間の基本的な複雑さのギャップのために、ヒューリスティック$\texttt{evince}$が受け入れる目的のための下位言語は、関数$\texttt{verify}$の定義域の論理言語と比較して常に比較的小さいものです。さらに、$\mathcal{L}_*$の形で記録できる仕様$S$であっても、特定の$\texttt{evince}$で使用される列挙戦略によって課される非常に特殊な制限に従って、極めて不自然な方法で定式化しなければならないことがよくあります。

第二に、$\texttt{evince}$の挙動は、処理されるアルゴリズムの些細な変更に対しても、必然的に非常に敏感です。プログラムのセマンティクスはその全体で仕様への適合性をチェックされるため、$p$と$p’$の違いがどれほど局所的であっても、列挙ヒューリスティック$\texttt{evince}(p, l_S)$と$\texttt{evince}(p’, l_S)$の計算は、ほとんど常に大幅に異なる経路をたどり、成功した場合でも、構造的に比較できない$c$と$c’$に至ります。

最後に、数学者が扱う伝統的な証明とは異なり、列挙ヒューリスティックによって見つかった正確性証明書から、プログラムと仕様の関係についてのさらなる情報を抽出することは、実際には不可能です。数学では、証明はしばしば証明される命題の定式化以上に、関与するオブジェクト間の関係についてのはるかに有用な情報を含むことがあります。

これらの欠点は、SMTソルバーやモデルチェック法を実用的な意味でそれほど有用でなくするものではありません。彼らが生成する反例はアルゴリズムのエラーを正確に特定し、有効な証明書はコードの特定のバージョンのデバッグプロセスで決定的な結論を可能にします。しかし、正確性証明書の構築の自動化が、その中に数学的な意味が欠如していることの十分な補償となるのかどうかを考えてみる価値があるかもしれません。業界は「ワンボタン」ソリューションの追求で何か重要なものを見逃しているのでしょうか？

ディープスペシフィケーション手法

「検証駆動開発」[4]で提案された方法論は、ディープスペシフィケーション手法とも呼ばれます。従来の技術とは異なり、これは$\texttt{verify}$手順のみの機械化を想定し、正確性証明書の構築は人間に委ねます。このアプローチは、明らかに、自動ヒューリスティックの使用と比較して、操作者の資格にやや高い要求を課しますが、その見返りとして、いくつかの重要な利点が期待されます。

第一に、演繹的な証明の探索では、論理言語$\mathcal{L}$を何らかの形で制限する必要はありません。仕様は最も自然な方法で定式化でき、自動ソルバーの特殊な要件に明晰さや簡潔さを犠牲にする必要はありません。帰納的な型の強力な表現力を持つCoqやLeanで定式化できる任意の命題は、仕様記述に使用できます。

第二に、漸進的な仕様の洗練の方法論を用いて構築された証明書は、多数の独立した命題の証明から構成され、検証されたアルゴリズムと構造的に並行しています。つまり、証明書の要素とプログラムコードのセグメントとの間に局所的な対応があります。これにより、プログラムや仕様の些細な変更が、ほとんどの場合、正確性証明書へのわずかな調整のみを必要とすることが期待でき、インクリメンタルな開発を促進します。

最後に、前回の記事の最後に私たちが定式化した仮説[5]が真である場合、正確性証明書とそれが検証するプログラムの並行した構築は、タスクをサブタスクに分解する自然な論理に従います。その結果、正確性証明書は、プログラムの観察された振る舞いの仕様への適合性の確認だけでなく、実装されるアルゴリズムの構造の正式な記述となります。つまり、プロジェクトのドキュメンテーションの基盤として使用できる正確なアーキテクチャ設計図となります。

$\texttt{evince}$のワンボタンのシンプルさを犠牲にすることで、伝統的に理解される利便性を失うかもしれませんが、もっと多くを得ることを期待しています。Inferaraでは、演繹的検証によって推進される開発が、ソフトウェア工学の完全に独立した方法論となり、大規模なプロジェクトで信頼性保証のシームレスなスケーリングを可能にすると提案しています。このスケーリングは、空間軸（最も重要と考えられる小さなコードセクションだけでなく、周囲のインフラ全体を正式な仕様でカバーすることを容易にする）と時間軸（既に検証されたアルゴリズムにさらなる変更を加える際に信頼性保証を維持するのに役立つ）の両方に関係します。

結論

演繹的プログラム検証は半世紀以上にわたって数学的なアーティファクトのままであり、その実用的なエンジニアリングでの稀な適用は、高度な技術的先端での数少ない粘り強い研究者にのみアクセス可能な高度な技芸と見なされてきました。一方で、SMTソルバーやモデルチェック法のような新しい技術は、実務のツールに変わり、形式的な検証の概念を産業界の日常的な一部にしました。おそらく今、ブロックチェーンと暗号通貨産業が明確に世界的な金融システムの一部となり[6]、直接的な金融義務を生み出し、演繹的定理証明のためのツールが成熟した現在、以前はあまりにも奇抜と考えられていたアイデアの真の可能性を明らかにする時が来たのかもしれません。

参考文献

この論文の議論に参加してください:

x
discord
telegram

この記事は AI 搭載の翻訳ツールによって翻訳されました。翻訳に誤りがある場合はご容赦ください。すぐに校正し、考えられる誤りを修正します。誤りを見つけた場合は、GitHub で問題を作成してください。