検証駆動開発

はじめに

前回の出版物[1]では、アルゴリズム仕様問題の操作的側面を形式化しました。今回は、アルゴリズムを定義したいと言うとき、それが何を意味するのかを詳述します。一般的な意味では、プログラムの仕様手順は通常、アルゴリズムの振る舞いに対して暗黙的に課される制限を設定する形を取ります。したがって、同じ一連のルールで制限されたプログラムの同値類を作成します。

形式的仕様入門

「_$s$は、厳密な順序$\prec$に従って$\Gamma$の要素列をソートするアルゴリズムである」と言うとき、期待される$\mathfrak M_s : \Gamma^* \rightharpoonup \Gamma^*$の振る舞いは以下のように形式化できます。

$\forall x \in \Gamma^*, \exists y = \mathfrak M_s(x)$、すなわち$\mathfrak M_s$は全域的である。
$\forall x \in \Gamma^*, y = \mathfrak M_s(x), \forall \gamma \in \Gamma, \displaystyle\sum_{i=1}^{\left| x \right|} [x_i=\gamma] = \displaystyle\sum_{i=1}^{\left| y \right|} [y_i=\gamma]$、すなわち$\mathfrak M_s$の出力は常に入力の置換である（アイバーソンのブラケット[2]記法を使用）。
$\forall x \in \Gamma^*, y = \mathfrak M_s(x), \forall i,j \in {1, \ldots, \left| x \right|}, y_i \prec y_j \Rightarrow i < j$、すなわち$\mathfrak M_s$の出力は常にソートされている。

これら3つの一階述語論理の公式は、一緒にすべてのソートアルゴリズムの集合を網羅的に記述します。言い換えれば、これらすべてを実装するプログラムは「ソートアルゴリズム」と呼ぶことができ、すべてのソートアルゴリズムはこれらすべてを実装しなければなりません。

上記のような同値類を作成することの最も重要な結果は、その特性について推論する文脈で、指定されたアルゴリズムのすべての実装詳細を無視できることです。複雑なプログラム$p(\ldots, s, \ldots)$を設計し、任意のソートアルゴリズム$s$をサブルーチンとして組み込み、もし$s’$がソートアルゴリズムであれば、$p(\ldots, s’, \ldots)$の特性についての推論はまったく同じになることを保証できます。しかし、このような考慮はプログラムの特性についての推論の区別不能性につながるのであって、プログラムの振る舞いの区別不能性ではないことを理解することが重要です。アルゴリズムの仕様は重要な側面のみをカバーし、重要でないものは無視します。例えば、部分順序付けされたアルファベット$\Gamma = {\mathtt A, \mathtt B, \mathtt C, \mathtt D}$を考えてみましょう。

$\mathtt A \prec \mathtt B \prec \mathtt D$、
$\mathtt A \prec \mathtt C \prec \mathtt D$、

ここで$\tt B$と$\tt C$は比較できません。すると、少なくとも2つの異なるソートアルゴリズム$s$と$s’$が現れます。これらのアルゴリズムを同じシーケンス$\tt CDACB$に適用すると、2つの異なる出力が得られます。

$\mathfrak M_s({\tt CDACB}) = {\tt ABCCD}$
$\mathfrak M_{s’}({\tt CDACB}) = {\tt ACCBD}$

このような不一致は正確性を無効にしません。つまり、特定の仕様は必要以上にアルゴリズムの振る舞いを制限しません。したがって、合成プログラム$p(\ldots, s, \ldots)$と$p(\ldots, s’, \ldots)$も異なる振る舞いをする可能性がありますが、$s$と$s’$の正確性のみに依存するその特性についての推論は同じになります。このアプローチは、ソフトウェア工学の最も危険な問題の一つである—モジュールテストの沼[3, p.4]を防ぎます。

モジュールテストの沼

プログラム設計$\mathfrak M_p : X \rightharpoonup Z$があり、それが形式的に定義された仕様$\forall x \in X, \mathtt{test}(x, \mathfrak M_p(x)) = \mathtt{true}$を実装するとします。ここで$\mathtt{test} : X \times Z \to Bool$は計算可能であり、ドメインの自然な列挙$(x_i \in X, i \in \N)$が存在し、それを用いて最終的な解が仕様に適合しているかテストできます。そのようなプログラムの開発サイクルの高レベルビューは、空の操作$p_0$から始まるインクリメンタルなプロセスのように見えるでしょう。次に、コードの繰り返しの修正、すなわち各$p_i$から$p_{i+1}$への修正がその品質を向上させ、望ましい観察可能な振る舞いが達成されます[4]。$X$の自然な列挙により、$p_i$の「品質」という用語は、最初の失敗に遭遇する前にパスしたテストの集合と考えることができます。このような観点で、開発の目標は、その品質$p_n$が測定不可能になるような反復$n$に近づくことです。なぜなら、失敗したテストが見つからないからです。

