バグの無いプログラムを作ることは可能ですか?



停止性問題から「バグのないプログラムは存在しない」(あるいは「プログラムにバグの無いことは証明できない」)と良く言われますが、
Coqによる証明駆動開発
http://d.hatena.ne.jp/mzp/20110228/ruby
ではプログラムを証明できるみたいですが、これは冒頭の1文が可能ということでしょうか?


あと、
「カリー・ハワード同型対応」
について教えて下さい。

回答の条件
  • 1人5回まで
  • 登録:
  • 終了:2011/03/08 23:10:02
※ 有料アンケート・ポイント付き質問機能は2023年2月28日に終了しました。

ベストアンサー

id:mzp No.5

回答回数9ベストアンサー獲得回数1

ポイント23pt

興味を持っていただけたようで、とても嬉しいです。

カリーハワード同型について

具体的な例で説明しますと、ソクラテスさんを殺すことで有名な三段論法を命題論理で書くと

(A->B) -> (B -> C) -> A -> C

となります。

で、これが真であることを証明するには、

  • 推論規則を使って変形していき、真を導く
  • ('a -> 'b) -> ('b -> 'c) -> 'a -> 'cという型を持つ関数が存在することを示す(= 実装してみる)

の2つの方法があります。

このように、推論規則を用いた証明と関数の実装が対応するのがカリー・ハワード同型です。

ただ、「だからどうした?」と言われるとボクにはうまく答えれません。せいぜい「型チェックモジュールを再利用して証明チェックもできて嬉しいよね」ぐらいしか答えれません。

仕様とプログラム

Coqというのは仕様の記述もできて、プログラムも組める言語なのでしょうか?

についてですが、簡単に答えるとyesです。

ボクの認識では仕様は「どのような性質を持つか」を記述したもので、プログラムは「どのようにそれを実現するか」を記述したものです。

http://d.hatena.ne.jp/yoshihiro503/20090923/p1 の例だと、「mergesortの結果はソートされている」という仕様を表現するためにSortedという述語を使っています。 Sortedはどのような性質をもつべきかは定義されていますが、どのようにそれを実現するかは定義されていません。

一方、プログラムはmergesort関数ですが、こちらは「どのように実行するか」は定義されていますが、どのような性質を満すかは定義されていません。

最後に、mergesort_sorted定理を証明することで、プログラムが仕様を満すことを証明しています。

このようにCoqでは仕様とプログラムの両方を記述して、プログラムが仕様を満すことを証明できます。

id:garyo

mzpさん、こんにちは。ありがとうございます。

('a -> 'b) -> ('b -> 'c) -> 'a -> 'cという型を持つ関数が存在することを示す(= 実装してみる)

->が関数だとすると

f(a)=b

g(b)=c

h(f(a))=g(b)=c

合成関数が存在することと三段論法は同じことでしょうか?

2011/03/05 11:38:49

その他の回答7件)

id:a-kuma3 No.1

回答回数4971ベストアンサー獲得回数2153

ポイント24pt

無理だと思うな。


一般的に、仕様を出す側と実装する側が分かれているとして、バグ(仕様を出す側の期待通りに動いてくれない)の原因として、以下のようになると思う。

  • 仕様が不完全

  • 仕様の誤解

  • (仕様は正しく理解しているが)正しく作れていない

  • その他


「Coqによる証明駆動開発」は、面白いと思うけど、仕様から「証明」を正しく導き出せている、という証明ができない。

従来の「仕様の誤解」によるバグと同列。


また、「その他」の中には、コンパイラやスクリプトエンジンのバグによる、というものもあるので、それも、証明駆動では解決できない。


「証明が正しいとしたら」という前提を置くなら、従来の手法でも、「テストケースが正しいとしたら」という前提を置くのと、何ら変わりが無いので、証明駆動だからどうだか、ということにはならない。


テスト駆動との比較も、多分に、恣意的な感じが否めない。

テスト駆動を正しく理解している人が、BASE64 の実装をするときに、ランダムに抽出したデータの確認だけで済ませるはずがない。


