パソコン書籍店

その通りだと思います．この本の重点は「プログラムの正当性の証明」ではなくて，間違いのないプログラムを開発するために，証明を利用することと考えています．つまりプログラムの仕様である「事前条件」と「事後条件」から「最弱事前条件」を計算したり，「ループ不変式」を導出して，その結果を利用しながら，プログラムを開発する方法を説明しております．例えば，事後条件が andでつながれた連言の場合，その連言肢（積項）の一つを削除してループ不変式を作り，同時にこの削除した連言肢の否定をループ繰り返しの条件とせよ，という定理はすぐに利用できます．

プログラムを書いてみて，うまく動けば良いし，うまく動かなければ，動くまで，あちこち訂正すればよいと考えておられる方に，この本をお薦めします．
細かくまとまっている名著
ボクは学生で研究にこの本を読むことになったのですが、よくまとめられていると思います。読み手はプログラミングに行き詰まった人から研究をしようとしている人までがよいと思います。ある程度プログラムに精通してないと読んでもわかりません。

内容はよくまとまっているのですが、細かくまとめすぎていて、定理なんかも丁寧すぎて逆にそれが読みにくくなっています。ですのである程度読み手を選んでしまう本であるともいえます。じっくり読まないと理解できません。ですが、プログラミングについての新たな境地を切り開くことができる良い本であることに変わりはありません。ボクの大学の教授たちの間でも名著としてあげられています。プログラマーには必須の本の一つと言っても過言ではないかもしれません。

内容は論理式などがでてきます。プログラムの正当性の証明、繰り返し部分の証明や開発の仕方などです。ループ不変条件を利用したプログラムなどは読んでみるとかなりおもしろいです。