人力検索はてな
モバイル版を表示しています。PC版はこちら
i-mobile

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


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


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

●質問者: garyo
●カテゴリ:コンピュータ 科学・統計資料
✍キーワード:Coq カリー ハワード バグ プログラム
○ 状態 :終了
└ 回答数 : 8/8件

▽最新の回答へ

1 ● a-kuma3
●24ポイント

無理だと思うな。


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


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

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


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


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


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

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


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


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

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


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

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

◎質問者からの返答

ありがとうございます。

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

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

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

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

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

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

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

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


2 ● taroe
●24ポイント

無理

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

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


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

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

◎質問者からの返答

ありがとうございます。

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

ただ、やはり

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

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

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

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


3 ● みずぴー
●24ポイント

リンク先の人間です。

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

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

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

の3つです。

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

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

◎質問者からの返答

mzpさん、こんにちは。

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

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

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

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

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

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

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

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

というイメージと、

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

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

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

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

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

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


4 ● toki-2131
●1ポイント

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

◎質問者からの返答

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


5 ● みずぴー
●23ポイント ベストアンサー

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

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

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

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

となります。

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

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

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

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

仕様とプログラム

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

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

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

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

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

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

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

◎質問者からの返答

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

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

->が関数だとすると

f(a)=b

g(b)=c

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

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


1-5件表示/8件
4.前の5件|次5件6.
関連質問


●質問をもっと探す●



0.人力検索はてなトップ
8.このページを友達に紹介
9.このページの先頭へ
対応機種一覧
お問い合わせ
ヘルプ/お知らせ
ログイン
無料ユーザー登録
はてなトップ