実装しようとしている対象の領域によっては、テスト駆動に比べて、楽に必要十分なテストができます、というふうに読むなら、同意できるかな、という感じ。


仮に、「ひとつでもバグが無いプログラムを作成できるなら、バグが無いプログラムを作ることは可能である」として、コンパイラのバグも考えないとしたなら、

「Hello world」級のプログラムなら、従来の手法でも、バグが無いプログラムを作れることになりますよね。


「カリー・ハワード同型対応」については、「論理の哲学」って本を読んでみたことはあるんだけど、僕には難し過ぎて、よく分からない。

他の人に解説を譲ります :-)

id:garyo

ありがとうございます。

「カリー・ハワード同型対応」は

http://www.at-akada.org/blog/2008/12/post-275.html

「論理学の証明と関数型言語のプログラムが一対一対応する」

これにより、論理学の方で証明しておけば、必然的にプログラムの方も証明されるということらしいですが、今ひとつどう対応するのか良くわからないので、どなたか教えていただきたいです。

リンク先の以下の話も面白いです。

関数型言語にcall/ccを加えると古典論理になるらしい。call/ccって背理法だったらしいぞ!なんだってー!!

(ちょっと調べるとcall/ccの方が広いみたいだけど)。

つまりあれだ、二重否定除去とか背理法とかうさんくさいから止めて直観主義論理でいこうというのは「call/ccとか黒魔術だから使うのやめよう」というのに相当する(たぶん)。

2011/03/02 11:42:08
id:taroe No.2

回答回数1099ベストアンサー獲得回数132

ポイント24pt

無理

http://d.hatena.ne.jp/yoshihiro503/20090923/p1

この例だと、証明の仕方が正しいかどうかの検証はしてない。


カリー・ハワードの対応(Curry-Howard correspondence)に関しては以下が簡潔に説明してます。

http://itpro.nikkeibp.co.jp/article/COLUMN/20070909/281498/

id:garyo

ありがとうございます。

2番目のリンク先分かりやすいです。

ただ、やはり

 型が論理式(命題)にあたるとすれば,その型を持つ式(プログラム)は何にあたるのだろうか? 実は,「式」は「型」が表す命題の証明とみなすことができる

というあたりから分からなくなってきます。

例えばCoqが有名で,グラフ理論の四色定理やCコンパイラの正しさなど,様々な性質が厳密に検証されている。

「Cコンパイラの正しさ」の確認と「バグの有無」はどういう関係にあるのかと、定理証明器でなぜプログラムが正しいことが証明できるのかがよく分からないです。(Coqでやる証明とプログラムの関係?)

2011/03/02 11:33:56
id:mzp No.3

回答回数9ベストアンサー獲得回数1

ポイント24pt

リンク先の人間です。

「証明駆動でバグがなくせる!」はわりとFUDで、実際はある種のバグを潰せるだけです。

証明駆動でやっているのは

  1. 仕様と実装をCoqで記述する
  2. 仕様が満すべき性質を証明する
  3. 実装が仕様を満すことを証明する

の3つです。

2.のおかげで仕様同士の矛盾を排除でき、3.のおかげで仕様と実装の食い違いを排除できます。ですので、Coqを使うことで「矛盾する仕様に起因するバグ」と「仕様と実装の食い違いによるバグ」を排除できます。もちろん仕様の誤解や、要件と仕様の食い違いなどには太刀打ちできません。

あと、Coq自体にバグが含まれる可能性は否定できませんが、小さくて枯れたコア部分 + その上に構築された便利な機能という構成なっているので、致命的なバグが含まれる可能性は低いはずです。

id:garyo

mzpさん、こんにちは。

「Coq to Rubyで初める証明駆動開発」の記事興味深く拝見させて頂きました。

全てのバグを無くすことが不可能だとしても、

「ある条件(前提下)の元で○○のバグを無くすことができる」

というのはとても興味があったので、質問してみました。

質問自体は「(全ての)バグの無いプログラムを作ることは可能ですか?」と読めて、

「無理」という回答が多いと思いますが、

実際にはCoqによる証明駆動開発というのはどんなのだろうと思い質問してみました。

