Google
ブログ(iiyu.asablo.jpの検索)
ホットコーナー内の検索
 でもASAHIネット(asahi-net.or.jp)全体の検索です。
 検索したい言葉のあとに、空白で区切ってki4s-nkmrを入れるといいかも。
 例 中村(show) ki4s-nkmr

ウェブ全体の検索

疲れる日々2006年08月06日 23時01分07秒

ASAHIネット(http://www.asahi-net.or.jp)のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 また、ダイヤ乱れ。
 昨夜(2006/08/02)は、都営地下鉄が車両故障。直通運転している京王線もダ
イヤ大乱れ。
 なんか、帰りにああいうことになってると、余計疲れるね。

 最近、毎朝、毎晩、以後・将棋チャンネル三昧で寝不足。タイトル戦やら面
白い対局からが多くて、午前2時くらいまでみて、朝7時からまたみたり。サ
ッカーワールドカップのときとあまり変わらん。
 あとは、音楽三昧。昔のフュージョン、少しではあるけど、CD復活してます
ね。一昨日は深町純さんを見つけて大興奮して、寝られない。\(^O^)/
 DVD「三丁目の夕日」、泣いたな。去年買ったカシオペア&シンクロナイズ
ドDNA、この前買ったチック&バートンのDVD(ニューヨークじゃなくて、ドイ
ツで録画したデュオ)をまた観て、感動した。
 あとは、言語とオントロジーとバイオの調査、お勉強、実装、その他。いろ
いろプロジェクトのあれこれも面倒みなくちゃいけないし。それにしても、ど
うしてあんな腐ったコードを書くのかな。何度も言っても直らない。フツー、
クビだよね。
 そんなこんなで、ここに書く時間がないです。

 Cleanと関数型・論理型言語。Formal Methodsのことだけでも、今週中に書
きたいけど。



 疲れるわ。

純粋関数型言語Concurrent Clean2006年08月06日 23時06分22秒

ASAHIネット(http://www.asahi-net.or.jp)のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 以前から紹介しようとしてなかなか紹介できなかった関数型言語が、
Concurrent Clean(以後Clean)です。
 といって、大した紹介はできないけど、ご勘弁を。
 日本では、いまは、関数型言語の代表といえば、Haskellで、Haskell本も
http://www.amazon.co.jp/exec/obidos/ASIN/4839919623/showshotcorne-22/ref=nosim
向井淳著「入門Haskell~はじめて学ぶ関数型言語」(毎日コミュニケーション
ズ)
http://www.amazon.co.jp/exec/obidos/ASIN/4797336021/showshotcorne-22/ref=nosim
青木峰郎著, 山下伸夫監修「ふつうのHaskellプログラミング ふつうのプログ
ラマのための関数型言語入門」
の2冊が出ていて、どちらも好評。
 だったら、Cleanだって流行るはず。\(^O^)/
 Cleanって何?という人は、まず、公式サイト
http://www.cs.ru.nl/~clean/
をどうぞ。
 日本語なら、
 池田聡さんが各種資料をまとめらっしゃる
http://sky.zero.ad.jp/~zaa54437/programming/clean/
純粋遅延関数型言語Concurrent Clean
(Pure and lazy functional language : Concurrent Clean)
と、
 lethevert(どう発音するんだろう? どういう意味?)さんのサイト、
http://www.geocities.jp/lethevert/softwares/clean/index.html
lethevertの純粋関数型言語Concurrent Clean覚え書き
をどうぞ。
 日本でのClean普及は、このお二人が孤軍奮闘状態といっていいんじゃない
か。この二人、すごいです。頭が下がります。くたびれない程度にがんばって
ください。

 中でも、lethevertさんの覚え書きは、入門として実にわかりやすい。
 だから、おれはもう2ヵ月も前に、いま、翔泳社にいる古田島さんに、
lethevertさんに連絡とって、このサイトの内容をベースにCleanの入門書を書
いてもらって、Haskell本が売れている今、ソッコーで出したらどうかといっ
たのに、先週、確認したら、何にもやってない。\(^O^)/
 翔泳社がやらないなら、Haskell本出してくれた、毎日コミュニケーション
ズとソフトバンクは、やってくれないかな。それとも地道に真面目にソフトウ
ェアの本を出し続けてくれてるオーム社にお願いかな。そういえば、オーム社
から出る予定の「On Lisp」の翻訳、いつになったら出るんだろう。^^;
 ともかく、出版社のみなさま、早い者勝ちですよ。と煽ってみる。^^;

 ところで、これを書くために、ちょろっとまた調べたら、lethevertさんは、
http://d.hatena.ne.jp/lethevert/searchdiary?word=Concurrent+Clean
lethevert is a programmerのConcurrent Clean
というページももってますね。
 しかも、どうやら、JavaでCleanを実装しているっぽいですね。すごいねえ。
 あ、ここにも、メルセンヌ・ツイスターの話がある。
 これ、以前、弾さんから教わったんだけど、紹介忘れてましたね。^^;
 メルセンヌ・ツイスター、擬似乱数標準の地位を着々と築きつつあるなあ。
これに関連して書きたい話があったの思い出した。バカのコメントにからめて
だけど。まあ、暇ができたらね。

 Haskellがわかる人なら、Cleanはすぐわかる。実際、HaskellとCleanのプロ
グラムは、ほとんど同じにみえるし。
 ぼくがいまどっちかを選べといわれたらCleanを支持するのは、
(1) コンパイラが非常に優秀
(2) GUIライブラリの充実
といった点で、実用性がHaskellより高いと思っているから。といって、実用
的なソフトは1行も書いてません。いつもながらの畳水練です。\(^O^)/

 (1)に関しては、Cと、少なくともgccのCと比べるなら、さほど遜色のない、
非常にいいコードを出す。
 ベンチマークをどこまで信じるかの問題はあるけど、ざっとした目安とする
なら、
http://shootout.alioth.debian.org/
The Computer Language Shootout Benchmarks

http://www.lib.uchicago.edu/keith/crisis/benchmarks/tak/
をどうぞ。

 (2)に関しては、CleanのIDE自身もCleanで書いてあるということと、ゲーム
もあれこれあって、実績がかなりあると思えるから。たとえば、
http://cleangl.sourceforge.net/
Clean Game Library
をどうぞ。

 関数型言語がブームとなれば、次に来るのは、あなた、形式仕様記述
(Formal Methods)のブームですよ。\(^O^)/
 ということで、この前、九大に教えに行ったとき、Formal Methodsの我が国
の第一人者である荒木啓二郎先生から直接お話を聞いて、仕入れてきました。
それは、次の機会に。
 Formal Methods、今週中に書くといいながら、ちょっと無理だったね。肩と
左手がもう悲鳴を上げて休ませないとだめだったから、これで勘弁ね。
 jouwa/salonに書いたフードファディズム(まだウェブやブログには転載して
ない)の続きも、しばらく時間ください。感動と恐怖の面白い話ばっかりで、
ネタはいくらも思いつくんだけどね。
 あ、あと、朝日に載ったWeb2.0の記事。服部桂がまとめた、あれ。梅田望夫、
やっぱだめ。偽物ね。西垣通さんを出したのスマッシュヒット。朝日的予定調
和の世界で、服部さんのせめてもの意地? これもいずれ詳しく。

フードファディズム2006年08月10日 09時32分56秒

ASAHIネット(http://www.asahi-net.or.jp)のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 これをjouwa/salonに書いたのは、2006/08/04だったので、最初は先週の週刊
ダイヤモンドと書いていたけど、もはや先週号じゃないので、2006/08/05号と
書きます。
 この号では、「危険な食卓」という特集やってて、ブルーバックスで出た
フードファディズム指摘本
http://www.amazon.co.jp/exec/obidos/ASIN/4062572311/showshotcorne-22/ref=nosim
高橋久仁子著「「食べもの情報」ウソ・ホント―氾濫する情報を正しく読み取
る」(講談社ブルーバックス)
をこの前買ったばかりでタイミング的にもいい。高橋先生、特集でも出てきま
す。
 それと科学ジャーナリストの松永和紀さんも出ている。この人、eMacさんが
教えてくれた
http://biotech.nikkeibp.co.jp/fsn/kiji.jsp?kiji=667
松永和紀のアグリ話●ロシア人科学者の遺伝子組み換え毒性試験を総括
の人だった。
 ほんとなら、この実験はデタラメだね。それを日本に呼んで、日本中回って、
遺伝子組み換え食品は怖い怖いとやってるのね。超能力者と称する連中を呼ん
で、テレビで行方不明の人間探す番組作ってるテレビ屋と同じひどさね。
 こういうバカな市民団体って、1960年代跋扈していた腐れ左翼、珍左翼を思
い出すね。最近は社会が右傾化して、今度は腐れ右翼、珍右翼が出てるもんね。
結局、尻馬に乗ってる連中は、腐れか、珍になるってこと。パソコンでも、PC
-9801, Macintosh, DOS/V、どのときもマイナーなときにはいいコミュニティ
が、メジャーになると腐れと珍が跋扈だもん。人間社会の宿命ね。
 松永さんは、週刊ダイヤモンドの中で、最近の酸素ブームはかなり怪しいとも指摘していますね。

 それにしても、テレビの「あるある」とか「みのもんた」に代表される健康
情報番組、煽るだけ煽って、ひどいね。
 ちゃんと番組テロップと音声で、
「これは個人の感想です。効能を述べたものではありません。科学的な根拠は
ありません」
「あるあるの実験は科学的ではありません」
「番組に踊らされてスーパーで食品を買い漁るのは猿未満の知能です(猿以下
と書いたら猿に悪いもんね)」
と流せよ。
 テレビショッピングで健康食品や器具を売るときは、そういうの流すでしょ。
健康情報番組もそれをやれ。白インゲンとかで健康被害まで出してるんだから。
 特集には、健康食品のコマーシャルがいかに誤ったイメージを送りつけてい
るか、サントリーの例も出てた。
 「燃焼系アミノ式」の「燃焼系」という言葉から、脂肪を燃焼するかのよう
に錯覚するのは視聴者の勝手。サントリー関係者によれば「日常生活を完全燃
焼!」の意味だそうだ。脂肪を燃焼なんてどこにもうたってないんだって。
 最近の「よからぬものが、ジョビジョバ~」の「よからぬもの」は、毒素と
かそういうのじゃなくて、「モヤモヤとした気持ち」だそうだ。毒素とかが出
ると思うのは、視聴者の勝手な錯覚なんだそうだ。
 おれ、サントリー、うまいこというなあと非常に感心した。さすが、受け答
えの教育が、しっかりしてますね。

 ほかにも、テレビの健康番組をよくみている層は、トクホ商品の利用が多い。
彼らは、自然・天然信仰で天然物や自然のものをありがたがり、添加物・科学
調味料を忌み嫌うが、トクホは人工物なのにという話もあって、なかなか嗤え
ます。人間の矛盾、非合理性がよく出ている。
 天然信仰といえば、江戸前の魚を珍重するのも、よーわからん。水銀の残留
度、外洋より江戸前の方が高いと思うけど、どうなの?
 水銀残留といえば、水銀が残留してても、シロナガスクジラの尾の身の刺身
とヒャクヒロが食えるなら、おれ、食うと思うなあ。マッコウとかミンクのク
ジラはどうでもいい。食いたいのはシロナガスだけ。子供のころの大ごちそう
だもん。
 おれが聞いた話じゃ、アミノ酸飲料を飲めばやせられると勘違いした女が、
毎日3リットル飲み続けて3ヵ月で糖尿病になったとか、ほんとなら非常識に
もほどがあるよね。

 あるあるが納豆やったら、いま、スーパーから納豆消えたんだってね。しか
も、番組が推奨した大粒納豆がなくなって、効果が薄いといったひき割り納豆
売れ残りらしい。
 こうも簡単に情報操作で大衆操作ができると、テレビ屋、笑いがとまらんだ
ろう。バカがいっぱいひっかかるんだもん。
 週刊ダイヤモンドの食の特集も、いかに大衆がバカで、企業や市民団体やテ
レビ屋にいいようにおもちゃにされ、金を巻き上げられ、健康を害したり健康
不安に怯えるように仕向けられているのに、それでいて、これだけ食べれば健
康になれるというマジックフードを追い求め、その上、身勝手極まる消費者エ
ゴを撒き散らしているのが、よくわかる。
 「健康番組などで有名な”血液サラサラ”という概念は医学的には存在しな
い」なども書いてあるから、テレビのあんな血液サラサラなんて信じてる奴は
バカなのね。
 以前、血液ドロドロやサラサラの映像は、全然ドロドロやサラサラを示して
いないという
http://allabout.co.jp/health/familymedicine/closeup/CU20040810A/index.htm
まだ基礎的研究段階の検査です。将来の発展に期待! 血液サラサラ?血液ド
ロドロ?
を紹介したけど、結局、いまだにこの段階なんでしょう?

 そんなこんなの一方、日本の足元では食糧危機が迫っているんだよね。興味
のある方は、週刊ダイヤモンドを一読を。
 週刊エコノミストも今週号は、特集が、
「食卓から魚が消える -日本の食料が危ない- マグロ高騰の深層,BRI
Cs爆食で穀物需給は逼迫」
だし、週刊東洋経済も
「社員の健康に目覚めた124社 デキる社員ほど「メタボリック」くん」
という健康ものだし。どっちもまだ読んでないけど、なくなる前に買いに行こ
う。
 こういうところでも、バカとちゃんとやってる奴でどんどん格差がつくんじ
ゃないか。テレビの健康番組を鵜呑みにするバカとちゃんと情報を集めて自分
で判断する努力をしている奴で、格差はあって当然だよね。
 で、そうやって研鑽してても、事故や病気で急死することもあって、世の中、
不条理ですよね。だから、文学があるんだけど。

 魚が消える話は、外国で魚食ブームという以外に、ちょっと前の日経サイエ
ンスの論文で、怖い話があるんです。地球温暖化や環境保護というと、みんな
大気の二酸化炭素濃度を気にしてるけど、海の酸性化の話。盲点でしょ。
 あった、あった。
http://www.nikkei-bookdirect.com/science/page/magazine/0606/ocean.html
日経サイエンス2006年6月号、S. C. ドニー「海洋酸性化の脅威」
ですね。冒頭だけだから、あとはバックナンバー頼むなり、図書館で読むなり
してください。おれには衝撃的だった。ほんとなら、人類があがいても、もう
手遅れだと思ったもん。

 自然を守れとか地球環境保護とか、思い上がりもいいとこ。地球や自然にと
って人類なんて、体についたほこり程度の鼻くそ以下の存在なんだから。人類
がどうなろうと関係なく地球や宇宙は自らの道を歩いているだけだもん。
 前も書いたけど、せめて、人類生存環境の維持といってほしいね。

 環境保護団体も、前述の市民団体みたいな手合いがいるね。食品と健康をめ
ぐる問題って、環境保護の話とよく似てる。
 おれのブログにも、コメントがついてて悲しい。なぜ悲しいかというと、あ
あいうのが、マイクル・クライトンが
http://www.amazon.co.jp/exec/obidos/ASIN/4152086688/showshotcorne-22/ref=nosim
「恐怖の存在」
で、拡大して見せた、多面的な思考ができず、共犯者たるメディアのいうこと
を鵜呑みして、単細胞、近視眼、視野狭窄的にしか物事がみえない人たちの典
型で、あらら、実例が引っかかって思うんだけど、ご当人は、気づかずに、コ
メントしてらっしゃる。

 国産安全とか添加物は悪とか、単純に信じるのは、地球にやさしい、環境に
やさしいなどとあれこれを鵜呑みにしているバカと同じなんだね。無知は罪。
 物事そんなに簡単じゃないのに、考える力がないから一番楽なワンフレーズ
に飛びつく。小泉に飛びついたバカと一緒。それで、いまごろになって、自分
らがこれからどんどん貧乏になるから、格差は許せんなどというんだもん。い
まごろ言ってももう遅いって。考えなかったお前らがバカというのが権力側の
扱いだもん。ダイエット目指してアミノ酸飲料飲みすぎて、糖尿病になった女
と一緒だね。
 そういう人の大量生産にせっせと加担しているのが、テレビ屋なんだよ。ほ
んと、人間のくずだよ。だから、「あるある」とか「みのもんた」に代表され
るあの手の番組、あと、細木数子とかスピリチュアルカウンセラーの江原なん
とかの番組、作ってる奴も出ている奴も、全員、死刑にしましょう。\(^O^)/
 司会やってるマチャアキとトキオの太一君も死刑かと思うと、ファンだから
かわいそうに思うけど、罪深いんだもん。\(^O^)/

 あと、補足したいこといろいろあるけど、またいつかね。
 eMacさん、いろいろ関係ある情報ありがとうございます。

 ところで、スーパーの棚から一気に寒天が消えうせた寒天ダイエット。
 あれ、まだやってる奴、100人のうち、何人いるの?
 おれの予想は、3人かな。\(^O^)/

 じゃ、おれはこれから、ヘルシーリセッタとエコナのブレンド油で、夏野菜
炒めを作ろうっと。
 お前、死んで、よし。\(^O^)/

国立健康・栄養研究所の「健康食品」の安全性・有効性情報2006年08月10日 09時33分45秒

ASAHIネット(http://www.asahi-net.or.jp)のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 国立健康・栄養研究所の「健康食品」の安全性・有効性情報は、面白いです
ね。
http://hfnet.nih.go.jp/
国立健康・栄養研究所の「健康食品」の安全性・有効性情報
をどうぞ。
http://hfnet.nih.go.jp/contents/index2.html
健康食品の基礎知識
には、
http://hfnet.nih.go.jp/contents/detail771.html
科学的根拠のある情報とは?
とあって、「あるある」や「みのもんた」系のテレビや雑誌の健康情報が科学
的にデタラメといって悪ければ、とってもテキトーなことがわかりますね。
http://hfnet.nih.go.jp/contents/index31.html
【話題の食品・食品成分】
にもいろいろあって、たとえば、
http://hfnet.nih.go.jp/contents/detail471.html
α-リポ酸の安全性・有効性情報(痩身効果との関連)
がありますね。これ、テレビでダイエットになるなんて煽っていたものですが、
科学的には有効性は確認できてませんね。^^;

第五世代コンピュータプロジェクトは死なず!\(^O^)/2006年08月10日 09時34分09秒

ASAHIネット(http://www.asahi-net.or.jp)のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
☆☆☆ 第五世代コンピュータプロジェクトは死なず!\(^O^)/☆☆☆

 最初は、シグマ計画の話だったのに、いつの間にか、第五世代コンピュータの話になりました。^^;

===
標題: これもベさん?
---
http://www11.ocn.ne.jp/~suiten/peke1.html
プロジェクト×(ペケ) -失敗者たち- 「Σ(シグマ)計画」
に出てくる藤本さんは、やっぱ、ベさん?

中村(show)

===
標題: Re: これもベさん?
---
経済産業省の役人をつかまえて

「Σ計画ってなあに?」

と聞いて、顔をしかめるのが旧通産省出身で、にやっとするのが
経産省になってからの入省、というのは本当か?

--
つばめどん

===
標題: Re: これもベさん?
---
ありゃま,そうです。これ,おれの本からの引用だわ(笑)。
ま,事実は事実なのでいいんですけど。
あと,オレは詳しくないんで書けないけど,「第五世代コン
ピュータ」とかいうのもあったよね,あれはどーなったんか
なぁ。誰かしりません?

べ@サンフランシスコ

===
標題: 第五世代コンピュータプロジェクトは死なず!\(^O^)/
---
 おお、ベさん、サンフランシスコか。つーことは、Appleの開発者会議だな。
 わざわざコメントに呼び出してすみませんです。

>あと,オレは詳しくないんで書けないけど,「第五世代コン
>ピュータ」とかいうのもあったよね,あれはどーなったんか
>なぁ。誰かしりません?

 おお、これは、書けということだな。
 何度か書いてるけど、おれの頭の中では、25年経って、Lisp, Prolog, 関数
型プログラミング、論理型プログラミング、AI, 知識表現、AIプログラミング
などが、わんさか懐かしさとともにやってきています。\(^O^)/
 それで、昨年くらいから仕事の合間にあれこれみたりしてるんですが、それ
でわかったことを、以前から、第五世代コンピュータプロジェクトの残したも
のがフリーソフトになってるよとか、いまでもKL1の後継言語としてKLICの開
発が続けられているよとか、そういうの紹介しようと思っていたんです。

 第五世代コンピュータプロジェクトについては、なんといっても、
http://www.jipdec.or.jp/archives/icot/ARCHIVE/HomePage-J.html
第五世代コンピュータプロジェクト・アーカイブス
(古いリンク切れしたURLは、http://www.icot.or.jp/ARCHIVE/)
に行ってください。
 なかなかに壮観です。これくらい資料があると、いまからでも全貌がわかる
だろう。これくらいちゃんと記録を残してあると、立派かつありがたいことで
す。
 ほかにも、
http://www.klic.org/software/klic/lang/lang.html
KLIC 講習会テキスト KL1 言語編
(古いリンク切れしたURLは、http://www.logos.t.u-tokyo.ac.jp/klic/software/klic/lang/lang.html)
http://www.ueda.info.waseda.ac.jp/~takagi/kl1/
けいえるわん
などをみてください。

 ぼくがこのICOTのサイトを発見したのは、偶然です。
 だって、ICOTなんてとっくに解散して、ネットにサイトなんかないだろうと
思っていて、探しもしなかったし、ICOTのサイトを発見したのも、論理型プロ
グラミングとか並列プログラミングとか、そういうのでググって見つけたわけ
じゃないんです。
 実は、バイオインフォマティクスでゲノム配列を調べるアルゴリズムやソフ
トを調べていて、
http://www.jipdec.or.jp/archives/icot/ARCHIVE/Museum/IFS/field-J.html
IFSの分野による分類
(古いリンク切れしたURLは、http://www.icot.or.jp/ARCHIVE/Museum/IFS/field-J.html)
の中にある、あるソフトに偶然、ぶちあたったのです。
 そのときの驚きを一言で表現するなら、

     「ICOTがまだあった!!」\(^O^)/

 KLICに興味がある人は、
http://www.klic.org/software/klic/index.ja.html
並列論理型言語処理系 KLIC のページ
をどうぞ。
 ここからリンクがある「KLIC 講習会テキスト KL1 言語編」は上記と同じ内
容みたいです。
 ぼくは例によって、ソフトをビルドもしてないし、畳水練、というより、テ
キストすらちゃんと読んでもいないけど、目次見るだけでわくわくしますね。

 つーことで、いろいろと批判はあっただろうし、マスコミの日の丸人工知能
万歳的な報道に白けたりもしたけど、シグマよりははるかにいいものを残して
いるといえるでしょう。
 そういえば、オムロンが作ったシグマワークステーション。某所でルータと
なって片隅で余生を送っていました。つーか、開発環境としては一度も使われ
ず、いきなりルータとしての余生だったようですが。\(^O^)/
 でも、まあ、ルータとして生きられただけ幸せだったのかも。^^;
 他のところにばらまかれたシグマワークステーションはもっと悲惨だった印
象があるので。^^;

中村(show)

===
標題: Re: 第五世代コンピュータプロジェクトは死なず!\(^O^)/
---
おお,ICOTはこんなページを作っていたんですね。
こりゃすごい,さっそくブックマークしました。

べ@昼休み

東京大停電2006年08月14日 08時57分25秒

ASAHIネット(http://www.asahi-net.or.jp)のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 東京、千葉、神奈川などで、いま、大停電なんですね。
 起きたばっかりで、テレビみて、びっくり。
 府中は大丈夫。
 都内は、電車も止まっているし、信号も消えている。
 エレベータに閉じ込められている人たちもいるらしい。
 東京電力にも、原因もわからないし、停電範囲もわからないという。
 一体、どうなっておるのだ。
 テロ? 宇宙人の仕業?^^;
 やっと休みがとれて、遊びに行こうと思ってたのに。

 日テレが一番早く詳しくやってますね。
 他はNHKを含めて、のんびりワイドショーやってる。^^;
 あ、いま、やっとフジがやりだした。

熱出て寝てました\(^O^)/2006年08月18日 23時04分21秒

ASAHIネット(http://www.asahi-net.or.jp)のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 月曜日、休みになったら東京大停電で遊びに行けず。
 火曜日、会社に行ったら熱が出始める。\(^O^)/
 水曜日、家で静養。

 休みになったら、熱が出て寝込むというのは、パターン化しましたね。^^;
 もう年だね。仕事の緊張が緩むと、すぐ病気だね。
 早く引退したいのに、これじゃ、引退したら、即死亡だね。\(^O^)/

形式仕様記述(フォーマルメソッド、Formal Methods)2006年08月19日 23時05分10秒

ASAHIネット(http://www.asahi-net.or.jp)のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 2006/08/06の「純粋関数型言語Concurrent Clean」のときに、
「この前、九大に教えに行ったとき、Formal Methodsの我が国の第一人者であ
る荒木啓二郎先生から直接お話を聞いて、仕入れてきました。それは、次の機
会に。」
と書いたけど、怠けと忙しさと体調不良で遅れに遅れてすみません。
 もうすぐ
LL Ring
なので、その準備もあって、いくらなんでもその前に書いておかないと最後に
あるように、荒木先生の第3回九州組込みソフトウェア研究会(QUEST)
での講演すら終わっちゃうので、簡単ながら書いておきます。

 形式仕様記述(フォーマルメソッド、Formal Methods)は、ぼくらが学生だっ
た25年前でも盛んにやられていたんですけど、当時は実用じゃなくて、論
文向けに小さなプログラムでああだ、こうだという感じだったんです。
 でも、いま、PerlやRubyといった、30年前遅い遅いといわれたLispより、30
倍も100倍も遅いスクリプト言語が実用になる世の中になったでしょ(*1)。

*1
 Lispが遅いといわれたのは30年前。いまのLispは、時にCに匹敵するくらい速い。
 Perlが30倍遅くて、Rubyが100倍遅いというのは、あくまで個人的感覚。

 だから、フォーマルメソッドも実用になるんじゃないかなと漠然と感じてい
たわけです。
 で、九大に呼んでもらったフォーマルメソッドの第一人者の荒木先生とお話
ししていたら、最近、すごいんだよという話になって、
http://techon.nikkeibp.co.jp/article/HONSHI/20051213/111568/
日経エレクトロニクス2005年12月19日号
特集「ソフトウェアは硬い」
の抜き刷りをもらいました。
 これは、素晴らしい。雑誌で形式仕様記述のことをここまで詳しく、かつ、
わかりやすく書いてあるのは、初めてだろう。書いたのは、進藤智則記者です。
非常にいい仕事ですね。バグをなくすことに興味のある人は、ぜひ、一読して
ください。
 最近、すごいというのは、ものすごい実例が出てきているからです。
 特集の中にも出てきますが、ソニーのフェリカネットワークスの事例がイン
パクトがありまくり。ここは、モバイルFeliCa、つまり、EdyとかSuicaとかお
サイフケータイなどをやっている会社です。
 ここが、それまで自然言語やUMLで仕様記述をやってきてバグがつぶせない
ので、形式仕様記述言語VDM++で形式仕様記述を実践して大きな成果を挙げた
のです。すごいのが、VDM++で10万行も書いてること。\(^O^)/
 これで、実装前、すなわち仕様の段階で350件ほどのバグを潰してます。
 フェリカの技術者たちは、数ヵ月でマスターしてここまで使ったらしいです。
 荒木先生によれば、「彼らは、たしかに優秀だし、大学と違ってビジネスで
大金がかかっていて、本気でやるからすごい」とのこと。
 ケータイだと、バグで回収騒ぎになると、ソニーや松下、たしか、100億円
くらい損失出したりしましたよね。極論するとバグ1個で100億円飛ぶんだか
ら、そりゃ、必死になりますよね。
 バグ1個で数億円飛ぶとなると、技術者にフォーマルメソッドを使うように
仕向けてもペイするかななどと思っていたんですが、もっと少額でもペイしそ
うな気もします。
 この前、XMLで有名な檜山さんがアンテナハウスに来てくれて、講演してく
れたんだけど、檜山さんによれば、100億円とか、数億円なんて巨額じゃなく
ても、小さなウェブショップのソフトを作ってるような世界じゃ、バグでショ
ップが止まって、日銭で70万円や80万円などの損害が出ると、その世界じゃ、
かなり大変。だから、フォーマルメソッドって、もっと少額でも、どんどん広
まったほうがいいんじゃないかと。
 つまり、フェリカの場合は組み込みで、バグが出たら回収が大変という世界
だけど、ウェブはウェブで365日24時間運用になってきてるから、止まるとや
っぱ大変ということ。
 全面的にネットワークに依存しつつある世界では、もう、バグは致命傷にな
りかねない。それなのに、理論的なやり方じゃなくて、行き当りばったりでア
ドホックなことばっかりやってシステム開発ってやられてますよね。特に若い
ITベンチャーなんて、理論なんか知ってる奴はいないし、体力と安くこき使う
人海戦術だけで乗り切る戦法だから、破綻は目にみえてるわけです。
 形式仕様記述の登場背景、現状、ケーススタディやらは、前記、特集を読ん
でください。

 前置きが長くなったけど、形式仕様記述の入門書として荒木先生と張先生の
入門教科書を紹介します。

http://www.amazon.co.jp/exec/obidos/ASIN/4274132633/showshotcorne-22/ref=nosim
荒木啓二郎、張漢明著「プログラム仕様記述論」
です。
 実はこの本、おれ、出版されたときに送ってもらって、去年のいまごろ、紹
介しているんです。
http://iiyu.asablo.jp/blog/2005/08/30/57720
荒木先生の形式仕様記述の教科書
をどうぞ。
 荒木先生たちが訳した
http://www.amazon.co.jp/exec/obidos/ASIN/4781907164/showshotcorne-22/ref=nosim
M.ヘネシー著「プログラミング言語の意味論入門」
も役立つかも。
 おれ、これ、たしか、当時、ゲラ、読ましてもらったんじゃないかな。ひょ
っとして、ゲラ、もらって帰ってきたかも。もし、そうだとしても、もう、ど
こにあるかわからんけど。^^;
 なお、この本、7月中旬に調べたとき、amazonのユーズドで12600円もして
いました。「184ページの本で、12600円はかなりのプレミアですね。^^;」と
荒木先生にメールしたくらい。今日(2006/08/19)現在は、2260円ですね。1万
円も安くなってる。\(^O^)/

 上記、教科書の内容は
http://dontaku.csce.kyushu-u.ac.jp/books/ProgramSpecification/
プログラム仕様記述論
でも公開されています。
 本と違って、公理や規則などポイントのみで、文章による説明はほとんどあ
りません。説明がほしいなら本でしょうね。逆にFlashのアニメーションを使
っているので動きがあってわかりやすい面はあります。特に部分的正当性の証
明は、Flashのアニメだとだんだん上に積みあがっていくので、本よりわかり
やすいと思います。
 だから、併用するのが一番ですね。
 その他
http://unit.aist.go.jp/cvs/tr-data/sympo/araki.pdf
システムモデル化と形式仕様記述
もどうぞ。参考文献が参考になるかも。

 荒木先生からは、ErlangとVDM++の話も伺ったんですが、その話というのは、
http://unit.aist.go.jp/cvs/tr-data/sympo/tokimatsu.pdf
「形式仕様記述言語VDM++による形式モデルの構築と関数型言語Erlang による
実行」
ですね。
 あと、コンピュータ将棋の話も教わって論文ちょっともらったんですが、こ
れはいつか暇があれば。

http://www.erlang.org/
Erlang言語

 で、ぼくが九大に行ったあと、SEA(ソフトウェア技術者協会)のシンポジウ
ムが熊本であったんです。
http://ss2006.kmt-iri.go.jp/SS2006-Call.txt
ソフトウェア・シンポジウム2006
2006年7月19日(水)~21日(金)
ウェルシティ熊本  http://welcity.net/
です。これをみてもらえれば、どういうことをやってるかはわかると思います。
 東京に戻ってすぐ、こういう紹介を書いていれば、熊本に話を聞きに行けた
人がいたかもしれないけど、ぼくが相変わらずトロくて、どうも、すみません。

 そして、これはもう形式仕様記述のことを書けと宇宙から言われているな
(爆)と思ったのが、7月下旬に出たばかりの日経サイエンス2006年9月号に、
「欠陥を見逃すな ソフトウエア設計検証ツール」と題して、仕様記述、設計
検証ツールの記事が出ていたこと。
 日経サイエンスのウェブに簡単な記事紹介があります。
http://www.nikkei-bookdirect.com/science/page/magazine/0609/software.html
欠陥を見逃すな ソフトウエア設計検証ツール
をどうぞ。
 書いているのは、MITのDaniel Jacksonです。
http://people.csail.mit.edu/dnj/
彼らが開発したAlloyというツールを紹介しています。
http://alloy.mit.edu/
 ZやVDMなどほかのツールも表で紹介してあります。

 今度、荒木先生が「第3回九州組込みソフトウェア研究会(QUEST)」
~高信頼性組込みソフトウェアについて~において、「形式手法に基づく高信
頼化組込みソフトウェア開発」という題目で講演されますね。短い時間なので
ほんの入門と思いますが。
http://www.isit.or.jp/
九州システム情報技術研究所(ISIT)
のウェブに行っても、まだ、案内が出てないみたい。どういうこと? 直接
ISITの担当じゃないってことなのか。ISITからのメールじゃ、2006/08/02に来
ているのに。だもんで、メール全文引用します。
 締め切りが8/23なのでほとんど余裕がないですが、まだ間に合うでしょう。

--- ここから ---
*********************************************************************

 「第3回九州組込みソフトウェア研究会(QUEST)」
  ~高信頼性組込みソフトウェアについて~


・日 時 平成18年8月30日(水) 講演会 15:00~17:55


                   交流会 18:00~19:30


・会 場 福岡システムLSI総合開発センター 2階 (会議室A/B)
      (福岡市早良区百道浜3丁目8番33号)
       


[主催者挨拶]  15:00~15:05 
      福田 晃
        九州大学大学院システム情報科学研究院(QUEST会長)


[招待講演]   15:05~16:05
     「宇宙機ソフトウェアの高信頼性化の現状と組込み分野への応用」


・講 師  片平 真史 氏 
         宇宙航空研究開発機構(JAXA)情報・計算工学センター


・内 容 
  宇宙分野のソフトウェア、特に人工衛星などの宇宙機に搭載する
 ソフトウェアの高信頼性化のために研究・利用されている技術を
 紹介するとともに、組込みソフトウェアへの応用について解説します。
  また、高信頼性のための設計技術や検証技術について事例を紹介すると
 ともに現在の技術適用時の注意点などを紹介いたします。


・プロフィール
  宇宙ステーション、ロケットなどの開発業務を得て、
  高信頼ソフトウェア開発保証及びソフトウェア安全性に関する業務に長年
従事。
  特に、プロセス改善、ソフトウェア独立検証及び妥当性確認(IV&V)、
  高信頼性RTOS開発に関する業務のチームリーダ。


  1987年     宇宙開発事業団(NASDA)入社
  1999年~2001年 マサチューセッツ工科大学 航空宇宙工学部 
  Complex Systems Research Lab(Prof. Nancy G. Leveson) 研究員・講師


[招待講演]   16:05~16:50
     「組込みソフトのテストについて」


・講 師  森 孝夫 氏
        三栄ハイテックス株式会社


・プロフィール
  元高校の数学教師という経歴を持つ、教育者型の組込みエンジニア。
  1996年、三栄ハイテックス(株)に入社。システム開発課に所属し、
  デバイス関連のソフトウェアテストを経験後、ソフトウェア、システム開

  に従事。一方で社内ソフトウェアの教育の立ち上げを推進、確立。
  現在は、プロセス改・ソフトウェア設計のコンサルティングに従事。

  SESSAME/TOPPERS会員
  情報処理学会正会員

・著 書 「組込みソフトウェア開発のための構造化モデリング」共著。



        <<< 休憩 >>>   16:50~17:05



[講 演] 17:05~17:30
     「Windows Embedded OSにおける高信頼化組込ソフトウェア開発」


・講 師  奥薗 啓朗 氏  
         安川情報システム(株) 組込コンポーネント事業本部


・プロフィール
  ハードウエア設計を経験したのち、ソフトウェア設計・開発に従事。
  一貫してハードウェア・ソフトウェアに関するEmbedded業務に携わる。
  現在、Microsoft社のEmbedded OSを中心とした、OS・デバイスドライバの
  ポーティング事業のマーケティング・営業管理に従事。


  1984年 東海大学工学部通信工学科卒業
  1984年 (株)日本デジタル研究所入社
  1988年 安川情報システム(株)入社


[講 演] 17:30~17:55
     「形式手法に基づく高信頼化組込みソフトウェア開発」


・講 師  荒木 啓二郎 氏  
         九州大学大学院システム情報科学研究院 教授


・プロフィール
  1978年 九州大学大学院修士課程修了
  1982年 工学博士(九州大学)
  1985年 訪問研究員(アメリカ合衆国イリノイ大学)
  1989年 文部省在外研究員(ドイツ連邦共和国パッサウ大学)
  1993年 奈良先端科学技術大学院大学 情報科学研究科教授
  1996年 九州大学大学院システム情報科学研究科情報工学専攻教授
  2000年 九州大学大学院システム情報科学研究院情報工学部門教授
  2004年~九州大学附属図書館副館長(兼)
  現在に至る


[交流会] 18:00~19:30
福岡システムLSI総合開発センター 4階 (交流サロン)

・対象者  どなたでもご参加いただけます。


・参加費  講演会参加費  無 料
     (ただし、交流会参加の方のみ2,000円(領収書を発行します)

      ISITの賛助会員の方は無料です。
    (http://www.isit.or.jp/kaiin.html 賛助会員一覧でご確認くださ
い)


・定 員  100名程度


・主 催  九州組込みソフトウェア研究会(QUEST)
      情報処理学会九州支部
      (情報処理学会九州支部の特別事業として行います)


・共 催  (財)九州システム情報技術研究所(ISIT)


・後 援  九州経済産業局(予定)
(財) 福岡県産業・科学技術振興財団(ふくおかIST)
      福岡市経済振興局産業政策部新産業課
(社) 組込みシステム技術協会九州支部
      電波新聞社


・申込み締切日  8月23日(水)


・申込方法 下記にお名前等をご記入のうえ、
       E-mail(koryu@isit.or.jp 宛)等でご返送ください。
       すべてのお申込みに対しご返事いたします。


  なお、過去にISITが開催した定期交流会・技術セミナー等に
  申込まれている方で、肩書き等の変更がない方は、企業・団体名、
  氏名のみで結構です。
----------------------------------------------------------------
 「第3回九州組込みソフトウェア研究会(QUEST)」
    ~高信頼性組込みソフトウェアについて~

申 込 先 E-mail to:koryu@isit.or.jp
開催日時 平成18年8月30日(水) 講演会 15:00~19:30

企業・団体名 :
部課・役職名 :
氏 名    :
郵便番号   :
住 所    :
TEL番号    :
FAX番号    :
E-mailアドレス:
※懇親会   :  出席 ・ 欠席 (いずれかを削除願います)
-----------------------------------------------------------------
【個人情報の利用目的】
  今後、(財)九州システム情報技術研究所が催すイベント等に関する情報

ご案内以外の目的で利用することはありません。
  なお、今後のご案内に関して、いずれかを削除願います。
     ( 必要 ・ 不要 )

 *交  通

・詳細はホームページのアクセス&地図をご覧ください。
 アクセス:下記URL参照 (福岡システムLSI総合開発センター)
         http://www.ist.or.jp/lsi/pg03_01.html

・申込み・問合せ先
  〒814-0001 福岡市早良区百道浜2丁目1-22-707
  (財)九州システム情報技術研究所 事業部 有吉 / 田中 / 牧野
  TEL  : 092-852-3451 
  FAX  : 092-852-3455
  E-mail: koryu@isit.or.jp
  ホームページ:http://www.isit.or.jp
--- ここまで ---

 またしても直前での案内になって申し訳ないけど、熊本のシンポジウムみた
いに、終わってから案内してないので、許してください。^^;
 ISITのウェブ、案内を探してあれこれやってたら、オープニングイベントで
ぼくが話したことが記録されてますね。
http://www.isit.or.jp/eventinf.html
にある
http://www.isit.or.jp/eventinf/open.html
合同オープニングイベントのご報告
です。平成8年6月10日だから、もう10年前なんだ。所属がまだソフトヴ
ィジョンだし。
 ほんと人生あっという間。
 いま、若い人。ほんと若いうちに必死になれること見つけて、悔いのないよ
うに必死になったほうがいいよ。
 あっという間に、おれみたいに、もう人生終わっちゃったになるよ。\(^O^)/
 技術者としては、ウェブ2.0なんて、腐れ頭のチンポとマンコとケツの穴が
騒いでるだけのウンコなことに時間を使うくらいなら、形式仕様記述を学んだ
ほうが、長く使えるものだし、スキルも上がるし、1兆倍いいです。
 だって、人間だもの。\(^O^)/

トラックバック閉鎖しました2006年08月20日 00時18分07秒

ASAHIネット(http://www.asahi-net.or.jp)のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 ブログのほう、これまでもトラックバックスパムがけっこうありましたが、
この数日、1日100個スパムが来るようになったので、トラックバックを閉鎖
しました。
 あしからず、ご了承ください。

 なんかね、外人さんから、諺みたいなトラックバックが何個もついてるの。
 ASAHIネットのブログって、ブログにスパムブロックつけてくれないのかな。
 草野君が動けないと、だめなんだろうか。
 ブログに広告を入れるようにする件も、どうなったんだろう。
 ブログ続けるなら、前からもってるlivedoorのブログに引っ越すか。
 ブログ閉鎖して、昔ながらのウェブだけにするか。
 そういえば、Mixiも何にもやってないもんね。
 「Mixiは養鶏場」というタイトルで書こうと思ってそのままだな。

TRONWARE 100号「TRONプロジェクト 回顧と展望」2006年08月22日 08時40分49秒

ASAHIネット(http://www.asahi-net.or.jp)のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 たまたま週末本屋でTRONWARE 100号が出ているのを発見。
 「TRONプロジェクト 回顧と展望」と題して、TRONのこれまでをすべてまと
めてあります。
 付録DVDは、TRONWAREの全バックナンバー、貴重な論文収録です。
 まさに永久保存版。ソッコーで買いました。

 眺めていると懐かしい。
 以前、どこかの雑誌に書いたと思うが、初めて坂村健さんを生で見たのは、
上京してすぐ。
 調布の電機通信大学で情報処理学会の全国大会か電気通信学会の学会だった
と思うけど、坂村さん自ら、発表していて、ウケを狙ってスベったり、思わぬ
ところでウケたり、なかなか面白かった。

 いまはユビキタスであれこれ実証実験やってるし、この前、ケーブルテレビ
の番組で、板橋だったと思うが、商店街で実験している模様が放送されてまし
た。
 プロジェクトは22年目に突入だが、坂村さん、まだまだ元気いっぱいだね。
ビル・ゲイツが引退するのとは対照的。
 ゲイツの引退は、MS(Microsoft, マイクロソフト)が、Google(グーグル)に
代表されるネット時代に対応できなかった象徴のように思えるね。
 Googleが提供するAPIにみんな盲目的に依存していくのは、問題だと思うけ
どね。