原因結果グラフを利用した形式仕様記述

形式仕様記述というと述語論理から始まるが、命題論理でもやれることは多い。その一つが原因結果グラフである。これについては以前インタフェース誌[1]に書いたことがある。しかし、最近ニフィのK氏がCEGTestをリリースされたのだがどうも仕様が違う様なので悩んでいる。また、FXのA氏のツール(X-CEG)とも違う様だ。特にMASKの扱いが違う。それで本当はどうなのか少し整理しておきたい。インタフェース誌[1]に掲載した変換規則を以下に示す。元ネタは[2]である。EとOは要素数が3ヶ以上の時は論理式の形が変わる。それは[1]を参照。

原因結果グラフの本来の使い方はテストケースを絞り込むことであり、仕様を記述することではない。仕様記述としてはMC/DC等の手法を使って絞り込む前の論理式表現に興味がある。同じ文章から原因結果グラフを作っても人によって違うグラフが出来ることが多い。それは元の文章の解釈の違いを反映するが、論理式で表現すると論理的には等価であることが分かったりする。等価でなくても、どこが違うか明確化できて仕様の解釈のブレをなくすことが出来る。

取りあえず以下の3点が気になっている。

(1)まず原因から結果に向かう線の解釈だけれど、私は⇒(ならば)でなく⇔(同値)をディフォルトで使用していた。これは問題文に依存して決めるべき。例えば、料金表などでは同値関係にしないと別の条件でも同一料金になることを認めることになる。排他的に扱いたいかどうかで使い分ける必要があるだろう。

切符の払い戻しの場合、誤購入の時は必ず払い戻すのであれば
(誤購入)⇒(払い戻し)
となる。払い戻すのは電車が止まってしまった時にも行われるので
(払い戻し)⇒(誤購入)
は成立しない。と言うようなことを考察しないと決められないのだと思う。
一般的には、原因結果グラフの元になる文章はある特定の状況を表すフレーズなのでその範囲では、電車が止まってしまうことなどは想定しない場合が多いので
(誤購入)⇔(払い戻し)

として良い場合が多いように思う。つまり普通は、
(誤購入)⇒(払い戻し)　または　(誤購入)⇔(払い戻し)
だろう。逆向きになるのは原因が目的で、結果が実現方法の様な場合かも知れない。
別の見方としてこれは論理関係ではなく定義であると思った方が良い場合もある。結果を定義しているdefine文のようなものであり、結論を一つの素命題とするのではなく単なるラベルと考える。

(2)MASKは三値論理を使用するのが正しいかも知れない。しかし、その場合結果も不定になることがある。結果が不定でも良いのかは元の文章を書いた人に確認する必要がある。たぶん不定は意図していないのではないか。

(3)これが一番重要かも知れないけれど、原因結果グラフの論理式が真になると言うことがその仕様が矛盾無いと言うことを表す。形式仕様記述は全体が真になる範囲で分析をする。偽になるところは、あり得ないと元の文章を書いた人が言っているところだから分析の対象外にする。テストの場合は、全体の真偽はあまり考えないのか? 全体が偽になるところから選んだテストケースはハードが故障した場合とかユーザーのオペレーションミスのテストに対応するのか?


幾つか事例についてそれぞれのツールの結果を比較してみたい。長くなったので(2)と(3)はまた改めて。


参考文献
[1] 新・組み込みソフトへの数理的アプローチ（第6回）

原因結果グラフ――原因と結果の関係を木構造で表現する

[2]