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 23:09:07 +0000 (UTC) Organization: Information Engineering, University of the Ryukyus Lines: 43 Message-ID: <3990498news.pl@rananim.ie.u-ryukyu.ac.jp> References: <3990496news.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 1094944147 32139 133.13.48.71 (11 Sep 2004 23:09:07 GMT) X-Complaints-To: news-admin@ie.u-ryukyu.ac.jp NNTP-Posting-Date: Sat, 11 Sep 2004 23:09:07 +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: <10196.1094944150.1@insigna.ie.u-ryukyu.ac.jp> Xref: ccsf.homeunix.org fj.comp.lang.c:417 河野真治 @ 琉球大学情報工学です。 In article , yas@is.tsukuba.ac.jp (Yasushi Shinjo) writes > 新城です。loop invariant は、けっこう厳しい。 これは、その通りで、実際の検証に使うには難しすぎるみたいですね。 そういう難しすぎる手法もたくさんあります。ポリヘドラ系とか。 > ハードウェアの設計では、形式的な証明の技術を使っているのですか。 まず、作成したLSIの歩止まりを判定しなければならないので、一 通り(回路毎)のテストを生成する必要があります。LSI設計の限界 は、それで決まると言われているようですね。 もう一つは、ハードは修正が高く付くことが多いので、ハードは修 正せずにソフトで対処する... じゃなくて、モデル検証などを使っ ても元が取れます。Intel はPentinumの乗算器のミスで痛い目にあ ったので力を入れているようですね。 例えば、 main() { while() { main_loop: if (event = event()) hoge(event); } } みたいなメインループを持つシステムは多いですよね。(Operating System とかもそう) この時に、 常にメインループに戻って来る あるいは、 メインループに5msec以内に戻って来る ってのを保証したいでしょ? これは自然だと思うんだ。で、 [] <5msec> main_loop 常に、5msec 以内に、main_loop に到達する みたいなプロパティを検証するわけです。これはトートロジーっぽく ないんじゃないかな。 --- Shinji KONO @ Information Engineering, University of the Ryukyus 河野真治 @ 琉球大学工学部情報工学科