- 締切済み
プログラムの形式的証明は本当に使い物になるのでしょうか？
近年プログラミングの世界でも VDM(http://en.wikipedia.org/wiki/Vienna_Development_Method) に代表さ れる形式的証明がもてはやされ始めました。 でも私には、プログラムの形式 的証明は、うさんくさいものに思えてなりません。 形式的証明が絶対に不可能だとは思っていません。Goedel の不完全性定理や、 Turing マシンの停止判定問題などから解るように、万能の証明方法を探すの は無駄です。でも、これらの証明不能性は問題の範囲をメタな対象まで含め てしまうことから発生しています。形式的証明の対象範囲を旨く限定してや ればプログラムが仕様どうりに動くことを形式的に証明できることはありう るだろうと思います。 でも一般的に証明問題は難しすぎます。プログラム動作の形式的証明が旨く 機能できる範囲など極端に限られると私の直感は主張しています。 現在でも、プロの数学者が定理や公理を構築する作業は、自分の頭の中での 論理展開をノートに書き残す方法で行っているでしょう。 Coq(http://coq.inria.fr/) なども出てきましたが、このようなソフトを使 っているのは、自動証明の研究者などに限られるでしょう。しばらくは(たぶ ん 100 年以上は)プロ数学者の研究・証明のために行う論理展開作業をコン ピュータが代行することはないと思います。 現実のコンピュータ・プログラムが対象としているのは、数学の世界のよう な綺麗なものではありません。人間が定める膨大かつ不明瞭な仕様書の塊は、 形式的証明の対象にできるとは思えません。たとえできたとしても純粋数学 より難しいはずです。 限られた特殊な領域では、現実のプログラムを形式的証明で扱えるかもしれ ません。でも、そんな形式的証明を理解でき人間は限られるでしょう。大多 数のプログラマーには理解されないでしょう。形式的証明自身に誤りが入り 込んでいないかを検証することは不可能に近い作業になると思います。 私には現実のプログラムが仕様書どうりに動くことを形式に証明することは、 まだ実務的には無意味な作業としか思えません。皆様の御意見を伺わせても らえますでしょうか
- loboskobay
- お礼率52% (12/23)
- 数学・算数
- 回答数4
- ありがとう数14
- みんなの回答 （4）
- 専門家の回答
みんなの回答
- sawara__
- ベストアンサー率0% (0/0)
形式的検証には モデル検証 定理証明による検証 がありますが、回答を見ていると上記２つの混同がある様に 思います。 定理による検証は 林晋先生のプログラム検証論 共立出版 1995 を参考に。 冒頭の 1.2章あたりを読めば雰囲気は十分に解ります。 回路検証用のフォーマルtoolは主にモデル検証を応用した物です。 RTLより抽象モデルを抽出して、このモデルが取り得る全ての 状態を生成する。モデルの性質を時相論理で記述する。これをタブロー法に基づいたアルゴリズムでオートマトンに変換し、先に生成した 状態をチェックする。 RTLより抽象度の高いシミュレーションと いう感じでしょうか。全状態をチェックできるので証明になります。 フォーマルtoolはRTLから抽象モデルの抽出を行ってくれる。 性質をアサーション形式で書ける機能を備える。全状態を生成するのでパターンは不要、さらにアサーション形式で性質を記述できるため、アサーション技術と混同しやすい。 アサーション技術は波形の目視検証時の誤認と目視工数の削減を 目的とした技術で形式的検証とは直接の関係は無い。 波形はアサーションにより自動チェックできるので、通常検証に必要な 入力パターンに対応する出力パターンの対応が不要となる。 このため入力パターンは生成した乱数で振り回路へ入れるだけ。。楽ちん。 →EDAメーカの難しい技術を強調したセールストークも混同一因と思います。 >>証明は絶対正しいことを複数の前提条件：公理から論理的導くことで>>す。絶対に正しいことを導くことです。 使用する言語の形式的意味も前提条件でしょ。 ”コンパイラバグで正しく動作しなかった” でも正しい事の証明は出来ています。 →コンパイラバグで不具合を起こして左遷された、 の経験が無ければ役にたつ実感が得られると思うのですが。
- rabbit_cat
- ベストアンサー率40% (829/2062)
もう一度だけ書きますと、 SystemVerilogの形式的検証は、loboskobayさんの仰る「証明」そのものですよ。 ＞そこでの検証は具体的なテスト・パターン： ＞可能な入力シーケンスと予定出力シーケンスの組み合わせテストの繰り返しです。 ＞ですからVMM では論理学を使った証明はされていないと思います。 違います。SystemVeilogの形式的検証では、「具体的なテスト・パターン」は全く使いません。（したがってテストベンチを作成する必要もありません） 「前件⇒後件」という形でAssertionを書いておくと、形式的検証ツールが、「前件かつnot(後件)」となるような入力パタンが存在しないことを、形式的に（論理学的な手法を使って）「証明」してくれます。逆に言えば、形式的検証をパスしたなら、全ての入力パタンについて、Assertionが満たされる、ということが保証されます。 それから、VMMと形式的検証は全く別の話です。 ＶＭＭは、形式的検証ではなくて、基本的には従来型のテストベンチを書いて具体的なテストパタンと予定出力パタンとの比較する、というテスト方法を念頭において作られたもので、 仰るとおり、検証系の書き方の標準化や再利用性向上を目的としています。
- rabbit_cat
- ベストアンサー率40% (829/2062)
SystemVerilogの形式的検証は、テストベンチやテストパタンは使いません。 moduleなどの要素ブロック毎に、入力が満たすべき前件条件と、出力が満たすべき後件条件を表明（Assertion）しておくと、形式的検証ツールが、入力が前件を満たすならば出力は必ず後件を満たすということを、論理学的な手法で検証（証明）してくれます。 また、たいていのツールは、もし入力が前件を満たしているに関わらず出力が後件を満たさない場合があれば、そういう入力パタンを例示する機能もあります。 形式的検証を本当に実務で使うようになったのは、Assertionの言語仕様がSystemVerilog等の中できちんと標準化されたここ数年のことだとは思いますが、現在は、大規模ＬＳＩの開発では、まあまま一般的な手法だと思いますよ。 もちろん、形式的検証ツールは、あくまで、明示的に表明されているAssertionが必ず満たされるということを証明するだけですので、Assetion自体に抜けや間違いがあればバグがある可能性はあるわけですが。
- rabbit_cat
- ベストアンサー率40% (829/2062)
少なくとも、ＬＳＩの論理の設計では、形式的証明の手法が、すでに実際の実務でかなり広く行われています。 「SystemVerilog 形式的検証」とかで検索すると、実例やツールなどが見つかると思います。 ＰＣ上のプログラムであれば、バグが見つかっても直せばいいですが、 ＬＳＩの論理設計（ようはＬＳＩ内部の論理のプログラミング）でバグがあってＬＳＩの作り直しなると、それだけで１０億単位のお金がかかります。 ＬＳＩに限らず、バグが非常に高くつくようなモノの設計では、多少お金をかけても「絶対にバグがない」ことを証明できる手段が必要とされると思います。
お礼
rabbit cat さん、御指摘ありがとうございます。でも逆に LSI での事情か らも、プログラムの形式的証明はありえないだろうと思っています。 >ＬＳＩの論理の設計では、形式的証明の手法が、すでに実際の実務でかなり広く行われています これは形式的「証明」ではなく、形式的「検証」だと思います。 SystemVerilog VMM は Verification Methdology Manual for SystemVerilog の略です。そして VMM での検証は再利用が中心に考えられて いると思います。Verilog のときは test bench も verilog でハード記述と 一緒に書いていましたが SytemVerilog ではテストは独立させて記述してい ると思います。そこでの検証は具体的なテスト・パターン：可能な入力シー ケンスと予定出力シーケンスの組み合わせテストの繰り返しです。ですから VMM では論理学を使った証明はされていないと思います。 一方で、ご指摘のように、LSI 設計ではバグは、プログラミングの世界より 大きな損失が発生しやすいため、昔から検証はしっかりなされてきました。 プログラミングの世界よりも進んでいます。その LSI の検証でさえ、論理学 なぞ使っていないのに、それよりも難しいプログラミングの世界で、論理学 を使った形式的証明が先に実用化されるなんてありえないはずだと思ってい ます。 実際問題として 8080 からの歴史を未だに引きずっている Pentium のような 複雑怪奇なプロセッサで論理学を使った形式的証明が本当に可能だと思いま すか？ またどんなプロセッサであっても、常に幾つものエラータリストを抱 えているものでしょう。 私はプログラミングの世界でも LSI の世界と同様に「可能な入力シーケンス と予定出力シーケンスの組み合わせテスト」を積み重ねることがプログラム の正しさを保障すると思っています。 なお私自身は Verilog の経験はありますが SystemVerilog までは実際には 使っていません。もし私の認識に誤りがあったら指摘してやってください。
関連するQ&A
- ゲーデルの証明不能命題
不完全性定理（形式的体系においてその公理と推論規則を使って証明も否定もできない論理式Ａが存在する。）にいう論理式Ａには例えばどんなものがあるのでしょうか？ いまだ解かれていない数学上の難問がありますが、これらが論理式Ａであるかどうかは、結局のところ証明できた時点でしか判定できないのでしょうか。
- ベストアンサー
- 数学・算数
- 数学でいう「証明」と論理学でいう「証明」は異なるものでしょうか？
数学で使われる「証明」という言葉と論理学で使われる「証明」という言葉は意味が異なるものであると思うのですが，間違いでしょうか？ 公理系で挙げられる代表的な恒真式と推論規則に基づいて，別の恒真式を導くことが論理学でいう「証明」ですよね？ そして論理学的な「証明」によって得られるものは恒真式（定理）だと思います．恒真式とは情報の価値としてはゼロ（自明）です． これに対して，数学で「証明」されるものは恒真式ではないですよね？数学における「証明」とは論理学における「演繹」に相当すると思うのですが，この考えも間違いでしょうか？ ご教授お願いします．
- 締切済み
- 数学・算数
- 数学でいう「証明」と論理学でいう「証明」は異なるもの？
数学で使われる「証明」という言葉と論理学で使われる「証明」という言葉は意味が異なるものであると思うのですが，間違いでしょうか？ 公理系で挙げられる代表的な恒真式と推論規則に基づいて，別の恒真式を導くことが論理学でいう「証明」ですよね？ そして論理学的な「証明」によって得られるものは恒真式（定理）だと思います．恒真式とは情報の価値としてはゼロ（自明）です． これに対して，数学で「証明」されるものは恒真式ではないですよね？数学における「証明」とは論理学における「演繹」に相当すると思うのですが，この考えも間違いでしょうか？ ご教授お願いします．
- 締切済み
- 哲学・倫理・宗教学
- 「数学が好き」という人は、どうして好きなのですか
「数学が好き」という人がいるそうですが、どうして好きなのでしょうか。 本当に数学自体がおもしろいと思っているのでしょうか。 それとも、「数学が好き」と人に言うとかっこよく聞こえるから、そう言っているだけなのでしょうか。 よく、「数学の問題は、論理的に考えれば必ず解けるから好きだ。」とか、 「定理が証明できると、美しさに感動する。」とか言う人がいるようですが、 私は、解が論理的に出てきても、定理が証明できても、「それがどうしたの？」と思うだけですが、どうしてそんなことをおもしろがる人がいるのですか？
- ベストアンサー
- 数学・算数
- 形式化の表す内容について
再質問になります。 以前、言葉尻の異なる同じような内容の質問をしております。ご容赦ください。 スコーレムの定理によりべき集合公理をもつ公理系にも可算モデルが存在する 無限体k上のベクトル空間の次元という概念は論理式では表現できない ペアノ算術において自然数の非標準モデルが存在する といったものから モデル側の性質をすべて形式体系で書くことはできないということが結論されているのを見るのですが、自分としてはそのような形式体系で書くことができない性質があるということ、その性質について考えるとことが、なぜ記号を対象とした数学という分野でできるのかということが不思議なのです。 つまり（あくまで建前上ではですが）、イメージや心象を閉め出して形式的な文字列の変形、生成で議論できるはずの数学においては形式体系、公理系のモデルも結局何らかの形式的な文字列の変形、生成で定義される以外無いはずであって（モデルを決めるというのは形式体系側の記号や述語に、新しい記号や述語を対応させた新しい形式体系を実装として定めるということだと考えています） 例えば 実数の公理系の非可算のモデルの更なる可算モデルを考えると、そもそも非可算モデルとはなんだったのだろうか（何をもって非可算といっていたのだろうか もちろん元の体系内で、ある集合が可算無限の集合と１：１対応のつけられないということが証明できるということをもってなのでしょうが、しかしそれも体系の外に出てみると可算モデルになっていることがあるということならどこまで行っても本当に非可算かどうかを確かめることはできないのではないだろうか つまり何をもって非可算となすという基準が作れないように見え、それならば非可算というもの自体がどういうものかわからないのではないか なら最初の非可算モデルとはいったい何だったんだろうといったように） ベクトルの次元という概念も表現できる視点があって初めて、ある論理上では表現できないということが分かるのであってその表現できる視点というのも論理式の集合で書かれるしかないのではないか ならば次元という概念も論理式の集合で表現できることになるのでは 標準的な(N,0,1,＋,・,＜)のＮも数学で考えるために論理式で定義されるものなら標準モデルだけを表す公理系があるのではないだろうか もしないならどうやって数学の議論の台に乗せるのだろうか などといった、おそらく擬似問題に悩んでしまうのです。 認識といってしまうといきなり怪しい話になってしまい恐縮ですが、「モデル側の性質をすべて形式体系で書くことはできない」ということは一見して数学の論理は、人間の心象、意味内容を全て認識することができないと受け取ってしまいそうになりますが、形式とモデルの関係はそのようなことをいっているのではなく、数学上の話である以上、体系間の関係のことをいっていると思うのですが正確にはどういうことを表しているのかわからないのです。 おおざっぱにいうと論理式で表せない性質があるということをいうためにはその性質を表すことが必要であり、数学においてはそれも論理式で書くことになると思うので、結局どういうことをしているのか混乱しているのです。 それとも最初に書いたようなことは人間側の推論と論理式での推論の関係（これは本当にイメージ心象と論理式の関係であって、想像上の集合、モデルと形式体系は１：１には対応しない）を、体系同士の関係で表した、まねさせたことから出てきた成果なので たとえば非可算かどうかを確認する絶対的基準なものがどこにあるかなどと言うことは意味をなさないのでしょうか。つまり実装（モデル）側で、ある論理式（可算性、非可算性に相当する）を証明できるものを可算モデル、非可算モデルという名前を付けているだけであって人間の使う非可算という意味とは（建前上は）関係がないということでしょうか。 もちろん例えば、自然数といわれればその意味するところはわかりますし、その自然数と同型でないモデルというのも色々なところで図などをつかって解説されている限り同型でないということや、どういうものかということは分かります、ただそれは明らかにイメージに頼ったものであって、厳密な意味での数学ではどうするのだろう（というか論旨式で表せないものを表すとは何だろう）と考え質問いたしました。 メタレベルと対象レベルを区別できてないが故の疑問だと感じているのですが、モデル（実装）にたいしても、その実装は？さらにその実装は？といっていくと結局非可算かどうかを区別できる視点などないのではないかということにならないのでしょうか？ かなり初歩的な勘違いをしていると思いますが、この方面に明るい方、過去このような疑問を持たれた方、お時間ありましたら解答、解説お願いします
- ベストアンサー
- 数学・算数
- ユークリッド幾何学にまつわる不完全性定理的理解について
ユークリッド幾何学にまつわる不完全性定理的理解について ゲーデルの不完全性定理の対象となる数学は『公理系Ｎが無矛盾である』が前提です。ユークリッド幾何学は 一階述語論理で表されることが出来る自然数の部分集合であって、ゲーデルの不完全性定理の対象である 公理Ｎの無矛盾である 論理の対象になってないとなり それ以上のユークリッド幾何学の論理的理解が進みません。そこでゲーデル理解を拡張して『公理系Ｎが無矛盾ではない』として不完全性定理を理解すると（須田隆良氏、中西章氏など） (1)ゲーデルの第一不完全性定理の解釈＝＝＞公理系Ｎが無矛盾であろうがなかろうが 公理系Ｎにおいて、「公理系Ｎにおいて命題は証明可能である。」という命題も、「公理系Ｎにおいて命題は証明不可能である。」という命題も証明不可能である (2)第２不完全性定理の解釈＝＝＞公理系Ｎが無矛盾であろうがなかろうが その無矛盾性を証明できない となります。これらはゲーデル不完全性対象から外れておりますが、対象外のユークリッド幾何学を理解するには都合がよい と思うのです。 (2)によりユークリッド幾何学の公理の無矛盾性は証明できない。 (1)によりユークリッド幾何学の未定義領域（非ユークリッド幾何学、虚数、無限遠点とか）は 公理系Ｎにふくまれ 多くの証明できない命題があることになります。もちろん 公理定義内では完全性理論は保証されています。 なぜ このようなユークリッド幾何学に こだわる かと申しますと 世の中の 論理（数学、哲学、論理を用いた論文 など）は ユークリッド幾何学的なものが 圧倒的に多いと思うのです。これら論文は ほとんどは一階述語理論で表され かつ ゲーデル不完全性定理 対象論理ではないのです。それら論文の特に(2)に関わる自己証明は出来ない ということは重要であると思うのです。もちろん 自己証明が出来ないと言って間違いとはなりません が 常に 冷静に謙虚に 主張理論の原点を見直すことに 繋がっていると思うのです。勿論、論理構成が出来ていないシロモノは 論外であります。 以上のように理解しているのですが、ユークリッド幾何学にまつわるゲーデル不完全性定理の場外理解は問題ないでしょうか。諸先生のコメント頂けましたら幸甚です。
- ベストアンサー
- 数学・算数
- 不完全性定理から証明された「真理性 Ω は、ランダムである」とはどういうことですか？
ゲーデルの不完全性定理の応用でチャイティンが、 「任意のシステム Ｓ において、そのランダム性を証明不可能なランダム数Ｇ が存在する」 という事を証明し、その後「真理性 Ω は、ランダムである。」という定理を発表したようですが、 この「真理性 Ω は、ランダムである。」とはどういう意味なのですか？ 論理学も数学もほとんど無知ですが感覚的に分かるように説明して頂けませんか。よろしくお願いします。
- ベストアンサー
- 数学・算数
- ３角不等式の証明。
３角不等式の証明。 ３角形の２つの角が等しくないとき、大きい角に対する辺は小さい角に対する辺より大きいことの証明を背理法で中学生を対象に授業形式で20分程度で発表しなければなりません。 みなさんだったらどのような授業の構成・展開をしていきますか。 中学２～３年生相手にでも理解できるようわかりやすくお願いします。 とりあえず背理法で証明を作ってみましたが、とても２０分は持ちません。 【証明】 △ABCにおいえて、∠B＞∠Cならば、´AC＞ABを証明する。 （１）AC＝ABと仮定すると以前示した定理より、二辺が等しいならば、△ABCは二等辺三角形であるから∠B＝∠C （２）AC<ABと仮定すると、以前示した定理より、三角形の二つの辺が等しくないとき、大きい辺に対する角は小さい辺に対する角より大きいため∠B＜∠C いずれにしても仮定∠B＞∠Cに反するから、AC＞ABでなければなりたたない。 この証明を膨らませるには２０分程度に膨らませるにはどうしたらいいでしょうか。 大至急お願いします!
- 締切済み
- 数学・算数
- 「科学的証明」の一般的定義について
一般に「科学的証明」と言う場合、数学や論理学などの形式科学における証明と、自然科学における証明とがあり、前者を一般に「論証」と言いおもに演繹法により、後者を一般に「実証」と言い実験や観測のデータにもとづく帰納法による・・・と、大雑把にはこういう理解でよいですか？ それで一般に科学的証明と言う場合、どちらかというと後者の意味で、つまり実証という意味で言われることが多いように思われますがいかがですか？ あと、形式的証明と非形式的証明の違いについて出来るだけわかりやすく教えて下さい。
- ベストアンサー
- 科学
お礼
返答が遅れて失礼しました。ここ「SystemVerilogアサーション効率的な検証 を実現する設計と検証の統合言語 http://www.synopsys.co.jp/products/technology/sva/index.html」を読ん でいました。 >形式的検証を本当に実務で使うようになったのは、Assertionの言語仕様が SystemVerilog等の中できちんと標準化されたここ数年のことだとは思います が、現在は、大規模ＬＳＩの開発では、まあまま一般的な手法だと思います よ。 VEGA の仕様書までは読んでいたのですが、それ以後 Hardware Discription Language からは遠ざかっていました。 >形式的検証を本当に実務で使うようになったのは、Assertionの言語仕様が >SystemVerilog等の中できちんと標準化されたここ数年のことだとは思います >が、現在は、大規模ＬＳＩの開発では、まあまま一般的な手法だと思います >よ。 あくまでも形式的「検証」だと思います。Assertion の積み重ねだと思いま す。if 事前条件 then 事後条件という制約は assert not(事前条件) or 事 後条件と等価です。VMM での concurrent assertion は、単純な論理変換以 上のものだとも思います。頭の良いやつも いる物だとは思います。 証明は絶対正しいことを複数の前提条件：公理から論理的導くことです。絶 対に正しいことを導くことです。一方で、検証は、個別の具体例について誤 っていないことを確認することです。証明と検証では、正しさの程度が質的 に異なります。そして現実の LSI の設計コードやプログラミングで行えるこ とは検証だと思います。 でも VDM では論理推論まで踏み込み、形式的「検証」を超えて、形式的「証 明」を主張します。私は、そんなことは実務で使えるはずがないと考えます。 LSI のような、すぐにお金に跳ね返る世界でも使われようともしていない VDM の形式的「証明」はうさんくさいものだと思っています。 rabbit_cat さんの補足により、上の自分の判断に少しばかり自信を持てるよ うになりました。ありがとうございました。