アカウント名:
パスワード:
普通のCとかC++の形式検証ってあまり進んでいないのか。どんなスパゲッティなプログラムであっても、検証可能だ（になって欲しい）
それって グラフ同型問題 [wikipedia.org] の一種じゃない??
解けなくはないだろうけれど、今判っているアルゴリズムが全部NPなのでは、よほど簡単な例以外実用にならないぐらい時間がかかる事になる。実用にならないから作ってない、ってことじゃないかと
デジタル回路の設計の世界では実用化されています。
えぇ、それは知っています。すでに述べたようにコンパイラの最適化でも利用されていますからね。
問題はこうです。「Verilogなどに比べると、C, C++ は形式検証がしづらい。だからあまり応用されていない。さ、なぜでしょう？」
ちなみに、Java などでは結構使われています。JITコンパイラが「ランタイムに」最適化をかけても間に合うのはこのため。また、CやC++でも「同形判定」ではなく、『バグの元になりやすいパターン』を検出し警告を出す(lintとか)世界ではよく使われています。
でも、C, C++ の形式検証はむつかしくなります。同形判定ができなくなります。演算量がNPになる
1) 厳密な同形性の判定ってそんなに大切？ 人間がソースを変えたなら何か変更したい意図があったのでは？
えぇ、意図はあったんでしょう。ただし、そのコードがその意図を「正しく反映している」保証はありません。そして、「論理的には正しくないが、文法的には正しい」状態は腐るほどあります。とくに文法のあちらこちらに「未定義」「実装依存」といった曖昧さがあると酷いことになる。# なにしろ、Cの場合 int が何ビットなのか、すら「実装依存」ですからね。
Javaなどはこの辺が厳密です。なので、意味論的な揺らぎが少なく、結果、形式検証が高い意味をもつ。
.
1) 自動で y =
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
私はプログラマです。1040 formに私の職業としてそう書いています -- Ken Thompson
言うほど簡単だろうか? (スコア:1)
それって グラフ同型問題 [wikipedia.org] の一種じゃない??
解けなくはないだろうけれど、今判っているアルゴリズムが全部NPなのでは、よほど簡単な例以外実用にならないぐらい時間がかかる事になる。実用にならないから作ってない、ってことじゃないかと
fjの教祖様
Re: (スコア:2)
形式検証にはいろいろあるのですが、デジタル回路の設計の世界では実用化されています。もうないと生きていけません。
論理多項式にしてその同型性を比較します。論理多項式といってもand or だけではなく一階論述式を使えます。（たしか使えるはず）
現実的に本当に同形なものを常に同形と判断できるか というと できない が簡単な答えになります。加算回路の実装方式はいろいろあるのですが、ばらばらにしてしまったものと元の足し算の間の同型性の判断はまじめにやるだけ無駄 と考えられています（数年前は）。NP であることは最初から分
Re: (スコア:1)
えぇ、それは知っています。すでに述べたようにコンパイラの最適化でも利用されていますからね。
問題はこうです。「Verilogなどに比べると、C, C++ は形式検証がしづらい。だからあまり応用されていない。さ、なぜでしょう？」
ちなみに、Java などでは結構使われています。JITコンパイラが「ランタイムに」最適化をかけても間に合うのはこのため。また、CやC++でも「同形判定」ではなく、『バグの元になりやすいパターン』を検出し警告を出す(lintとか)世界ではよく使われています。
でも、C, C++ の形式検証はむつかしくなります。同形判定ができなくなります。演算量がNPになる
fjの教祖様
Re: (スコア:2)
1) 厳密な同形性の判定ってそんなに大切？
人間がソースを変えたなら何か変更したい意図があったのでは？
つまり同型性判定を行いたい場合で、diff みたいなtoolでは比較できない場合は、つねになんらかなの違いがあるのでは？
2) 未定義な部分を比較してもしかたがないのでは？
!= なのか !== なのか。
例のような場合、オイラが欲しいのは、
1) 自動で y = p->x でp == NULL の場合が直近でチェックされていないのを見つける。
2) p == NULL になる場合があるのか、ないのか遡って調べてくれる
ような tool.
p == NULL
Re: (スコア:1)
えぇ、意図はあったんでしょう。ただし、そのコードがその意図を「正しく反映している」保証はありません。
そして、「論理的には正しくないが、文法的には正しい」状態は腐るほどあります。とくに文法のあちらこちらに「未定義」「実装依存」といった曖昧さがあると酷いことになる。
# なにしろ、Cの場合 int が何ビットなのか、すら「実装依存」ですからね。
Javaなどはこの辺が厳密です。なので、意味論的な揺らぎが少なく、結果、形式検証が高い意味をもつ。
.
fjの教祖様
Re:言うほど簡単だろうか? (スコア:2)
いや。限定的な範囲の中で、想定外のことが起きない、あるいは自分の想定と、コードとの間にずれがないことを知りたい。
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 使わないっだったけ。