商品の説明
内容（「MARC」データベースより）
1.プログラムの検証 2.ホーア論理入門 3.形式的理論 4.ホーア論理詳説 5.ホーア論理の数学 6.ダイクストラの検証法 7.古典理論を越えて 8.形式的技法
登録情報
|
この商品を見た後に買っているのは？
カスタマーレビュー
最も参考になったカスタマーレビュー
3 人中、2人の方が、｢このレビューが参考になった｣と投票しています。
形式:単行本
プログラムの検証を考えるならまず本書を読むことをお薦めします。
はじめに、第１章に、なぜ、この本を書いたか、この本の内容がどうしてこうなっているかの説明があります。プログラムの不具合があるかどうかを確かめる必要があり、そのために形式手法がどのような役に立ちそうかという見通しが書かれています。
最大公約数を求めるプログラムが、自然数の最大公約数しか求めないプログラムだったお話という具体例で、プログラムの正しさと、プログラムの仕様や説明書について、なるほどと言える説明をしている。プログラムの仕様や、説明書に、自然数の最大公約数しか求めないプログラムであることを明記していれば、正しいことが証明できたという話は、しばしば現実の問題でも直面することなので、大変参考になりました。
具体的な中身では、次のところで少し引っかかっているので記録します。
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の値を書き換えないことを保証しないといけないのではないだろうか。
はじめに、第１章に、なぜ、この本を書いたか、この本の内容がどうしてこうなっているかの説明があります。プログラムの不具合があるかどうかを確かめる必要があり、そのために形式手法がどのような役に立ちそうかという見通しが書かれています。
最大公約数を求めるプログラムが、自然数の最大公約数しか求めないプログラムだったお話という具体例で、プログラムの正しさと、プログラムの仕様や説明書について、なるほどと言える説明をしている。プログラムの仕様や、説明書に、自然数の最大公約数しか求めないプログラムであることを明記していれば、正しいことが証明できたという話は、しばしば現実の問題でも直面することなので、大変参考になりました。
具体的な中身では、次のところで少し引っかかっているので記録します。
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の値を書き換えないことを保証しないといけないのではないだろうか。
リストマニア
|
|
同じキーワードの商品を探す
フィードバック
- カタログ情報、または画像について報告
- 著者からのコメント
- 出版社からのコメント
