プログラムの形式的証明は本当に使い物になるのでしょうか？

近年プログラミングの世界でも
VDM(http://en.wikipedia.org/wiki/Vienna_Development_ … に代表さ
れる形式的証明がもてはやされ始めました。 でも私には、プログラムの形式
的証明は、うさんくさいものに思えてなりません。

形式的証明が絶対に不可能だとは思っていません。Goedel の不完全性定理や、
Turing マシンの停止判定問題などから解るように、万能の証明方法を探すの
は無駄です。でも、これらの証明不能性は問題の範囲をメタな対象まで含め
てしまうことから発生しています。形式的証明の対象範囲を旨く限定してや
ればプログラムが仕様どうりに動くことを形式的に証明できることはありう
るだろうと思います。

でも一般的に証明問題は難しすぎます。プログラム動作の形式的証明が旨く
機能できる範囲など極端に限られると私の直感は主張しています。

現在でも、プロの数学者が定理や公理を構築する作業は、自分の頭の中での
論理展開をノートに書き残す方法で行っているでしょう。
Coq(http://coq.inria.fr/) なども出てきましたが、このようなソフトを使
っているのは、自動証明の研究者などに限られるでしょう。しばらくは(たぶ
ん 100 年以上は)プロ数学者の研究・証明のために行う論理展開作業をコン
ピュータが代行することはないと思います。

現実のコンピュータ・プログラムが対象としているのは、数学の世界のよう
な綺麗なものではありません。人間が定める膨大かつ不明瞭な仕様書の塊は、
形式的証明の対象にできるとは思えません。たとえできたとしても純粋数学
より難しいはずです。

限られた特殊な領域では、現実のプログラムを形式的証明で扱えるかもしれ
ません。でも、そんな形式的証明を理解でき人間は限られるでしょう。大多
数のプログラマーには理解されないでしょう。形式的証明自身に誤りが入り
込んでいないかを検証することは不可能に近い作業になると思います。


私には現実のプログラムが仕様書どうりに動くことを形式に証明することは、
まだ実務的には無意味な作業としか思えません。皆様の御意見を伺わせても
らえますでしょうか

No.4 回答者： sawara__ 回答日時： 2009/05/08 16:52

形式的検証には

　モデル検証
　定理証明による検証
がありますが、回答を見ていると上記２つの混同がある様に
思います。

定理による検証は
　　林晋先生のプログラム検証論　共立出版 1995
を参考に。　冒頭の 1.2章あたりを読めば雰囲気は十分に解ります。

回路検証用のフォーマルtoolは主にモデル検証を応用した物です。

RTLより抽象モデルを抽出して、このモデルが取り得る全ての
状態を生成する。モデルの性質を時相論理で記述する。これをタブロー法に基づいたアルゴリズムでオートマトンに変換し、先に生成した
状態をチェックする。　RTLより抽象度の高いシミュレーションと
いう感じでしょうか。全状態をチェックできるので証明になります。
　フォーマルtoolはRTLから抽象モデルの抽出を行ってくれる。
性質をアサーション形式で書ける機能を備える。全状態を生成するのでパターンは不要、さらにアサーション形式で性質を記述できるため、アサーション技術と混同しやすい。

アサーション技術は波形の目視検証時の誤認と目視工数の削減を
目的とした技術で形式的検証とは直接の関係は無い。
波形はアサーションにより自動チェックできるので、通常検証に必要な
入力パターンに対応する出力パターンの対応が不要となる。
このため入力パターンは生成した乱数で振り回路へ入れるだけ。。楽ちん。

　→EDAメーカの難しい技術を強調したセールストークも混同一因と思います。

>>証明は絶対正しいことを複数の前提条件：公理から論理的導くことで>>す。絶対に正しいことを導くことです。
使用する言語の形式的意味も前提条件でしょ。
　”コンパイラバグで正しく動作しなかった”
　でも正しい事の証明は出来ています。
　　　→コンパイラバグで不具合を起こして左遷された、
　　　　の経験が無ければ役にたつ実感が得られると思うのですが。

No.3 回答者： rabbit_cat 回答日時： 2008/08/04 03:18

もう一度だけ書きますと、

SystemVerilogの形式的検証は、loboskobayさんの仰る「証明」そのものですよ。
＞そこでの検証は具体的なテスト・パターン：
＞可能な入力シーケンスと予定出力シーケンスの組み合わせテストの繰り返しです。
＞ですからVMM では論理学を使った証明はされていないと思います。
違います。SystemVeilogの形式的検証では、「具体的なテスト・パターン」は全く使いません。（したがってテストベンチを作成する必要もありません）
「前件⇒後件」という形でAssertionを書いておくと、形式的検証ツールが、「前件かつnot(後件)」となるような入力パタンが存在しないことを、形式的に（論理学的な手法を使って）「証明」してくれます。逆に言えば、形式的検証をパスしたなら、全ての入力パタンについて、Assertionが満たされる、ということが保証されます。

それから、VMMと形式的検証は全く別の話です。
ＶＭＭは、形式的検証ではなくて、基本的には従来型のテストベンチを書いて具体的なテストパタンと予定出力パタンとの比較する、というテスト方法を念頭において作られたもので、
仰るとおり、検証系の書き方の標準化や再利用性向上を目的としています。

No.2 回答者： rabbit_cat 回答日時： 2008/07/17 22:47

SystemVerilogの形式的検証は、テストベンチやテストパタンは使いません。

moduleなどの要素ブロック毎に、入力が満たすべき前件条件と、出力が満たすべき後件条件を表明（Assertion）しておくと、形式的検証ツールが、入力が前件を満たすならば出力は必ず後件を満たすということを、論理学的な手法で検証（証明）してくれます。
また、たいていのツールは、もし入力が前件を満たしているに関わらず出力が後件を満たさない場合があれば、そういう入力パタンを例示する機能もあります。

形式的検証を本当に実務で使うようになったのは、Assertionの言語仕様がSystemVerilog等の中できちんと標準化されたここ数年のことだとは思いますが、現在は、大規模ＬＳＩの開発では、まあまま一般的な手法だと思いますよ。
もちろん、形式的検証ツールは、あくまで、明示的に表明されているAssertionが必ず満たされるということを証明するだけですので、Assetion自体に抜けや間違いがあればバグがある可能性はあるわけですが。

この回答へのお礼

返答が遅れて失礼しました。ここ「SystemVerilogアサーション効率的な検証
を実現する設計と検証の統合言語
http://www.synopsys.co.jp/products/technology/sv …」を読ん
でいました。

>形式的検証を本当に実務で使うようになったのは、Assertionの言語仕様が
SystemVerilog等の中できちんと標準化されたここ数年のことだとは思います
が、現在は、大規模ＬＳＩの開発では、まあまま一般的な手法だと思います
よ。

VEGA の仕様書までは読んでいたのですが、それ以後 Hardware
Discription Language からは遠ざかっていました。


>形式的検証を本当に実務で使うようになったのは、Assertionの言語仕様が
>SystemVerilog等の中できちんと標準化されたここ数年のことだとは思います
>が、現在は、大規模ＬＳＩの開発では、まあまま一般的な手法だと思います
>よ。

あくまでも形式的「検証」だと思います。Assertion の積み重ねだと思いま
す。if 事前条件 then 事後条件という制約は assert not(事前条件) or 事
後条件と等価です。VMM での concurrent assertion は、単純な論理変換以
上のものだとも思います。頭の良いやつも いる物だとは思います。

証明は絶対正しいことを複数の前提条件：公理から論理的導くことです。絶
対に正しいことを導くことです。一方で、検証は、個別の具体例について誤
っていないことを確認することです。証明と検証では、正しさの程度が質的
に異なります。そして現実の LSI の設計コードやプログラミングで行えるこ
とは検証だと思います。

でも VDM では論理推論まで踏み込み、形式的「検証」を超えて、形式的「証
明」を主張します。私は、そんなことは実務で使えるはずがないと考えます。
LSI のような、すぐにお金に跳ね返る世界でも使われようともしていない
VDM の形式的「証明」はうさんくさいものだと思っています。

rabbit_cat さんの補足により、上の自分の判断に少しばかり自信を持てるよ
うになりました。ありがとうございました。

お礼日時：2008/07/19 08:36

No.1 回答者： rabbit_cat 回答日時： 2008/07/16 01:08

少なくとも、ＬＳＩの論理の設計では、形式的証明の手法が、すでに実際の実務でかなり広く行われています。

「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 までは実際には
使っていません。もし私の認識に誤りがあったら指摘してやってください。

お礼日時：2008/07/17 03:44