この概念は一見良さそうに見え、率直に言って、それには理由があって産業標準になったのでしょう。それは本当にシンプルで取り組みやすいからです。しかし、このワークフローには、戦術レベルで深く精査すると現れる隠れた欠点があります。複雑な作業において、品質を劣化させずに$p_i$から$p_{i+1}$への修正を行うことは非自明なプロセスです。複雑なシステムを全体として考えることは困難です。この問題は通常、大きな機能を独立して考慮されるサブタスクに分解することで対処されます。通常、変更はコードベース全体ではなく、個々のコンポーネントに絞られます。その変更の品質は通常、全体の$p$に課された品質についての個々の考えに依存します。

$\mathfrak M_p := \mathfrak M_{\hat p} \circ \mathfrak M_{\check p}$を2つの部分、すなわちプロデューサー$\mathfrak M_{\check p} : X \rightharpoonup Y$とコンシューマー$\mathfrak M_{\hat p} : Y \rightharpoonup Z$の合成として考えます。これら2つの部分間のインターフェースは、プロデューサーからコンシューマーに渡される可能性のある中間データ構造の可算集合$Y$として記述されます。自然に、そのようなモジュール化が機能するのは、テスト関数$\mathtt{test/prod} : X \times Y \to Bool$と$\mathtt{test/cons} : Y \times Z \to Bool$を用いてコンポーネントの振る舞いを指定できる場合のみです。そして$\forall x \in X, z \in Z, \mathtt{test}(x, z) \implies \exists y \in Y : \mathtt{test/prod}(x, y) \land \mathtt{test/cons}(y, z)$となります。ここで、適切なモジュール化の形式的な前提条件として、個々のテスト関数が存在するという理論的な可能性について話しており、実際の形式化ではありません。実際のケースでは、伝統的な開発ワークフローはそれを義務的とは考えていません。

次に、$\mathtt{test/prod}$と$\mathtt{test/cons}$がモジュール分割の前に形式化された場合を考えます。したがって、タスクの小さな部分を実装する必要があります。つまり、$\mathtt{test/prod}$に準拠する任意の$\mathfrak M_{\check p}$と$\mathtt{test/cons}$に準拠する任意の$\mathfrak M_{\hat p}$に対して、適切な仕様設計の結果として、合成$\mathfrak M_{\hat p} \circ \mathfrak M_{\check p}$は$\mathtt{test}$に準拠します。しかし、プログラム開発の反復プロセスは、プログラムがエラーなしで開発されないという事実によって複雑化します。

プロデューサーの品質は、全体のプログラムの品質と同じ方法で定義できます。すなわち、ドメイン$X$の自然な列挙に対してテストすることによってです。コンシューマーの品質を決定することは非自明なタスクであることが判明します。中間ドメイン$Y$は任意に定義されたので、与えられた自然な列挙を持ちません。固定された列挙$(y_i \in Y, i \in \N)$に対してテストされたコンシューマーの品質は、全体のプログラムの品質に疑問を投げかけます。なぜなら、それは必然的に特定のプロデューサーの実装に依存する人工的な列挙$(\mathfrak M_{\check p}(x_i), i \in \N)$に$\mathfrak M_{\hat p}$を適用することを要求するからです。これは、モジュールプログラムの反復開発の最もよく知られた普遍的な問題の一つにつながります。

レーマンとベラディは、大規模なオペレーティングシステムにおける連続するリリースの歴史を研究しました。彼らは、モジュールの総数はリリース番号とともに線形に増加しますが、影響を受けるモジュールの数はリリース番号とともに指数関数的に増加することを発見しました。すべての修正は構造を破壊し、システムのエントロピーと無秩序を増加させる傾向があります。元の設計上の欠陥を修正するための努力はますます少なくなり、以前の修正によって導入された欠陥を修正するための努力はますます多くなります。時間が経つにつれて、システムはますます秩序が悪くなります。遅かれ早かれ、修正は何の進展ももたらさなくなります。前進する一歩ごとに後退する一歩が続きます。原理的には永遠に使用可能であっても、システムは進歩の基盤としては使い古されています。さらに、マシンは変化し、構成は変化し、ユーザーの要件は変化するので、システムは実際には永遠に使用可能ではありません。ゼロからの真新しい再設計が必要です[3, p.122]。

