Think Stitch
PRINCIPIA  最近の更新


計算プログラムの正当性

計算プログラムという言葉はここだけの呼び名ですが、入力を与えられるとガチャガチャ(もうやめます)と動いて結果を出して止まる、というものでした。 もう1度図を出しておきます。数学の関数と見なせるようなプログラムです。

このようなプログラムの正当性(あるいは詳細化関係)とはどのようなものなのかということを書きたいと思います。 正当性とは、平たくいうとプログラムが正しい、ということです。 もう少しちゃんというと、プログラムが仕様を満たしている、ということです。

プログラムの正しさは仕様に対して決まるものなので、まず仕様を表現しなければなりません。 計算プログラムの場合、これは比較的簡単です。 どの入力に対して、どの出力が対応するのか、その対応関係を明確にすればいいからです。

このような対応関係は、文字通り数学でいうところの"関係"で表すことができます。 関係というのはペアの集合です。 例えば、入力を i1, i2, ..., iN とし、それぞれに対応する出力を o1, o2, ..., oN とすると、仕様を表す関係 S は次のように表すことができます。

S = { (i1, o1), (i2, o2), ..., (iN, oN) }

要するに、正しい入出力のペアを表にして並べただけです。これが計算プログラムの仕様です。

計算プログラムの仕様は、そのままテストケースでもあることがわかります。 計算プログラムに入力 i を与えたときの結果が o であったとき、ペア (i, o) が仕様に含まれていれば結果は正しく、そうでなければ誤りということになります。

同様に、計算プログラムの実装が各入力に対して出力する結果を関係として表したものを R とします。 ユーザガイドで、プロセスの正当性について説明したときと同じく、この関係は実行からではなく、プログラムの記述から得ることになります。

さて、問題はこうです。計算プログラムの動作を表す関係 R と、仕様を表す関係 S があるとき、計算プログラムが仕様を満たしているという条件はどのようなものでしょうか。

条件は次のようになります。

  1. S の定義域は R の定義域に含まれている。
  2. S の定義域から入力 i を選んだとき、R によって i が 出力 o に対応するならば、S によっても i が o に対応する。

ここで定義域というのは、関係に含まれるペア (i, o) のうち、左の要素、つまり入力 i だけを集めた集合のことです。仕様でいえば、どのような入力が許容されるのか、ということを表す集合です。 これを dom S と表すことにします。定義域は英語で domain だからです。 仕様 S の場合、dom S は次のようになります。

dom S = { i1, i2, ..., iN }

それぞれの条件を言葉で丁寧に説明すると次のようになります。

  1. 仕様が受け入れなさいといっている入力を、計算プログラムはすべて受け入れなければなりません。
  2. 計算プログラムの出力は、仕様が出力しても良いとしているものの中に含まれていなければなりません。

この条件が成り立つことを、プロセスと同じように記号 S ⊑ R で表します。条件の内容も、雰囲気がプロセスの正当性に似ていると思います。

補足

計算プログラムの正当性条件を記号で表す

定義域の記号 dom S に加えて、もう1つ記号を導入すると、正当性の条件を簡潔に表すことができます。 それは定義域制限演算子というもので、◁ で表します。 演算子の左には集合、右には関係を置きます。 A ◁ R は関係で、その意味は、R の要素のうち、左の要素が A に含まれるペアだけを選んで作られる関係です。 つまり R の定義域を A に制限しているわけです。 数式では次のように定義することができます。

A ◁ R = { (i, o) | (i, o) ∈ R ∧ i ∈ A }

これを使うと正当性の各条件は次のようになります。

  1. dom S ⊆ dom R
  2. (dom S) ◁ R ⊆ S

このように書くと、プロセスの正当性との類似がさらにはっきりすると思います。

リスコフの置換原則

リスコフの置換原則(LSP)についてご存知の方が多いと思います。 リスコフの置換原則は主にオブジェクト指向言語の継承の文脈で語られる原則で、あるメソッドを派生クラスで再定義するときに守らなければならない原則です。

ご存じない方には、定義や意義についてどこかで見ていただくとして、ここで言っておきたいのは上記の正当性条件が基本的にリスコフの置換原則と同じ条件だということです。 つまり、派生クラスで再定義するメソッドは、次の条件を満たさなければなりません。

  1. 受け入れる引数の範囲を広げてもいいけど、狭めてはだめ。
  2. 基本クラスのメソッドが受け入れる範囲の入力に対しては、結果の範囲を広げてはだめ。
2013/08/08
© 2013,2014,2015 PRINCIPIA Limited