形式仕様は厳密に書けて、正確であるという意見がある。
だから
形式仕様を使ったほうがいいと。
ある程度は正解だけど、過信しないほうがいい。
形式仕様でも、あいまい性を含んだり、とんでもない間違いをしでかすこともある。
具体的に見てみよう。
■そのまえに
形式仕様を復習しておこう。形式仕様には
形式仕様言語
・証明をして、正当性を確認するもの：Ｂメソッド
・値を入れて、確からしさを確認するもの：ＶＤＭ
モデル検査
・デッドロックは起こらないとかの確認：ＳＰＩＮ等
・並行性や詳細化の妥当性確認：ＣＳＰ
・時間的にＯＫ？：ＵＰＰＡＡＬ
ってなかんじになる。ＺやＥｖｅｎｔ－Ｂは、証明による正当性に軸足を置きつつ、データによる確認もやろうと思えば出来る。ＶＤＭは、データによる確認に軸足を置きつつ、最近、証明による正当性もかくにんできるようだ。
モデル検査に関しては、もっといろいろある。
■証明をして、正当性を確認するもののリスク
これらのものは、
・不変条件と事前条件が成立するときに
・最終的に、事後条件と不変条件を満たすか？
ということを「論理的に」確認していく。
ここで、「論理的に！」というのがミソ。
論理的にとは
Ａ ならば Ｄ
というのを確認していく。
このとき、命題Ａが偽ならば、Ｄは真のときはもちろん、偽のときでも真になる。
このことは、不変条件に偽の命題を書いてしまうと、何でも真になったことになり、証明できてしまうことを意味する。うっかり１＋１＝３ならば。。。みたいなことを書いてしまうと、証明ＯＫで通っても、バグは入るのだ（１＋１＝３と書くバカはいないが、間違いを書くやつはいる）。
それと、現状のマシンスペックと論証能力では、機械ですべての論証を自動的に行うことは難しい。
そこで、Ｂメソッドでは、証明中に、ある正しい命題を教えてあげて、それをもとに、証明をさせるようにするのだが、この正しい命題というのが、自分では正しいと思っていても、ほんとは間違っていると、ここでもバグが入る危険がある。
そして、基本的には、論理性を確認するだけなので、非機能要件に関して調べることは直接は出来ない。もし、そんなことを調べたいとしたら、そういうことをモデル化しないといけないが、そんな面倒なことをする場合は、モデル検査する。
■値を入れて、確からしさを確認するもののリスク
これは、値をいれて確認しているだけで、証明しているわけではない。
だから、本当に正しいことを数学的に示しているわけではない。
この値だったからうまく行ったということはありえる。
■モデル検査のリスク
モデル検査は、しらべたいことを時相論理式（ＬＴＬ）で記述するものがある（ＳＰＩＮなど）。このＬＴＬに間違いが入る危険性がある（思っていることを正しく表現していない）
また、モデル化する場合、ある程度の捨象を行うので、捨象しすぎると、本当の問題点まで捨象してしまう危険がある。捨象（モデル化）の際に間違いも入る可能性がある。
ということで、形式仕様でも、バグが入るリスクはあるし、書き方によってはあいまいにかけてしまい、そこにチェック(証明）が入らないリスクもある。
じゃあ、形式仕様は意味ないかというと、そんなことは全然なくて、形式仕様で書こうとする事によって、もうそれだけで、証明しなくても、厳密性は増す。
ただ、それは「かなり出来る人が」「ものすごく出来るようになる」場合に有効なことなのであって、
自然言語で書いてもだめだめな人が、形式仕様で書けば、ばっちりになるかというと、そういうわけではない。
だめだめなやつは、
なにをやっても
だめだめなのだ。
アクセス
トータル
ランキング