フレデリック・P・ブルックス・ジュニアがその不朽の名著『人月の神話』で述べた問題は、大部分がテストによって暗示される品質指標の不適切さに起因すると言えます。プロデューサーをドメインの自然な列挙に対するより多くのテストをパスさせるパッチは、以前のテストを通じてその振る舞いを変更する代償を伴う可能性があります。たとえそのような変更がプロデューサーの仕様内で有効であっても、前の開発反復でプロデューサーの出力に対して十分にテストされたコンシューマーは、新しいテスト環境のために以前より早く失敗に遭遇し始めるかもしれません。つまり、テストの品質指標では、プロデューサーの改善がプログラム全体の劣化につながる可能性があり、そのような指標の妥当性に疑問を投げかけます。

沼からの脱出

ここで、重要な質問を提起します。「モジュールテストのパラダイムが時々失敗する可能性があるなら、代替案は何か？」もし、サブモジュールの環境的な振る舞いの検証が間違っている可能性があるという主張があるなら、サブモジュールの振る舞いをその環境の仕様に対して検証することが一つの選択肢となり得ます。上記のコンセプトに従って、モジュール化は今やプログラム仕様の分解から始めるべきであり、もし独立して指定されたサブモジュールが形式的な推論によって検証できるほど小さいならば、論理推論のルールによってプログラム全体の検証が可能になります。

実行可能なマシン$\mathfrak M$のプログラム$p$での実装で使用される仕様$S = {f : X \rightharpoonup Y \mid \ldots}$を考えます。空のプログラム$\mathfrak M_{p_0} \notin S$から始めて、段階的にそれを$\mathfrak M_{p_n} \in S$に修正する代わりに（テストでは捕捉できない）、論理的同値のルールを使用して$S$を書き換え、正しく実装するのが簡単な反復に到達するまで行います。提案された手順を詳細に説明するために、まずいくつかの記法を導入します。

$\left|p\right| \in \N$は、プログラム$p$の複雑さを示す（例えば、異なる実行状態の数）。
$\left|S / \mathfrak M\right| = \displaystyle\min_{p,\mathfrak M_p \in S}\left|p\right|$は、$\mathfrak M$上での最も簡単な$S$の実装の複雑さを示す。
$q(p_1, \ldots, p_k) : P \times \ldots \times P \to P$は、複数の任意のプログラムを一つに集約する計算可能な関数であるプログラムテンプレートを表す。
$T(S_1, \ldots, S_k) : 2^{X \rightharpoonup Y} \times \ldots \times 2^{X \rightharpoonup Y} \to 2^{X \rightharpoonup Y}$は、複数の任意の仕様を一つに集約する非計算可能な関数である仕様テンプレートを表す。
$q \models T$は、以下のように解釈されるテンプレートの適合性の関係を示す。$\forall p_1, \ldots, p_k \in P, S_1, \ldots, S_k \subseteq X \rightharpoonup Y, \mathfrak M_{p_1} \in S_1 \land \ldots \land \mathfrak M_{p_k} \in S_k \implies \mathfrak M_{q(p_1, \ldots, p_k)} \in T(S_1, \ldots, S_k)$。

重要な定義を一つ紹介します。

マシン$\mathfrak M$は、有限の適合するテンプレートのシステム$q_1 \models T_1, \ldots, q_t \models T_t$と自明性の境界$n \in \N$を持つ場合、合理的と呼ばれます。つまり、複雑さが$n < \left|S / \mathfrak M\right| < \infty$であるすべての仕様$S$に対して、ある$i \in {1, \ldots, t}$が存在し、$\emptyset \subset T_i(S_1, \ldots, S_k) \subseteq S$に精緻化でき、$\forall j \in {1, \ldots, k}, \left|S_j / \mathfrak M\right| < \left|S / \mathfrak M\right|$となる。

非形式的に言えば、$\mathfrak M$は合理的と呼ばれます。もし実装が可能で十分に複雑なすべての仕様$S$が、その実装が$S$よりも容易なサブ仕様$S_1, \ldots, S_k$の集合に適合的に分解できるならば。この特性により、以下の手順をインクリメンタルな開発ワークフローとして使用できます。

