「プログラムの形式検証」記事へのコメント

言うほど簡単だろうか?

[okky (2487)]

普通のCとかC++の形式検証ってあまり進んでいないのか。
どんなスパゲッティなプログラムであっても、検証可能だ（になって欲しい）

それって グラフ同型問題 [wikipedia.org] の一種じゃない??

解けなくはないだろうけれど、今判っているアルゴリズムが全部NPなのでは、よほど簡単な例以外実用にならないぐらい時間がかかる事になる。実用にならないから作ってない、ってことじゃないかと

--
fjの教祖様

Re:

[gm300 (14617)]

えっと、えっと。
形式検証にはいろいろあるのですが、デジタル回路の設計の世界では実用化されています。もうないと生きていけません。
論理多項式にしてその同型性を比較します。論理多項式といってもand or だけではなく一階論述式を使えます。（たしか使えるはず）
現実的に本当に同形なものを常に同形と判断できるか　というと　できない　が簡単な答えになります。加算回路の実装方式はいろいろあるのですが、ばらばらにしてしまったものと元の足し算の間の同型性の判断はまじめにやるだけ無駄　と考えられています（数年前は）。NP であることは最初から分

Re:

[okky (2487)]

デジタル回路の設計の世界では実用化されています。

えぇ、それは知っています。すでに述べたようにコンパイラの最適化でも利用されていますからね。

問題はこうです。「Verilogなどに比べると、C, C++ は形式検証がしづらい。だからあまり応用されていない。さ、なぜでしょう？」

ちなみに、Java などでは結構使われています。JITコンパイラが「ランタイムに」最適化をかけても間に合うのはこのため。また、CやC++でも「同形判定」ではなく、『バグの元になりやすいパターン』を検出し警告を出す(lintとか)世界ではよく使われています。

でも、C, C++ の形式検証はむつかしくなります。同形判定ができなくなります。演算量がNPになる

--
fjの教祖様

Re:言うほど簡単だろうか?

[gm300 (14617)]

うーむ。
1) 厳密な同形性の判定ってそんなに大切？
  人間がソースを変えたなら何か変更したい意図があったのでは？
つまり同型性判定を行いたい場合で、diff みたいなtoolでは比較できない場合は、つねになんらかなの違いがあるのでは？

2) 未定義な部分を比較してもしかたがないのでは？
  != なのか !== なのか。

  例のような場合、オイラが欲しいのは、

1) 自動で y = p->x でp == NULL の場合が直近でチェックされていないのを見つける。
2) p == NULL になる場合があるのか、ないのか遡って調べてくれる

  ような tool.

　p == NULL の時に y = p->x はよくない。それは事実。
  だからといって文法的に許されるのに、p->x を全部禁止するのは意味がない。 (文法的に許さないというのもひとつの考え方。)
  使用状況が限定されていれば、関数localで検査する必要はない。馬鹿ばかしいが、if( p != NULL && function(p) != 5 ) .. みたいに一回だけfunctionが呼ばれている場合。

「Verilogなどに比べると、C, C++ は形式検証がしづらい。だからあまり応用されていない。さ、なぜでしょう？」に対する答えは、作業フローの差ではないかと思う。
1) Verilog の場合は、記述する人、シリコンに実装する人が異なり、記述する人がいいと思ってもその意図は伝わらない。意図ではなく、自動的な方法で検証できないといけない。
2) Cコンパイラに比べるとはるかにマイナーなツールでどんどん変形する。より多くの変形ミスの可能性がある。
3) Verilog シミュレータは遅く、実際に使われる期間は長く、ハードのバグは、ソフトよりも出荷後の修正が格段に大変だからより自動検証のデマンドがある。
0) 回路のほうがアトミックな構造が単純だから。これは説明のしかたが悪そう。どう直したらいいかよくわからない。

「あまり」なのか「ほとんど全く」なのか知りたいよん。

Re:言うほど簡単だろうか?

[okky (2487)]

1) 厳密な同形性の判定ってそんなに大切？
    人間がソースを変えたなら何か変更したい意図があったのでは？

えぇ、意図はあったんでしょう。ただし、そのコードがその意図を「正しく反映している」保証はありません。
そして、「論理的には正しくないが、文法的には正しい」状態は腐るほどあります。とくに文法のあちらこちらに「未定義」「実装依存」といった曖昧さがあると酷いことになる。
# なにしろ、Cの場合 int が何ビットなのか、すら「実装依存」ですからね。

Javaなどはこの辺が厳密です。なので、意味論的な揺らぎが少なく、結果、形式検証が高い意味をもつ。

.

1) 自動で y = p->x でp == NULL の場合が直近でチェックされていないのを見つける。
2) p == NULL になる場合があるのか、ないのか遡って調べてくれる

    ような tool.

1 であれば、最近の lint はできます。つーかgccのワーニングオプションを全部 on にすれば当然できる。
というかですね、1はできて当然です。だって最適化フェーズで「p==NULLの場合があるかどうか」をチェックできている。

   int y = p->x;
 
   if ( p == NULL ) {
      return ERROR;
   }

だと if 文は消失しますが、

   if ( p == NULL ) {
      return ERROR;
   }
 
   int y = p->x;

だと、if文は消失しません。

.

2はちょっと難しい。「pがNULLになる可能性を考慮したコードになっていない」事をチェックするのは簡単ですが(そういう文法チェッカーはある)、pがNULLに「ならない」事をチェックするとなるとシステムコールや標準ライブラリも含めた、全コードが必要になる(正確には、入力条件の厳格なルール記述と、出力の値範囲が全部できていればいいんですが)。

また、実際には「pがNULLになるかどうか」じゃなくて、一般的に「変数xが値のレンジaaa-bbb になる可能性」が本当に欲しい機能ですよね?

--
fjの教祖様

Re:言うほど簡単だろうか?

[gm300 (14617)]

>また、実際には「pがNULLになるかどうか」じゃなくて、一般的に「変数 xが値のレンジaaa-bbb になる可能性」が本当に欲しい機能ですよね？
  いや。限定的な範囲の中で、想定外のことが起きない、あるいは自分の想定と、コードとの間にずれがないことを知りたい。
　y = p->x ;
    if( p == NULL ) ..

  と書いたなら、y= の式のときに意味があるx が取れることを知りたい。意味があるyが取れてさらにp がNULL であるかをチェックできることを知りたい。残念ながらこの場合はそういったことはできない。p がNULL の時にif(p==NULL)まで行き着くことはできない。未定義なんで「できるとは限らない」のほうが正しいかも。

>2はちょっと難しい。... pがNULLに「ならない」事をチェックするとなるとシステムコールや標準ライブラリも含めた、全コードが必要になる
  ここでも反論したい。全コードを食わせて自動で答えが有限の時間のなかででればうれしい。それが、「なる」でも「ならない」でもなきく「わからない」であっても。常に、24時間待ちたいとは思わない。部分的なソースとその前提条件を入力して2分で答えを知るという方法も欲しい。答えが不満ならば、前提条件を絞ったり、ソースを足したり引いたりして答えを調整したい。上位の腐った関数のために、それ以降の動作が全部不定になってしまい検証ができないのはまずい。不定になる部分はとりあえず捨ててそれ以外の部分を検証したい。make -k みたいに。Java な人はmake 使わないっだったけ。