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