形式検証で保証できることとは何か？数学的に捉えて見えてきたこと

#はじめに
プログラムを検証する手法として、形式検証と呼ばれる、仕様を満たすことを数学的に証明する手法があります。
本記事では、この形式検証によって、プログラムの何が保証されるのかを数学的な観点で考察してみたいと思います。

#「形式検証」自体を数学的に捉える
まず、形式検証自体を数学的に捉えてみます。
そこで、実装(プログラム本体)と仕様をそれぞれ数学的にみるとどうなるか見ていきます。

##「実装」とは
プログラムとは何かを数学で表してみます。

\operatorname{implementation} : X \to Y

入力の集合$X$、出力の集合$Y$とすると、数学的にはプログラムは単なる関数だと考えることができます。(入力が複数ある場合でもuncurry化して1引数関数としてみることができます。)

##「仕様」とは
そして、この実装が満たしてほしい「仕様」とは何かというと、入力と出力の間にある関係だと考えることができるので、以下のように書けます。

\operatorname{specification} : X \to Y \to 2

ただし$2 := \{\top,\bot\}$はTrueとFalseからなる集合、つまりbool値の集合とします。¹

##「実装が仕様を満たす」とは
仕様と実装を定義したので、最後に仕様を満たす実装とは何かを定義します。
任意の入力$x \in X$に対して、その入力と、実装の返り値が仕様の関係を満たしていることが言えればいいので、以下のように書けます。

\operatorname{verify} : \forall x \in X, \operatorname{specification} x\, (\operatorname{implementation} x)

##例
ソート関数を例に見ていきます。
以降、コードは形式検証ツールの1つである定理証明支援系Coqで説明したいと思います。

###仕様が実装を満たすことを定義する
まず、仕様が実装を満たすことverifyを定義します。

Definition verify (X Y:Type)
           (specification:X -> Y -> Prop) (implementation:X -> Y) :=
  forall x:X, specification x (implementation x).

集合$X,Y$はそれぞれ型X Y:Typeで表します。

また、集合$2$ですが、Coqでは命題を表すとき、通常のブール値の型boolよりも命題の型Propを使うのが一般的なので、仕様specificationの型はX -> Y -> Propとします。

その上で述語verifyは仕様specificationと実装implementationを受けとって、それが仕様を満たしていることを示す命題forall x:X, specification x (implementation x)を返す関数として定義できます。

###ソート関数の実装
ここでは自然数リストのソート関数mysort:seq nat -> seq natを定義したとき、これを形式検証することを考えます。²

Definition mysort : seq nat -> seq nat := (* omitted *).

Let implementation : seq nat -> seq nat := mysort.

ソート関数は数学的には以下のような関数だと考えることができます。

\operatorname{mysort}:\mathbb{N}^* \to \mathbb{N}^*

###ソート関数の仕様

今、実装として考えたいのはソート関数mysortなので、verifyにおける型X,Yはそれぞれseq nat,seq natとなります。
つまり仕様はseq nat -> seq nat -> Prop型で記述することになります。

Coqのライブラリにはソートされている状態を表す関数sorted:forall T:eqType, rel T -> seq T -> boolがあるので、これを使って仕様を定義します。³⁴

Let specification : seq nat -> seq nat -> Prop :=
  fun _ => sorted leq.
(* fun input output => sorted leq output *)

これを数学に直すと以下のような関数になります。

\operatorname{specification}:\mathbb{N}^* \to \mathbb{N}^* \to 2\\
\operatorname{specification} x\,y := \operatorname{sorted}\,(\lambda nm.n \leq m)\,y

###ソート関数の形式検証
そこで、ソート関数が仕様を満たしていることを示してみたいと思います。

Theorem mysort_verify : verify specification implementation.
Proof.
  done.
Qed.

本記事では詳細は説明しませんが、先ほど定義したverifyを使って、このように書くことによってspecificationとimplementationがverifyを満たすこと、つまりどんな入力をもらっても、mysortはソートされた列を返すことを保証できます。

しかし、これで本当に検証がうまくいったのでしょうか？

#形式検証の問題点

実は形式検証を行う上で考えなければならない問題があります。
その1つとしてあげられるのは「仕様は十分設計通りに記述できているか」です。

##先ほどの例で解説
先ほどのソートの例をテストしてみます。

Eval compute in (mysort [:: 3; 5; 1; 2]).
(* = [::]
   : seq nat *)

なぜか空列が返ってきました。本当は[:: 1; 2; 3; 5]が返ってきてほしいのですが...

実はmysortの実装は以下のように何をもらっても空列を返す関数になっていました。