良くわからないのは「論理学の証明と関数型言語のプログラムが一対一対応する」

というイメージと、

>仕様と実装をCoqで記述する

>仕様が満すべき性質を証明する

>実装が仕様を満すことを証明する

上記がどのように行われるのかです。

Coqというのは仕様の記述もできて、プログラムも組める言語なのでしょうか?

宜しければまた教えてください。

2011/03/04 09:05:40
id:toki-2131 No.4

回答回数138ベストアンサー獲得回数1

ポイント1pt

つくれたらつくってください

id:garyo

不適切な解答にチェックを入れました。

2011/03/04 20:56:10
id:mzp No.5

回答回数9ベストアンサー獲得回数1ここでベストアンサー

ポイント23pt

興味を持っていただけたようで、とても嬉しいです。

カリーハワード同型について

具体的な例で説明しますと、ソクラテスさんを殺すことで有名な三段論法を命題論理で書くと

(A->B) -> (B -> C) -> A -> C

となります。

で、これが真であることを証明するには、

  • 推論規則を使って変形していき、真を導く
  • ('a -> 'b) -> ('b -> 'c) -> 'a -> 'cという型を持つ関数が存在することを示す(= 実装してみる)

の2つの方法があります。

このように、推論規則を用いた証明と関数の実装が対応するのがカリー・ハワード同型です。

ただ、「だからどうした?」と言われるとボクにはうまく答えれません。せいぜい「型チェックモジュールを再利用して証明チェックもできて嬉しいよね」ぐらいしか答えれません。

仕様とプログラム

Coqというのは仕様の記述もできて、プログラムも組める言語なのでしょうか?

についてですが、簡単に答えるとyesです。

ボクの認識では仕様は「どのような性質を持つか」を記述したもので、プログラムは「どのようにそれを実現するか」を記述したものです。

http://d.hatena.ne.jp/yoshihiro503/20090923/p1 の例だと、「mergesortの結果はソートされている」という仕様を表現するためにSortedという述語を使っています。 Sortedはどのような性質をもつべきかは定義されていますが、どのようにそれを実現するかは定義されていません。

一方、プログラムはmergesort関数ですが、こちらは「どのように実行するか」は定義されていますが、どのような性質を満すかは定義されていません。

最後に、mergesort_sorted定理を証明することで、プログラムが仕様を満すことを証明しています。

このようにCoqでは仕様とプログラムの両方を記述して、プログラムが仕様を満すことを証明できます。

id:garyo

mzpさん、こんにちは。ありがとうございます。

('a -> 'b) -> ('b -> 'c) -> 'a -> 'cという型を持つ関数が存在することを示す(= 実装してみる)

->が関数だとすると

f(a)=b

g(b)=c

h(f(a))=g(b)=c

合成関数が存在することと三段論法は同じことでしょうか?

2011/03/05 11:38:49
id:chinchin-kozou No.6

回答回数198ベストアンサー獲得回数7

ポイント23pt

関数がカリー化されている言語なら理論上は可能です。



カリー化を利用すると、複数の引数をとる関数を、一つの引数のみを取る複数の関数のラムダ計算などの単純な理論的モデルと見なして研究できるようになる

http://ja.wikipedia.org/wiki/%E3%82%AB%E3%83%AA%E3%83%BC%E5%8C%9...

id:garyo

ありがとうございます。

2011/03/05 12:53:24
id:Endows No.7

回答回数169ベストアンサー獲得回数7

ポイント11pt

そのバグをチェックするためのプログラムでさえバグが無いという保障はないので、完全にバグのないプログラムはできません。世界中に存在するウィルスと同じように、誰しもが完全に「存在しない」「撲滅した」とは言い切れないのです。あくまでも「発見されなくなった」程度のことしか言えないものです。

プログラムならば、簡単にアラートメッセージくらいの内容を一文(JavaScriptで言えば「alert("文")」)。というくらいのプログラムなら「ミスはない」などと言えるでしょう。しかし、何行、何十行、何百行となるとたとえ一行一行チェックしたとしても、完全な意味で「バグはない」とは言えません(細部の不具合はほとんどコンピュータ画面上にエラーを出さないほど無視されるものです)。何十年以上かけてデバッグしたとしても完全にバグは取り除かれたという保障は存在しません。

