ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
　東京は、今日は少し過ごしやすいが、この前、猛暑、酷暑のときに、姉から
来たメール。

正ちゃん、煮えてないかね？

の一言。
　すごいのぉ、お前のお姉さん。暑すぎて煮えてないかという言い方、言語感
覚がすごい。
　そうやろ。びっくりしたわ。
　ちょっと、あなたたち、二人とも、勘違いしてらっしゃるんじゃない？
　(二人そろって)えっ!?
　つまり、あなたのお姉様は、あなたを食料だと思って、そろそろ食べ頃かな
と思って、メールなさったんじゃないかしら。
　(二人そろって)そ、そうか。そういう読み筋もありか。＼(^O^)／
　ほらほらほら。お前、いっつも、「こいつを食料にしろ」なんてわめいてる
から。
　いやーん、姉ちゃん、おれ、食料にせんでちょうだい。

補足解説：
　「食料にしろ」は、情報省用語で、使えない人間を、食料にすること。
　食料だけではもったいないので、最近は、「リサイクルしろ」ともいう。
　リサイクルは次の流れで行なわれる。
　(1) 人体実験に使う。これで医学・医療の発展に貢献する。
　(2) 臓器を販売する。これで資金を稼ぐ。あるいは財政難の国庫に貢献する。
　(3) 食料にする。将来の食糧危機に備えて、備蓄される。

ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
　Macintosh(マック)でWindowsアプリが動くようにする、互換レイヤーソフト
の「CrossOver Mac 9 Standard」が出ますね。

http://www.amazon.co.jp/exec/obidos/ASIN/B003VWK400/showshotcorne-22/
CrossOver Mac 9 Standard
ネットジャパン

　紹介記事は、
http://itpro.nikkeibp.co.jp/article/NEWS/20100721/350478/
ネットジャパン、Mac上でWindowsアプリが動作する互換レイヤーソフト
　詳しい製品情報は、
http://www.netjapan.co.jp/r/product_mac/com_9/

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, 仕様記述(フォーマルメソッド)

ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
http://iiyu.asablo.jp/blog/2010/07/29/5254538
高品質高信頼ソフトウェア開発の特別セミナー
で書いた続き。
　形式仕様記述(フォーマルメソッド、Formal Methods)関係の新刊が出ます。
　翔泳社の古田島さん(コタさん)。
　大して数が出ないだろうし、儲からないだろうから、社内で肩身が狭いかも
しれないが、こういう大切な本を出してくれて、ありがとうございます。
http://iiyu.asablo.jp/blog/2008/07/04/3609430
翔泳社 IT Architects’Archiveシリーズ
で書いたように、がんばって、出してくれてるんですよね。このシリーズは、
たぶん、ほぼ全てコタさんが手がけたものだろうと思います。
　さて、本題の新刊というのが、
http://www.amazon.co.jp/exec/obidos/ASIN/479811961X/showshotcorne-22/
VDM++によるオブジェクト指向システムの高品質設計と検証 [大型本]
ジョン・フィッツジェラルド、ピーター・ゴルム・ラーセン、ポール・マッカ
ージー、ニコ・プラット、マーセル・バーホフ (著), 酒匂 寛 (翻訳)
　コタさん、献本、ありがとうございます。

　翔泳社にあるページは、
http://www.seshop.com/product/detail/12267/
VDM++によるオブジェクト指向システムの高品質設計と検証

　送られてきた本書をみると、なんと、オビに九州大学の荒木啓二郎先生のお
言葉が。しかも、巻頭に荒木先生の推薦文が。
　今度、九大に行くときに持っていって、荒木先生にサインしてもらおうかな。＼(^O^)／