Definition mysort : seq nat -> seq nat := fun _ => [::].

しかしながら空列はsortedを満たすので、先程の命題が証明でき、verifyしてしまったというわけです。

##この例の問題点を数学的に見る

もう一度、仕様と実装を数学的にみてみましょう。

\operatorname{specification}:X \to Y \to 2\\
\operatorname{implementation}:X \to Y

まず仕様ですが、$Y \to 2$と$Y$のべき集合$2^Y$は同型なので、以下の2つは同型になります。⁵⁶

(X \to Y \to 2) \sim (X \to 2^Y)

つまり仕様と実装は以下のようなものとみなすことができます。

\operatorname{specification'}:X \to 2^Y\\
\operatorname{implementation}:X \to Y

このとき仕様が実装を満たすことは以下のように書き換えることができます。

\operatorname{verify}:\forall x \in X, \operatorname{implementation} x \in \operatorname{specification'} x

言い換えるならば、「仕様」とは入力に対する出力の部分集合への対応であり、「仕様を実装が満たす」とはあくまで実装がその出力の部分集合の中の1点を返すことを保証するだけであるということです。

先ほどの例だと、仕様sorted leqはただソートされている列全体の集合であって、その中の1点さえ返せば「仕様を満たす」と言えてしまうため、空列を返す関数がverifyしてしまったというわけです。

しかしながら、本当は元の列をソートした値が返ってきてくることを示したいですよね。
次にそれをどのようにして保証するかを考察していきます。

##解決策
解決策として考えられるのは以下のようなものです。

###仕様の条件を厳しくする
仕様とは各入力による出力の部分集合への対応なので、この部分集合を小さくすれば、つまり仕様の条件を厳しくすればいいということです。
究極的には仕様が1点集合であれば、仕様を満たすことと想定されていた返り値を返すことが同値であることが分かるので、仕様を満たすことを証明することによって設計通りの返り値を得ることを保証することができます。

仕様が一意性を満たすことは、以下の命題が成り立つことを示せばいいです。⁷

\forall x \in X, \forall y, y' \in Y, \operatorname{specification} x\,y \to \operatorname{specification} x\,y' \to y' = y

Definition unique_specification (X Y:Type) (specification:X -> Y -> Prop) :=
  forall x y y', specification x y -> specification x y' -> y' = y.

先ほどの例でいえば、sortedの他に、入力と出力が置換の関係であれば、仕様を満たす点の集合が1点集合になることが保証されます。

Let specification2 : seq nat -> seq nat -> Prop :=
  fun input output =>
    sorted leq output && perm_eq input output.

  Theorem specification2_unique : unique_specification specification2.
  Proof.
    (* omitted *)
  Qed.

しかしながら、一般には1点集合になるような仕様を記述するのは難しく、乱数を使う場合や「半順序でソートするためのアルゴリズムとは？」のように、出力の候補が複数あり、その中の1つが出力されればいいというものに対してはうまく使えません。

現時点で私はより良い方法は思いつきませんでしたが、あくまで形式検証で保証できるのは仕様の条件を満たす何かの出力を1つ得られるということであり、プログラマが想定している出力を保証しているわけではないということを意識するということが大事だということが言えると思います。

#まとめ
形式検証で保証できることについて、数学的な観点で考察していきました。
結果的に「仕様」とは入力に対する出力の部分集合への対応であって、「実装が仕様を満たすこと」はあくまで実装が仕様の部分集合の点を1つ返すことを保証しているに過ぎないことがわかりました。
特に仕様を決める際、常にこれを意識することが大事であることがわかりました。

1. 他にも表記はありますが、あえて$2$と記述する理由は後述します。 ↩

2. 型T:Typeに対し、seq Tは要素がTのリストを表す型です。 ↩

3. eqTypeは型のうち、等号==が有限時間内に計算できるものを指します。自然数の型natはeqTypeなので、問題なくsortedが使えます。 ↩

4. sortedの返り値はbool型ですが、Coqではcoercionによって自動的にProp型に変換されます。 ↩

5. $P:Y \to 2$と$S \in 2^Y$に対し、$\forall y \in Y, P,y \leftrightarrow y \in S$で、一対一対応。 ↩

6. $2 := \{\top,\bot\}$と記述したのはべき集合の表記に合わせるためです。 ↩

7. この命題は1点集合であることではなく、1点集合であるか空集合であるかのどちらかであることを表していることに注意。空集合でないことは実装が仕様を満たすことによって副次的に示せるので、仕様に対してはこの一意性の命題のみを示せば十分です。 ↩