ASAHIネット(http://www.asahi-net.or.jp)のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
　国立情報学研究所の
http://www.topse.jp/wp/wpb.da3
「トップ」ソフトウェア開発者養成プログラム
の話題をみて、
http://www.topse.jp/wp/wpb.da3?wpcmd=chg_page&wppid=2259&wpprcid=9852
受講内容
にある、シラバス

要求分析
形式仕様記述
設計モデル検証
コンポーネントベース開発
アジャイル開発

の２番目、形式仕様記述
http://www.topse.jp/wp/img/contents/syllabi2.pdf
の参考文献には、この前、日本語と中国語の会話形式でソフトウェア工学の実
践的入門ができると
http://www.asahi-net.or.jp/~ki4s-nkmr/kaiwa-software-eng.html
に紹介記事を書いた「会話によるソフトウェア工学の開発実践」を監修なさっ
た、ソフトウェア工学上の恩師であり、筒井康隆さん・山下洋輔さん方面でも
わが師でもあり、中洲の飲み先輩でもある荒木先生の本が２冊入ってますね。

　１冊は訳書で、
http://www.amazon.co.jp/exec/obidos/ASIN/4000056093/showshotcorne-22/ref=nosim
ソフトウェア開発のモデル化技法
ですが、もう１冊の
http://www.amazon.co.jp/exec/obidos/ASIN/4274132633/showshotcorne-22/ref=nosim
荒木啓二郎，張漢明：プログラム仕様記述論，オーム社 2002.
は、以前、送ってくださった本です。
　この前、「会話によるソフトウェア工学の開発実践」を紹介したとき、
「荒木先生のご著書を紹介してないのは、つまらないからではなく、プログラ
ムの理論であり、意味論や公理系など専門性がとても高いので、私の頭がつい
ていかないせいです。すみません」
などと言い訳した本です。

　荒木先生にうかがったところ、形式仕様記述の書き下ろしの日本語の教科書
は、荒木先生と張さんのこの本しかないそうです。これが入門編で、続編をあ
と２冊、少しまとまった事例編と、大規模事例編を出したいそうです。
　訳本が、少しまとまった事例編でもあるので、教科書は、その訳本に繋がる
ように意識していて、そのため、使った仕様記述言語も、当初は Z にしてい
たのを訳本に合わせて VDM にしたそうです。でも、訳本ではなくて、国産の
事例で書き下ろしを書かなくてはいけないと思っていますとのことです。

　なるほど、それで Z の解説が付録になってるんですね。なんだか、その話
も昔研究室にお邪魔したときに聞いたような気がしてきた。つーか、おれ、こ
の本のゲラ、研究室で見せてもらったんじゃないか。＼(^O^)／
　もう、ぜーんぶ忘れてた(泣)。

　仕様記述言語の世界は、ホーアとかスコットのプログラムの意味論などと同
様、一般プログラマからみれば数学的な世界です。そういうと全然役に立たな
い高踏的世界に思えるかもしれませんが、いまや、いろいろ役に立つ事例もで
てきていて、仕様記述言語を使った通信プロトコルの形式的仕様記述なんてこ
ともやってますよね。

　最近、また何回目かのLispのハシカに罹っていて(笑)、その前から関数型言
語やらをつらつら眺めていたんですが、そしたら形式仕様記述の話ですもんね。
それも「会話によるソフトウェア工学の開発実践」の話題を書いたら、こうだ
もん。なんか流れができちゃってる。

関連：
http://iiyu.asablo.jp/blog/2005/08/21/50510
快挙「会話によるソフトウェア工学の開発実践」

　実は、Lispハシカに罹るつもりはなかったんですが、
http://www.amazon.co.jp/exec/obidos/ASIN/1590592395/showshotcorne-22/ref=nosim
Practical Common Lispという本のせいで、完璧に罹っちゃいましたね。
　７月には、この１年くらい興味深く見守っていたプログラミング言語の話題
を書こうと思っていたけど、いまは早く「Practical Common Lisp」の紹介を
書こうと思ってます。
　この本読むと、やっぱ、Lispがあれば、そこらのスクリプト言語やらは全部
要らんわ状態になっちゃうんだもんね。すごいよ。それくらい面白い。