プログラム検証論 の商品レビュー

林晋(著者)

2011/06/25

プログラムの検証を考えるならまず本書を読むことをお薦めします。
はじめに、第１章に、なぜ、この本を書いたか、この本の内容がどうしてこうなっているかの説明があります。プログラムの不具合があるかどうかを確かめる必要があり、そのために形式手法がどのような役に立ちそうかという見通しが書かれています。
最大公約数を求めるプログラムが、自然数の最大公約数しか求めないプログラムだったお話という具体例で、プログラムの正しさと、プログラムの仕様や説明書について、なるほどと言える説明をしている。プログラムの仕様や、説明書に、自然数の最大公約数しか求めないプログラムであることを明記していれば、正しいことが証明できたという話は、しばしば現実の問題でも直面することなので、大変参考になりました。

具体的な中身では、次のところで少し引っかかっているので記録します。
P29代入文の公理
{A[t/a]} a:=t{A}

{11>3} a:=11{a>3}
a:=t
という代入が正しくないことがないだろうか。例えば、tがaの型よりも大きい場合。
負の数が補数である場合に、aは3よりも小さくなることがないだろうか。
その部分をどのように検証すればよいのだろうか。

P40 while文の規則（完全正当性の場合）
変数nはプログラムPには現れてはいけないとする。
という制約条件がある。
しかし、この制約条件をどのように満たしているかを検証できるかどうかが課題とならないだろうか。ポインタ変数を使っていれば、実質上の変数nがプログラムPに現れないことを保証するのは大変な作業である。また、他の原因で変数nの値を書き換えないことを保証しないといけないのではないだろうか。