Path: ccsf.homeunix.org!ccsf.homeunix.org!news1.wakwak.com!nf1.xephion.ne.jp!onion.ish.org!news.daionet.gr.jp!news.yamada.gr.jp!newsfeed.media.kyoto-u.ac.jp!oix.u-ryukyu.ac.jp!u-ryukyu.ac.jp!ie.u-ryukyu.ac.jp!not-for-mail From: kono@ie.u-ryukyu.ac.jp (Shinji KONO) Newsgroups: fj.comp.lang.c Subject: Re: assert() and precondition and invariant Date: Sat, 11 Sep 2004 10:18:15 +0000 (UTC) Organization: Information Engineering, University of the Ryukyus Lines: 50 Message-ID: <3990496news.pl@rananim.ie.u-ryukyu.ac.jp> References: <3990493news.pl@rananim.ie.u-ryukyu.ac.jp> NNTP-Posting-Host: insigna.ie.u-ryukyu.ac.jp Mime-Version: 1.0 Content-Type: text/plain; charset="iso-2022-jp" Content-Transfer-Encoding: 7bit X-Trace: naha.ie.u-ryukyu.ac.jp 1094897895 10457 133.13.48.71 (11 Sep 2004 10:18:15 GMT) X-Complaints-To: news-admin@ie.u-ryukyu.ac.jp NNTP-Posting-Date: Sat, 11 Sep 2004 10:18:15 +0000 (UTC) X-Image-URL: http://www.ie.u-ryukyu.ac.jp/~kono/skono.gif Fcc: send X-Newsreader: news.pl,v 1.11 2003/10/08 11:51:01 Content-ID: <8828.1094897898.1@insigna.ie.u-ryukyu.ac.jp> Xref: ccsf.homeunix.org fj.comp.lang.c:412 河野真治 @ 琉球大学情報工学です。 In article , yas@is.tsukuba.ac.jp (Yasushi Shinjo) writes > この辺りに検証が使えないという問題の本質があるかもね。C言語 > でプログラムを書く時と assert() のレベルは近い。けど、 > validity とかsatisfiablity というのレベルとは違う。違うレベ > ルで書く事が難し。 まったく違いますね。このあたりが、ハードウェアの信頼性とソフ トウェアの信頼性の差を生んでいる原因だと思います。僕は、ある 時点で、検証されないソフトウェアが受けいられなくなると思う。 動くソフトと、ちゃんと動くソフトの差は結構大きい。 > assert() の記述から検証用の条件を自動生成できれば、いいんじゃ > ないですか。 それはあったと思います。つうか、最近はそういうのが主流かも。 なんだけど、自動生成したものが検証可能かどうかはわからないと 思う。なんかの制限が必要ですね。 > 昔、「実行可能な仕様」というのがあったけど、あれはどうなった > んだろう。 > > [] (ボタンが押される -> <> 反応変数がセット) > こんな感じにハンドアセンブルしないとだめなのね。今の段階では。 > おまけに、このハンドアセンブルが正しいかどうかも不明です。 そういう言い方するのか。この作業は、 プログラムがちゃんと動くということはどういうことなのか っていうのを定義していく作業なんです。それが仕様を書く、ある いは、検証可能なプロパティを決める、あるいは、十分なテストを 書くってことですよね。 僕は、それができないプログラマは、もう役に立たないと思う。 > それで、最後は、この検証に通ったものを正しいとすると定義する > しかなくなって、トートロジーっぽくなるわけです。 例えば、ループインバリアントって、あんまり自明じゃないですよ ね。だけど、ループインバリアントをチェックするのは、トートロ ジーっぽいよね。でも、そのループの正しさって実は、ループイン バリアントで定義されるわけだよね。検証は、どっちかっていうと、 インバリアントを見付ける作業です。 --- Shinji KONO @ Information Engineering, University of the Ryukyus 河野真治 @ 琉球大学工学部情報工学科