プログラムの意図された振る舞いの形式的な仕様$S_\varepsilon = {f : X \rightharpoonup Y \mid \ldots}$から開始し、再帰のインデックス変数として$\lambda := \varepsilon$を設定します。
もし$\left|S_\lambda / \mathfrak M\right| \leq n$ならば、$p_\lambda : \mathfrak M_{p_\lambda} \in S_\lambda$は直接見つけるのに十分自明です。
もし$\left|S_\lambda / \mathfrak M\right| > n$ならば、ある$i \in {1, \ldots, t}$が存在し、$\emptyset \subset T_i(S_{\lambda.1}, \ldots, S_{\lambda.k}) \subseteq S_\lambda$となり、$\forall j \in {1, \ldots, k}, \left|S_{\lambda.j} / \mathfrak M\right| < \left|S_\lambda / \mathfrak M\right|$です。各$j$に対して、$\lambda := \lambda.j$で手順を再帰的に適用し、$p_{\lambda.j} : \mathfrak M_{p_{\lambda.j}} \in S_{\lambda.j}$を生成します。適合性の関係により、$\mathfrak M_{p_{\lambda.1}} \in S_{\lambda.1} \land \ldots \land \mathfrak M_{p_{\lambda.k}} \in S_{\lambda.k} \implies \mathfrak M_{q_i(p_{\lambda.1}, \ldots, p_{\lambda.k})} \in T_i(S_{\lambda.1}, \ldots, S_{\lambda.k})$となるので、$p_\lambda = q_i(p_{\lambda.1}, \ldots, p_{\lambda.k})$とすれば$\mathfrak M_{p_\lambda} \in S_\lambda$となります。

この手順は構造的再帰であり、つまり段階的に単純な仕様にのみ深く進むので、最終的に停止し、葉として小さな手作業で選ばれたプログラムの集合に分岐テンプレートをツリー状に適用した$p_\varepsilon$を生成します。このような設計の健全性、つまり$\mathfrak M_{p_\varepsilon} \in S_\varepsilon$は、次の3つの前提セットから自然に結論付けられます。

テンプレートの適合性$q_1 \models T_1, \ldots, q_t \models T_t$が証明されている。
すべての再帰的ステップの包含$\emptyset \subset T_i(S_{\lambda.1}, \ldots, S_{\lambda.k}) \subseteq S_\lambda$が証明されている。
すべての自明なスニペット$p_\lambda : \mathfrak M_{p_\lambda} \in S_\lambda$が正しく選ばれている。

すべての要素が揃っていれば、結果として得られるプログラムは正確性の証明を伴います。これは、建設的な証明が存在するため、反論が見つからない可能性のある有限のテストカバレッジで保証されるよりもはるかに強力です。バグを明らかにする新しい入力ケースを突然発見し、その修正がプログラムの他の部分の振る舞いの連鎖的な劣化を引き起こすという状況は、単に発生し得ません。もちろん、そのような保証は無料ではありません。プログラマブルなマシンは、上記の定義に従って合理的でなければなりません。

Inferaraでは、次のような非公式に述べられた仮説を信じています。

実用的な操作セマンティクスを持つすべてのマシンは合理的である。古典的な意味でのインクリメンタルな開発を可能にするあらゆるプログラミングパラダイムに対して、アルゴリズムのモジュール化の直感的なルールに関連する完全な適合テンプレートのシステムを構築することが可能である。さらに、そのようなシステムの自明性の境界は常に管理可能な小ささである。

結論

ここで説明した開発ワークフローは、検証駆動プログラミングと呼ぶことができます。この新しいコンセプトは、テスト駆動開発の古典的なワークフローには避けられない限界があり、タスクの複雑さがアルゴリズムの非自明なモジュール化を必要とし始めると、プログラマーがプログラムの正確性の状態に確実に到達することを妨げるという観察に基づいています。ここでは、開発者の意図に対するプログラムセマンティクスの機械支援による確認を可能にする新しい方法を提案します。それは、観察可能な振る舞いの最も抽象的な形式化からアルゴリズム構造の細粒度の記述まで、密接に結合されたサブ仕様の階層として定式化されます。このようなアプローチは、無数の人的資源を消費してきた悪名高いモジュールテストの沼に対する貴重な安全ロープであると信じています。実装前にエンジニアリンググループが推論セットを適切に設計すれば、初回でプログラムを正しく実装することが可能です。

参考文献

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

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

目次#

はじめに#

形式的仕様入門#

モジュールテストの沼#

沼からの脱出#

結論#

参考文献#

目次

はじめに

形式的仕様入門

モジュールテストの沼

沼からの脱出

結論

参考文献