なお、障害には「ビザンチン障害」というのがあって、ありとあらゆるケースで正しい反応を示すが、唯一あなたが本当に正しく動作してほしい場合にだけ、誤った結果を出す、という障害がありえます。ですので、ビザンチン障害が全く無いことを証明しなくてはいけません。 # 詳細は Andrew S. Tanenbaum 先生の本を読んでくれ。 .
「完璧ではないもの(バグがありえるもの)」の上で実行された結果を使っても、証明にはならないのですよ。それは CPU であっても同じです。チューリングマシンはそもそも CPU というハードウェアとその上で動くソフトウェアをワンセットにしてモデル化したものですから。
ノイマンじゃないの (スコア:0)
結局非ノイマン型はほとんど日の目を見てないし、他の人たちは彼の考えたフレームワークの上で動いているに過ぎない。
基礎論 (スコア:1)
計算機科学の基礎を築いたという意味ではチューリング [wikipedia.org]もすてがたい。
Re:基礎論 (スコア:4, おもしろおかしい)
基礎も築いたが
「デバッグは無限地獄である(その変更でバグが取れたと言う保証がなされることはありえない)」
という証明もしてくれたすばらしい人。
唯一の問題は、この証明が言っている事を「ちゃんと理解している人」が日本にほとんどいない、ということぐらいだろう。
# 「バグがなくなったという証明を持ってこいっ」と無茶を言う顧客の割合が、日本だけ突出しているのは
# どういうことなのか…
fjの教祖様
Re:基礎論 (スコア:2, 参考になる)
チューリングの停止性問題は、「（任意の）プログラムにバグがないか判定できるプログラム」は存在しないといっているだけで、「バグのないプログラム」が存在しないとは言ってませんよ。
お客に「プログラムじゃなくて人間が判定して持ってこい」と言われたらどうします？
＃「人間はチューリングマシンと同等か」という哲学的問題に発展するが。
Re:基礎論 (スコア:2, 興味深い)
ほら～やっぱりわかっていない人がいる。
それがどうしたのかね?
バグの無いプログラムであることが判明しないなら、同じことじゃないか。
そして、あるプログラムx を別のプログラムp0で判定して「xにバグは無い」と出てきた場合、『p0はあてになるのか?』という問題が発生する。
p0をp1で判定すると『p1はあてになるのか?』、p1をp2で判定すると『p2はあてになるのか』…
p(n)をp(n)で判定すると『p(n)はあてになるのか?』という問題に帰着してしまう。
セキュリティの Chain of Trust も同じだが、「鎖がつながっていることは判った。その鎖の端はどこにつながっているのだ?」という問題が発生する。そして、つながっている先の最初の輪が信頼できるかどうかは、証明できないのだよ。
しないってば。「バグがなくなったという証明を持ってこいっ」が要求なんだから。
人間がチューリングマシンの能力を包括するとしよう。すると人間には2種類の事ができることになる。
1) チューリングマシンができること
2) チューリングマシンにはできないこと
しかし、1の内容と「証明可能な内容の証明」とは等価だ。で、プログラムが誤りがあるかどうかの判定は 1 に属する問題で「不可能」とすでに証明されている。
人間がプログラムを読むことで「2の能力によって」プログラムに誤りがないことは判るかもしれない。しかし、その判定結果が正しいことは証明できない。
ましてや1を完全に包括できていないなら、証明できないに決まっている。
fjの教祖様
Re:基礎論 (スコア:2)
バグの無いプログラムであることが判明しないなら、同じことじゃないか。
ここだけなんですが、
Xが証明できないならXは存在しないのと同じというのは論理的には間違ってますよね。
停止性問題は『「停止性を証明できるチューリングマシン」の不存在』は証明してますけど、
これは、『停止するチューリングマシンがない』というのとは違いますね。
停止するチューリングマシンはありますし。
Re:基礎論 (スコア:1)
アランチューリングの停止性問題の証明は、
「Xのようなプログラムは作れない。だからXは証明できない」
と言っています。
http://ja.wikipedia.org/wiki/%E5%81%9C%E6%AD%A2%E6%80%A7%E5%95%8F%E9%A1%8C [wikipedia.org]
こちらを、特に「証明」の部分を丁寧に読んでいただければ誤解はさっくり解けるかと。
fjの教祖様
Re: (スコア:0)
Re: (スコア:0)
それまた論理の飛躍ですねぇ。
「特定のプログラムに対しては、バグの存在を証明するプログラムが存在しないことは証明できない」という程度のこと話でしょう。
Re:基礎論 (スコア:2)
停止性問題は、停止性を証明できるようなプログラムは作れないと言っているだけで、
停止するプログラムを作れないとは言っていないですよ
Re: (スコア:0)
ランダムに１か０を格納する箱があるとして、その箱の中身を確認する手段がなかったとする。
この状況、証明する手段はないということは言えても、０とも１とも言えない。
バグと停止性問題は全く別の話だけれども、仮に停止性問題と同様だったとして、証明できるのはせいぜい
・プログラムuにバグがないことを証明するプログラムpがあったとすると、そのpを用いて書いたbというプログラムはpに判定させると矛盾した結果を生む。したがって、pというプログラムは存在しない。という程度です。
停止性問題と違って、バグの問題は、矛盾した結論を導くbを書くのは難しいと思いますが、仮に証明できたとして、「uにバグがある」もしくは、「バグのないプログラムはない」とするには証明が不足しているでしょう。
# まさか、似ているからってだけで適用できるなんて思ってないですよね。
Re: (スコア:0)
http://srad.jp/~okky/journal/467651 [srad.jp]
こちらを読んであなたが何を誤解してるのかわかりました。
つまり Pを含む系の正しさをPで正しく解くことはできない のがポイントなのだ。
曖昧な表現なので解釈の仕方がまだまだ難しいですが・・・
たとえば、
他のプログラムの行数をカウントして解くプログラムの集合Ｘを想定すると、
行数をカウントするプログラムP0、P1はその集合に含まれますとします。
仮説：
P0はP1の行数を正しく解くことができる。
「Pを含む系の正しさを
Re:基礎論 (スコア:1)
どこにぶらさげようか迷ったあげくここに!(ごめんなさい
証明とか小難しいことはさておいて(えー!?)
なんかテキトーなことをテキトーにやってくれる(超意訳)コンピューティングってのが
出てきてますね。
http://srad.jp/science/article.pl?sid=09/02/11/0219213 [srad.jp]
今はテキトーな事も律儀に定義して計算させてテキトーっぽく見せてますが、
やっぱり天然でテキトーなのが出てくるようになったら本物かなあと。
テキトーである人間を相手するには証明できる分野で記述しちゃだめなんじゃないかと
思うのです。
Re:基礎論 (スコア:1)
証明できないに決まっている，って思いっきり主観が入っているような気がしますが．
不明瞭な前提と独断的な決めうちばっかりに見えます．
# こういう文書を書くヒマがあるのなら，
# お客さんに提出するバグを一つでも消す努力をしたら良いのに．
そうじゃないだろう！
Re:基礎論 (スコア:1)
元コメであってると思います。その論だと、不完全性定理の方へ落ちてってるような・・・。
たまたま運良くバグ無しが証明出来るプロジェクトもあるかと。「1～100の範囲の数字を受け取って、受け取った数の2倍の数を返すプログラム(それ以外の値の動作は未定義でOK)」だとすると、100回試せば「バグがない証明」になると思うのですが。
で、仰ってるのは、このカギ括弧付きの「証明(笑)」は、理論上完璧な意味での証明ではない。なぜなら、そもそも不完全定理から、数学的に絶対に正しい(無矛盾である)と証明出来る数学体系が存在しない。あらゆる数学体系は『多分大丈夫』と信じられてるだけ。だから「その『数学大系(笑)』上で行ったいかなる『証明(笑)』も『多分大丈夫』以上の意味はない」、すなわち「世の中に意味のある証明など存在しないんだよ!!」と仰ってるだけのような。
考察しきれていないのですが、 チューリングマシンの停止問題の原理を突き詰めていくと、 仰る「チェーンを辿ってってどこにも辿り着けない」、になるんでしょうか? 何となく、「信頼出来る出発点」を仮定してもチューリングマシンには限界がある、という話だと理解していました>停止問題。
なにより、そこまで極端な原理を使ってぶった切るなら「仕様書が不完全だ」「契約の金額計算が正しいことが証明不可能」とかなんとでも言えそうな。
# どっちにしろ、先方にややこしい話が通じるわけがない、と言う意味なら納得ですが。
Re:基礎論 (スコア:2)
チューリングマシンがバグっていないことをチューリングマシン自身が証明できない。って話もあるけど、「バグってなくても証明できないこともある」っていうことが重要なんでは。
# 無限に見せられた人たちは、みんな晩年精神病棟行きみたいなので、これ以上は突っ込みたくありません。(^^;
事態は際限なく悪化する。
Re:基礎論 (スコア:1)
停止問題にしろゲーデルの不完全性定理にしろ、前提として「ある程度以上複雑な体系」においては停止判定できないあるいは無矛盾性を証明できない、というものです。例えば言語仕様からチューリング完全性を取り除いた、簡素化した言語を用いていれば、停止することを証明することができるし、バグがないことも証明可能となります。だから、両者ともに正しい主張です。
Re:基礎論 (スコア:1)
ですから，判定を「別のプログラムp0」でやるのではなく「人間」がやれ，といわれたら？
ここが必ずしも自明ではない。「証明可能」を公理論的かつ有限の立場で定義するのならばそのとおりだが，それを超える「証明」も存在する。はたしてそれが証明になっているのかという議論はあるだけど，数学の世界とかでは多用されている手法ではある。
なので，チューリングマシンには証明できなくても人間には証明できるかもしれない。
しかし「プログラムが誤りがあるかどうかの判定」は「チューリングマシンができること」に属するのにチューリングマシンでは「不可能」だ，って日本語として超絶的に変ですよね。その「変」の部分に停止問題の証明のキモがあるわけなんですが。
Re: (スコア:0, オフトピック)
キミたちが、「証明せよ」と言う単語の意味を理解していない、と言うことがよくわかった。
大前研一がわざわざ「お前らは馬鹿だ」という内容の本を書くわけだ。
fjの教祖様
Re: (スコア:0)
証明とは縁遠い世界の住人がそれだけ多いということなのでしょう。
少なくとも(かように日本語を解してる)日本人の多くが。
いっぽうで、「仕事」が証明と縁遠い世界である場合、
仕事と証明どっちが大事なの？！…という問題も出てくるんだよな。
証明が出来ても仕事(人間が定義するんだよな)が終わらなければ…と。
＃仕事と証明どっちが尊いんだろう？
＃そういや著名な宗教は仕事については言及してるが証明についてはカラッキシだ。
＃たぶん証明という概念は人類史にとってまだまだ新参なのだろう。目鼻がつくには、こなれるのを待つしか無いんじゃない？
Re:基礎論 (スコア:1)
優劣をつける必要がある段階で論外だな。
数学的に証明された事実を仕事に使って一人前だ。
fjの教祖様
Re: (スコア:0)
この部分の飛躍がひどい。 不完全性定理(計算停止問題のアナロジー)はその体系の中で無矛盾性を証明できないというもののであって、それ以外の体系についてはなにも言及していない。ペアノの公理系の無矛盾性はペアノの公理の中では証明不可能だけど、他の体系で証明されてるでしょ。 もうちょっと、謙虚になった方が良いよ。
Re:基礎論 (スコア:1)
Re: (スコア:0)
>> 仕事と証明どっちが尊いんだろう？
> 優劣をつける必要がある段階で論外だな。
> 数学的に証明された事実を仕事に使って一人前だ。
いやいや。#1513170は多分、証明に血道を上げて仕事がお留守になってしまう人特有の雰囲気を感じてしまったのでは無かろうかと。工学はいわば白猫黒猫論に代表される様な現実論の世界であって、猫が白いのか黒いのかの喧喧囂囂もとい侃侃諤諤の議論は理学にお任せしたいですな。
Re: (スコア:0)
okky氏のお客様はokky氏の言う「証明」の意味で「証明せよ」と言っているのでしょうか？ という、コミュニケーション能力の問題な気もします(いや、わざとやってるのはわかってますけどね)。
Re: (スコア:0)
キミたちが、「証明せよ」と言う単語の意味を理解していない、と言うことがよくわかった。
あなたの言う「証明できない」が通用するんなら、計算機科学が相応な時間で解けるとして証明済みの問題も、「証明できない」に入ってしまいますよ。
あぁ、わかった、あなたの言う「証明せよ」は計算機科学での「証明せよ」とは別な意味なんですね（笑）
Re:基礎論 (スコア:1)
思いっきり単純に「バグがなくなったという証明を持ってこいっ」ってのは悪魔の証明だからってんじゃぁだめなのかな？
ここは自由の殿堂だ。床につばを吐こうが猫を海賊呼ばわりしようが自由だ。- A.バートラム・チャンドラー 銀河辺境シリーズより
反例 (スコア:0)
「バグのないプログラムは無い」の反例知ってますよ。
今確認しましたが、VisualStudio2008のC#のプログラムでバグがないものが書けました。
え、どんな仕様なんだ、ですか？
「VS2008でコンパイルできるC#のプログラムを作れ」って仕様ですが、何か？
# 物理学で宇宙の外を語ることはありません
Re:反例 (スコア:1)
お客さんがプログラムを使って、使い終わるまで一回もバグがでないときもあるかもしれませんが、それを前もってなんとか証明できるかどうかです。 もちろん、実際に使って一回もバグが出なかったらそれはそれで結構な話なのですが。 人間だったら前もって知ることができるのでしょうか？
お客さんが欲しいプログラムというのはHello World ではなく、お客さん自身の要求した仕様にあったプログラムなのに、何故かみなさん Hello World の素晴らしさを語っています。
-- 哀れな日本人専用(sorry Japanese only) --
Re:反例 (スコア:1)
典型的で古典的な勘違いですね。
「あなたのマシンが壊れていて、たまたま VS2008でコンパイルが通ってしまっただけである」のではない証明をしてください。壊れたマシンの上で、たまたまエラーが見当たらないからと言って、障害が無いとはいえない、という点は理解できていると思います。
なお、障害には「ビザンチン障害」というのがあって、ありとあらゆるケースで正しい反応を示すが、唯一あなたが本当に正しく動作してほしい場合にだけ、誤った結果を出す、という障害がありえます。ですので、ビザンチン障害が全く無いことを証明しなくてはいけません。
# 詳細は Andrew S. Tanenbaum 先生の本を読んでくれ。
.
「完璧ではないもの(バグがありえるもの)」の上で実行された結果を使っても、証明にはならないのですよ。それは CPU であっても同じです。チューリングマシンはそもそも CPU というハードウェアとその上で動くソフトウェアをワンセットにしてモデル化したものですから。
fjの教祖様
Re: (スコア:0)
君の頭の中ではバグってのはコンパイルエラーのことなのかね。
Re:反例 (スコア:1)
元コメ [srad.jp]で明らかに間違ってそうな点がそこだから、とりあえず指摘したくなるんです。 元コメの親コメ [srad.jp]から 引用して、その誤りを指摘しているように読み取れる部分、
で引用されてる部分は、そもそもあってます。 ついでに、この部分から、元コメの親コメが「わかってない人」かどうかは判断付きません。
で、手っ取り早く、ツッコミがおかしい事を示そうとすると、反例として「そのプログラムにはバグが無いことを示せる」という事例を挙げることになり、Hello Worldになるわけです。
下記の分析後の個人的な印象ですが、「今の時刻は?」「0時59分」「わかってないなぁ、0時59分42.0034秒だよ」みたいな。調べりゃ分かる/知ってても、普通この流れでいきなりそこまで答えないよね、みたいな所にツッコミ入れてるように見えます。
まず、元コメの議論を追うにはちょっと付け加える必要があって、 (1)「ある計算機Xがあった場合に『X用の任意のプログラムにバグがないか判定できるX上で動作するプログラム』は存在しない」 とする必要があります。
「X用の全てのプログラムにバグがないかを判定できる別の計算機Y用のプログラム」は理論上、存在しえます。 ただしここで言う「別の」ってのは「互換性が無い」程度の意味ではなく、根本的に別次元です。ほとんど反則ですが、夢の計算機Yを「X用のプログラムが与えられたときに、それが正しいかどうかを1クロックで判定する命令」を持っている計算機として考えます。 あくまで数学的な考察なのでやりたい放題です。どんな裏技を使っても良いし、あらゆる既知の物理法則を前提にしても良いからちゃんと動作しそうな具体的なYの設計を考えろ、と言われても多分無理なんじゃないかと。
すると、Yを使うと、(1)の問題が解決出来そう・・・と思いきや、Y自身にも(1)の制限は同じように付いてしまい、 (2)『Y用の任意のプログラムにバグがないか判定できるY上で動作するプログラム』は存在しない」と言うことになります。
じゃあ、と、Y用の全プログラムをチェック出来る、夢のまた夢の計算機Zを定義しても、結局(1)はZに対しても成り立つので、(3)『Z用の任意のプログラムにバグがないか判定できるZ上で動作するプログラム』は存在しない」。以下、(4)、(5)、・・・と、どこまで行っても、「あらゆるプログラムのバグを見つけられる存在は存在しない」と言うところに落ち着きます。
んでまあ、実用上、(1)だけ考えていれば困ることはないんです。なにせ、計算機Yの時点で具体的に想像する事すらほぼ不可能、そんな物が目の前に現れるわけがないんですから。世の中で使われてる計算機は全てX互換機と仮定してOK、ぐらいの勢いです(正確にはXの劣化版。量子コンピュータですらこの範疇に含まれる)。
更にツリーを遡ると元コメの親コメの親コメ [srad.jp]は、「バグ無しを証明しろと言われて困る」だったので、上記を当てはめると「証明しろ」「計算機Xでは不可能です」「いいや、計算機Yがあれば出来るだろう」「計算機Yが正しいかどうか・・・」「計算機Zを使え!!」という、相当マニアックな顧客と言うことになりますね。 普通は「いやいや、計算機Yなんて実装できませんし」となるかと。
ついでに、元コメのどこが意地悪かというと、
この辺も、非常にミスリードです。「プログラム」=「計算機の定義(設計)+その上で動作するプログラム」と言う 意味で書かれていて、このp1、p2が、上記Y、Zに相当するわけです。バグ取りの実務でよもや計算機Yが話題に上るとは想像出来ず、「プログラムp0、p1、p2、・・・」を「計算機X上で動くプログラムp0、p1、p2」をとして読み進めてしまい、釣られてしまったわけです。
元コメは、分かってない人用の説明っぽく書きだしておいて、その実、ちゃんと分かってる人でないと、 言わんとすることが分からない説明ですね。
# 以上、自分がこのジャンルに自信がないので、間違った理解をしていないかチェックの流れ。
# 「良くある間違いはコレだ!」と、表題が付いてるのはチェックに最適なもので。
Re:反例 (スコア:1)
ここでの話題って、#1512749から分岐して誘導されていると思うんですよ
で、装置の移動の方なんですが、よくある実務領域に限定すれば、バグ判定としては、仕様に基づいた限定的なテストに合格するかどうかだけです。
残りのバグは人間仕様からテストケースを起こす段階になるので、判定装置は機械から人間に移動するんですよね。
プログラムを解析しての判定は難しいので、バグ判定装置を人間レイヤーに移動させたうえで問題を単純化し、特殊事例としての「バグのないプログラム」問題に変化させて解決しようとしている。←ここでチェーンを終了させてようとしている、というか次のチェーンがないので仕方がないんですけど。
「計算機Zを使え!!」は現場では「次の計算機はSEだ」で、「次の計算機は顧客だ」になるようにしている。
それでバグがないことを（常に）証明できるか？というとそうではなくて、証明できるケースもあるだろうし、できないケースもある。人間が納得できるレベルまで不完全性を縮小できればいい、ということまでしか言うつもりはないんですけど。
そういう矮小化された議論が成り立たないような問題を解く領域では、バグがないことを保証することはできないような逆の意味のHello Worldを出すことも可能ではあるわけですが。
私の認識では、「人間が解決済みの課題を処理させるためのプログラム」なら、判定装置を人間側に誘導することが可能で、「人間が解決していない課題をプログラムに代わって解かせるためのプログラム」については判定装置の移動で問題を先延ばしにしても収束しない、と思っています。
Re:反例 (スコア:1)
これ [srad.jp]の
は、やっぱり、チューリングマシンの停止問題とは違う一般論ですね。前後の文脈から、停止問題そのものを扱った話題かと勘違いし、関連を見いだそうとして混乱していました。
この場合はp0の作り方の問題で、p0を上手いこと作っておけば、『p0の出力』を見て数学的に納得出来れば『xは正しい』と出来ますね。 ご指摘のp0の正しさをあらかじめ頑張って確かめておく、という手順とは言わば逆のやり方になるわけですが。
要するに『p0は信用出来るのか?』という疑問は、p0が『xは正しい』『xは間違っている』としか出力してくれない場合にだけ起こります。p0が、『xは、(1)再帰を含めて全てのループは有限回で止まる。なぜならループ変数iは・・・・(以下xの中身を引用した数学的証明)、(2)答えは仕様通りになる。なぜなら(同様に証明)。よってxは正しい』と、出力してくれれば、p0の信頼性は気にしなくても大丈夫です。その出力をSEなり顧客なりが読んで、筋が通ってるかどうかだけ気にすれば良いんで、p1、p2、・・・の出てくる余地はありません。
ちなみに、この場合のp0は「ある特定の構造をしたプログラムのみ解析出来る」とかそんな物になります。 その構造をしてないxを与えた場合には「このプログラムは分からない」とでも出力します。 似たようなのは売ってます。ただ、出力される「証明」が非人間的な記述方法と量になるので、 その「証明」を読み解くことは事実上不可能ですが。 よって、おおむね、「p0は正しい」というのを信じるしか無いわけです。
こういう方法で、1ターンで事を「プログラムの正さの証明」から「数学的に記述された証明」に落とせるので、私としては「筋が通ってても、『数学が正しい』という保証がないから無駄」と言う意味かと最初に誤解しました。 私がコメントを付けた最初のコメントは、「正しい/間違ってる、としか出力しないプログラムだと、どうやってオーソライズする? 読み解けないほど長い証明を出しても無意味」という主張だったんですね。停止問題を理解してるかどうかとは無関係な議題ですね。
Re:反例 (スコア:1)
間違い。
p0 がxについての評価結果を出したとしよう。
その評価結果が正しいということを「どうやって証明するのだね?」
いいかい?ここでいう「証明」というのは意外と厄介な存在だ。たとえば、
という記述があるとする。これゆえにp0は「無限ループになっています」と出力したとしよう。キミも私もそれに同意したとする。それでは証明とはいえない。p0とキミと私がバグっているだけかもしれないではないか。
ちょっと世界中の技術者と計算機科学者全員に問い合わせてみる。全員 p0 の出力に同意したとする。それでは証明とはいえない。
K&R に「while(1); と書いたら無限ループになります」と書いてあったとしよう。それでも証明とはいえない。
有限の帰納的蓄積は証明とは言わない。機能的蓄積が使いたければ、帰納法を使って無限を扱わなくてはいけない。
fjの教祖様
Re:反例 (スコア:1)
1. 繰り返し1回目は、条件式の値が1であるのでこのループからは抜けない
2. 繰り返しn回目を迎えた場合、条件式の値が1であるのでこのループからは抜けず、繰り返しn+1回目へと遷移する
3. 1,2より、このループは終わらない
とか。もうちょっと数学的に厳密な表記が要るはずですが。
これを証明として認めるかどうかの議論になると、「証明として認められるかどうかは拠り所にしている数学体系によって異なる」という漠然としたイメージでしたが、間違ってますか?
「適当な拠り所で上記証明は証明として認められる」、ならそれで十分かと思ってました。 なにせ「拠り所など関係なく究極的にはどうか?」と言い出すと、 不完全性定理から「そもそも究極の数学体系は存在しないので、究極の証明もありえない」で、 議論の余地無しで解決、余地のない議論をわざわざしてみるのも徒労ですし。
Re:反例 (スコア:1)
これを証明として認めるかどうかの議論になると、「証明として認められるかどうかは拠り所にしている数学体系によって異なる」という漠然としたイメージでしたが、間違ってますか?
それを漠然としたイメージって言ってしまうと、もともこもないんでは？
無限ループとは何かを、公理から導いて定義したうえで（じゃないと命題にならんので）、その定義から発して論理的に矛盾なく説明されていれば「証明された」とみていいはずです。
いや、それでも、その証明が正しいことをどうやって証明する？なんて言ってしまって、それが通用するんであれば、土俵が違うってだけになると思います。
その証明を否定するには、「それをどうやって証明する？」っていう幼稚な反復じゃなくて、「その証明が正しいとすると、矛盾が生じる」っていう反証が必要だと思うんですよ。
Re: (スコア:0)
プログラムが誤りがあるかどうかの判定は 1 に属する問題で「不可能」とすでに証明されている。
え、そうなんですか？
もしプログラムに誤りがあることを何によっても証明できない状況だとすると、チューリングの証明も成立しないですよね。
Re: (スコア:0)
証明・証明って言ってる割に、対角線論法で証明できると"断定"しちゃった理由も知りたいところです。
Chain of Trust に逃げるんなら対角線論法は必要ないですよね。
バグのないプログラムは２つあるよ (スコア:2)
その２：何の機能もないプログラム
Re:バグのないプログラムは２つあるよ (スコア:2)
-- 哀れな日本人専用(sorry Japanese only) --
モデル検査 (スコア:2)
バグが無いという保証されることはありえないっていうのと停止問題は違う話なんじゃないでしょうか。
例えば、形式的検証(formal verification) [wikipedia.org]やその一例であるモデル検査(Model Checking) [wikipedia.org]という手法を使って数学的な正確さでバグ無しであると証明する試みはなされています。AT&T の電話交換機のバグを発見したという逸話もあるので通常デバッグしづらい並行性システムの検証などある程度実用化されてきてるみたいです。
Re: (スコア:0, 荒らし)
バグとはどういうものか、バグの発見方法とは、などをちゃんとわかりやすく説明していないからでしょ。
「説明」とか「プレゼン」ができないコンピュータ技術者の多いこと多いこと・・・
コンピュータ技術者は院卒じゃないとろくにプレゼンもできないから困る。
Re: (スコア:0)
そう言って、見つかったバグすら直すのを拒否するわけですね。
うんうん、今度使ってみよっと。
Re: (スコア:0)
＞# 「バグがなくなったという証明を持ってこいっ」
わかりました、将軍様。それでは、バグのない仕様書を提出してください。
# ココとソコの行間に時間軸のずれがあるのに気づけない将軍様の多いことといったら…
Re: (スコア:0)
そうそう。
仕様書にバグがないことを証明できれば、プログラムにバグがないことも証明できる。