河野真治 @ 琉球大学情報工学です。

In article <s7f1xh48p6r.fsf@xxx.kgc.co.jp>, candy@xxx.kgc.co.jp writes
> yas@is.tsukuba.ac.jp (Yasushi Shinjo) writes:
> > これなら、Ｃ言語と Lisp とか、違うプログラミング言語で２回プ
> > ログラムを書いて同じ結果が出てくるか調べた方が楽じゃないかなあ。
> なるほど!! そうすると今度は C と LISP のプログラムが
> 等価であることを証明するために、5 倍位の労力を要するわけですね!!

プログラム単体の正しさを証明するより、等価性を証明する方がや
さしいと言われています。ハードウェアの方だと等価性判定器に関
する研究が流行ったことがあって、かなりの大規模な回路(えーと、
数万ゲートぐらいだったかな。状態があるとだめなんだけど)まで
判定できます。ただ、First order の等価性判定は難しいらしい。

In article <YAS.04Sep15033225@kirk.is.tsukuba.ac.jp>,yas@is.tsukuba.ac.jp (Yasushi Shinjo) writes
> わりと、本質を付いているんじゃないですか。つまり、
> ・Ｃ言語で総和のプログラムを書くより、ループ不変量を書く方が難しい

これは、そうなんですよね。ループ不変量は、ループを脱出した時
に満たす条件よりも豊富な情報量を持っていて、そこからループ一
回の操作に関する入力と出力を導出出来る程です。

> ・Σの方はバグがあるのかないのかわからない

これは、良くある間違いなんだけど、Σの方はモデルの持つ数学的
条件なのでプログラムではないです。

なんだけど、仕様とかループ不変量の間違いをどうやって見つける
っていうか、そもそも、その「仕様の間違い」ってなんだよとか、
いろいろ議論はあるんだけどさ。

で、結局、

     仕様   <===>   実装

ではだめで、
          
           -プログラム->
     仕様   <==========>   実装
      ||                    ||
      ======= 事例  ==========
  <-分析----          <--実行---
    テスト

というようにしたりします。

事例の集合でプログラムの意味を定義出来るてのが表示的意味論な
んだけど残念ながら無限集合になってしまいます。実装と仕様を
一致させるためには操作的意味論が重要なんだけど、プログラム
と同じになってしまってあまり役に立たない。

なんだけど、モデル(データ構造で表されたプログラムの意味)
みたいなのが事例に対応するってあたりでいろんな技術が開発
されたわけですね。

---
Shinji KONO @ Information Engineering, University of the Ryukyus
河野真治 @ 琉球大学工学部情報工学科