[ トップへ | 全ページ一覧 | 最近の更新 ]　[変更点]　[ 過去ログブラウザ | ファイルマネージャ ]

「プログラム検証論」林 晋 著

初版1刷と初版2刷の内容が異なっていることが判明。 共立出版さん、そういうのは第2版って普通いいませんか? ともかく、著者のページに有る正誤表 http://pascal.seg.kobe-u.ac.jp/~hayashi/books-jp.html は初版1刷を現行(2001年06月21日 (木) 22:27:01現在)の『初版2刷』同等にする訂正のようだが、 それでもまだ誤りが目立つ。ということで..

98/3/20 初版2刷 の私家版Errata

多くなってきたからページを分ける。 プログラム検証論Errata-1/プログラム検証論Errata-2 /プログラム検証論Errata-3/6.2非決定的プログラムとその検証

p.151 配列の代入公理 の前後から、ところどころ代入文の記号が := でなく = になっている。

p.152 表明 A0 の 3 の後半 a[k] ≦ a[j+1] は、 そのページの下から2行めを見て a[h] ≦ a[j+1] と思われる。

p.154 l.7 「代入を一つにまとめれ」などという操作が形式的に定義されたことはない。

p.154 l.-3 突然「1/0 の評価時」と書いて division by zero のことだとは通じない。

プログラム検証論-その他気になったこと

p.115 5.1.2 semantics, syntax を「働き」「書き方」と呼ぶ人は初めて。 「合成性」と「働き」の話の順序がまずい。

p.117 lemma 「停止するならば」最後のラベルから出て行く．と補足が必要。

p.124 (5.8) 式 pwp(P,B) は前ページの「その集合と同一視される表明」と読ませるには それなりの記号を用意するべき。次の行も同じ。

p.150 a[1+1]=3 という表明は、pwp を求めると FALSE になるので、 「問題がない」と言い切るにはちょっと例が悪いのではないかと..