　内容は、目次をみれば想像がつくと思うが、フォーマルメソッドでモデル化
する意義、VDM++やツールの解説、設計やモデリングの実際、モデルからJava
による実装まで、フォーマルメソッドを実際に適用するとは、どういうものか
を、わかりやすく解説したもの。
　ケーススタディで、おおっと思ったのが、第２次世界大戦中、ドイツが誇っ
た超強力暗号エニグマの例。エニグマ暗号機をVDM++でモデル化するの。
　エニグマのロータやプラグボードもモデル化している。エニグマを知らない
人のために、歴史などの解説があって、チューリングたちが解読したこと、世
界最初のプログラム可能な電子式コンピュータの１つであるコロッサス
(Colossus)のこと、チャーチルが秘密を守るためにコロッサスを解体し、情報
封鎖したために、ENIACより先に稼働していたのに、長らく世界最初のプログ
ラム可能な電子計算機だということが世界に知られてなかったことなどなどが
出てくる。
　脱線するが、エニグマにまつわるこの辺の話を含め、暗号の歴史を知るには、
それもわくわくする筆致で詳しく知るには、
http://iiyu.asablo.jp/blog/2008/12/22/4020425
楕円曲線、暗号といえば
をはじめ、何度も紹介している、
http://www.amazon.co.jp/exec/obidos/ASIN/410215972X/showshotcorne-22/
サイモン・シン著, 青木薫訳「暗号解読 上巻 (新潮文庫 シ 37-2)」
http://www.amazon.co.jp/exec/obidos/ASIN/4102159738/showshotcorne-22/
サイモン・シン著, 青木薫訳「暗号解読 下巻 (新潮文庫 シ 37-3)」
がお薦め。

　さてさて、フォーマルメソッド、VDM++といえば、最大、最高の成功事例は、
フェリカネットワークスの事例。
http://iiyu.asablo.jp/blog/2006/08/20/491884
形式仕様記述(フォーマルメソッド、Formal Methods)
で、
http://techon.nikkeibp.co.jp/article/HONSHI/20051213/111568/
日経エレクトロニクス2005年12月19日号
特集「ソフトウェアは硬い」
に出ているフォーマルメソッドの記事の中でも、
--- ここから ---
フェリカネットワークスの事例がインパクトがありまくり。ここは、モバイル
FeliCa、つまり、EdyとかSuicaとかおサイフケータイなどをやっている会社で
す。
--- ここまで ---
と書いたが、この前、九大に行ったときに、荒木先生から聞いた話では、
FeliCaの事例は、おれだけじゃなくて、世界的にもインパクトがありまくりで、
国際会議をはじめ、あちこちから講演してくれという話が多いらしい。
　フェリカネットワークスの人たちは、本書で解説してある形式仕様記述言語
VDM++で、10万行も書いたんだから、すごいよね。しかも、仕様の段階で350件
ほどのバグを潰している。
　そして、ほんとにすごいのは、FeliCaのチップは、Edy, Suicaをはじめいろ
んなところで、去年の段階で１億数千万枚使われているらしいが、これまでチ
ップにはバグが１つもないこと。
　これだけ広く社会に使われているもので、バグが１つもないなんて、ほとん
ど奇跡にしか思えないわけで、ギネスブックに申請しようかという話があるく
らいだそうだ。
　おれがみるところ、成功の要因は、単にVDM++を使ったからよかったなどと
いう話ではない。
　もちろん、フェリカネットワークスの人たちが優秀ということもあるだろう
が、開発プロセス全体をちゃんと見直して、再構築している。
　つまりですね。現場の優秀さだけじゃなくて、経営者、経営層がバカだと、
こうはならないんですよ。経営者、経営層の理解があって、こういうことに投
資できないと成功しないわけ。
http://ci.nii.ac.jp/naid/40017084078
経営者はアーキテクチャと形式手法を忘れてはいけない
藤枝純教
という論文もあるくらい。

　フェリカネットワークスの栗田太郎さんの論文が読めますね。
http://www.ipsj.or.jp/15dp/Vol1/No3/IPSJ-DP0103007.pdf
モバイル FeliCa のソフトウェア開発における品質確保のための構造と実践
フェリカネットワークス　栗田太郎

　このあと、フォーマルメソッドに関する日本語の教科書のリストを書く。

追記：書いた。
http://iiyu.asablo.jp/blog/2010/07/29/5254556
フォーマルメソッド(形式仕様記述、Formal Methods)の教科書

関連：
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, 仕様記述(フォーマルメソッド)