ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
http://iiyu.asablo.jp/blog/2010/07/29/5254538
高品質高信頼ソフトウェア開発の特別セミナー
http://iiyu.asablo.jp/blog/2010/07/29/5254545
VDM++によるオブジェクト指向システムの高品質設計と検証
で書いた続き。

　フォーマルメソッド(形式仕様記述、Formal Methods)の日本語の教科書のリ
スト。
　この前、九大に行ったときに、荒木先生からもらった資料に基づき、テキト
ーに(笑)、並べてみました。
　英語はもっとあるが、とにかく、日本語で読めることが普及には大事なので。
　ほかに専門誌や論文誌の記事や論文もいっぱいあるけど、一般に簡単には入
手できないし、とてもじゃないがリストできないので、それは省略。

　教科書に行く前に、NTTデータの山本修一郎氏による紹介記事があったので、
それをまず。
【新・言語進化論】仕様記述言語を知っていますか？
http://thinkit.co.jp/free/article/0711/6/1/
第1回：仕様記述言語を紹介するにあたって
http://thinkit.co.jp/free/article/0711/6/2/
第2回：仕様記述言語の種類について
http://thinkit.co.jp/free/article/0711/6/3/
第3回：Z言語とVDM-SLの記述例
http://thinkit.co.jp/free/article/0711/6/4/
第4回：Z言語とVDM-SLの違いとその効果

　さて、教科書。
　まず、ざっくり入門に最適なのが、
http://www.amazon.co.jp/exec/obidos/ASIN/4274132633/showshotcorne-22/
プログラム仕様記述論 (IT Text) [単行本]
荒木 啓二郎 (著), 張 漢明 (著)

http://iiyu.asablo.jp/blog/2006/08/20/491884
形式仕様記述(フォーマルメソッド、Formal Methods)
でも書いたように、内容は、九大で公開もされています。
http://dontaku.csce.kyushu-u.ac.jp/books/ProgramSpecification/
プログラム仕様記述論
--- ここから ---
　ただ、公理や規則などポイントのみで、文章による説明はほとんどあ
りません。説明がほしいなら本でしょうね。
(略)
だから、併用するのが一番ですね。
--- ここまで ---
という感じ。

　それから、
http://iiyu.asablo.jp/blog/2010/07/29/5254545
VDM++によるオブジェクト指向システムの高品質設計と検証
で紹介した荒木先生の推薦文が巻頭にある
http://www.amazon.co.jp/exec/obidos/ASIN/479811961X/showshotcorne-22/
VDM++によるオブジェクト指向システムの高品質設計と検証 [大型本]
ジョン・フィッツジェラルド、ピーター・ゴルム・ラーセン、ポール・マッカ
ージー、ニコ・プラット、マーセル・バーホフ (著), 酒匂 寛 (翻訳)

http://www.amazon.co.jp/exec/obidos/ASIN/4000056093/showshotcorne-22/
ソフトウェア開発のモデル化技法 [単行本]
ジョン フィッツジェラルド (著), ペーター・ゴルム ラーセン (著), John
Fitzgerald (原著), Peter Gorm Larsen (原著), 荒木 啓二郎 (翻訳), 荻野
隆彦 (翻訳), 染谷 誠 (翻訳), 張 漢明 (翻訳), 佐原 伸 (翻訳)

http://www.amazon.co.jp/exec/obidos/ASIN/4764903474/showshotcorne-22/
Bメソッドによる形式仕様記述―ソフトウェアシステムのモデル化とその検証
(トップエスイー実践講座) [単行本]
来間 啓伸 (著), 中島 震 (監修)

http://www.amazon.co.jp/exec/obidos/ASIN/4764903474/showshotcorne-22/
SPINモデル検査―検証モデリング技法 [単行本]
中島 震 (著)

http://www.amazon.co.jp/exec/obidos/ASIN/4274208443/showshotcorne-22/
SPINモデル検査入門 [単行本（ソフトカバー）]
Mordechai Ben-Ari (著), 中島 震 (翻訳), 谷津 弘一 (翻訳), 野中 哲 (翻
訳), 足立 太郎 (翻訳)

http://www.amazon.co.jp/exec/obidos/ASIN/4764903547/showshotcorne-22/
SPINによる設計モデル検証―モデル検査の実践ソフトウェア検証 (トップエス
イー実践講座) [単行本]
吉岡 信和 (著), 青木 利晃 (著), 田原 康之 (著)

http://www.amazon.co.jp/exec/obidos/ASIN/4883732584/showshotcorne-22/
形式手法の技術講座―ソフトウェアトラブルを予防する [単行本]
佐原 伸 (著)

http://www.amazon.co.jp/exec/obidos/ASIN/4764955059/showshotcorne-22/
モデル検査 初級編―基礎から実践まで4日で学べる [単行本]
産業技術総合研究所システム検証研究センター (著)

http://www.amazon.co.jp/exec/obidos/ASIN/4764955067/showshotcorne-22/
モデル検査 上級編―実践のための三つの技法 [単行本]
産業技術総合研究所システム検証研究センター (著)

関連：
http://iiyu.asablo.jp/blog/2006/08/20/491884
形式仕様記述(フォーマルメソッド、Formal Methods)
http://iiyu.asablo.jp/blog/2005/08/30/57720
荒木先生の形式仕様記述の教科書
http://iiyu.asablo.jp/blog/2008/08/04/3672175
形式的仕様記述の国際会議ICFEM2008
http://iiyu.asablo.jp/blog/2007/08/06/1708469
仕様記述言語Zのテーマソングが決定
http://iiyu.asablo.jp/blog/2008/09/20/3775398
Eiffel, 仕様記述(フォーマルメソッド)