内容説明
本書は、ソフトウェア開発におけるいわゆる形式手法（ｆｏｒｍａｌ ｍｅｔｈｏｄｓ）の入門書である。プログラムの正しさを証明するためのプログラム検証理論と形式仕様記述との初歩を紹介している。
目次
第１章 プログラムの正しさ―プログラムの検証入門
第２章 Ｆｌｏｙｄ‐Ｈｏａｒｅ論理
第３章 仕様としての事前条件と事後条件
第４章 ＶＤＭ‐ＳＬによる仕様記述の例
第５章 例題で見るシステム仕様記述
第６章 事例で見る実用的仕様記述
付録Ａ ＶＤＭ‐ＳＬ概説
付録Ｂ Ｚによる仕様記述
著者等紹介
荒木啓二郎［アラキケイジロウ］
１９７６年九州大学工学部情報工学科卒業。１９８２年工学博士。現在、九州大学大学院システム情報科学研究院情報工学部門教授
張漢明［チョウカンメイ］
１９９９年奈良先端科学技術大学院大学情報科学研究科情報システム学専攻博士後期課程修了。１９９９年博士（工学）。現在、南山大学数理情報学部情報通信学科助教授
※書籍に掲載されている著者及び編者、訳者、監修者、イラストレーターなどの紹介情報です。