id:garyo

「カリー・ハワード同型対応」やCoqに関してもリンク先を参照の上でご回答願いたく。

2011/03/05 16:24:25
id:tukasa329 No.8

回答回数1ベストアンサー獲得回数0スマートフォンから投稿

それははっきり言って無理。

wikipediaにも書いてあるよ

id:garyo

不適切な解答にチェックを入れました。

「カリー・ハワード同型対応」やCoqに関してもリンク先を参照の上でご回答願いたく

2011/03/05 22:09:13
  • id:seble
    厳密に言えば、世の中に「絶対」というものは存在しない。
    絶対にバグが無い、とか、絶対にバグを発見できる、とかという論理自体が間違っている。
  • id:taknt
    すべてが仕様だと言えば バグではなくなる。
  • id:SweetSmile1978
    SweetSmile1978 2011/03/02 11:01:21
    バグだと思ってサポートに問い合わせたら
    「それは仕様です」と言われちゃったりとか。
  • id:rsc96074
    Hellow world プログラムとか。(^_^;
    β版には本当に仕様でバグを入れておくとか。(^_^;
  • id:b-wind
    「バグ」という言葉の定義から始めにゃならんな。
    それは「仕様」か?「バグ」か?
  • id:taknt
    >厳密に言えば、世の中に「絶対」というものは存在しない。

    それは 絶対ですか?
  • id:seble
    それは言葉尻を捉えるという。
  • id:SALINGER
    そこにバグは存在しない。存在するのは無能なプログラマだけだ。
     
    ・・・ゲイツやジョブスが言いそうな言葉だけど、私が今考えましたw
  • id:ryota11
    プログラマがバグを作るのではない。バグを作るからプログラマなのだ。

    ・・・ゲイツもジョブスも言いそうにない言葉だけど、私が今考えましたw
  • id:taknt
    >それは言葉尻を捉えるという。

    矛盾というやつだろ。
  • id:seble
    絶対が存在する事を証明できなければ絶対が存在しないという真理は絶対である。
  • id:taknt
    まず「真理」は絶対なのかを証明してください。
  • id:standard_one
    プログラム単体で考えればコンピュータは人間が作ったおかしなコードを正常に実行しているだけであり人間がそれを勝手にバグと呼んでいるだけですよね。
    本件を言い換えると「おかしなコードを組まないでもらえますか?」とクライアントに言われた時に「無理です」と答えるか否かということになりますか?
  • id:niwa-mikiho
    そもそも証明しようとする人が開発者のみという時点でそのコードの健全性を証明出来てない。


    開発者というのコードの動作をある程度把握してるから、バグを再現させる手順すらも身につけてる。
    この時点でレールに沿った行動とも言えるかと。
  • id:youta0
    あはは:::
  • id:kuro-yo
    バグの無いプログラムを作ることは「可能」であるはずです:
    さもなければ、全てのプログラムには必ずバグが存在する事になるからです。

    …だからと言って、「実用的な時間内に」作れるかどうかは、また別の問題。
  • id:ANKAWA
    むりですね
    だってバグのないゲームなんてないでしょ?
    ドラクエだつてポケモンだって探せばたっくさんありますよ
  • id:kia_44
    rsc96074さんのコメントにあるように、単純なプログラムなら可能ではないでしょうか。
    想定外がなければいいわけですから、インプットの無いプログラムなら~とか。
  • id:taknt
    a=1

    このプログラムにおけるバグは?

    バグは条件によってさまざま変わります。

    たとえば 2をセットしないといけないのに 1をセットしてたら それで バグです。
    ほかにも いろいろありますけどね。

この質問への反応(ブックマークコメント)

「あの人に答えてほしい」「この質問はあの人が答えられそう」というときに、回答リクエストを送ってみてましょう。

これ以上回答リクエストを送信することはできません。制限について

回答リクエストを送信したユーザーはいません