おめぇら、形式的仕様記述について知ってる事を書け

形式的仕様記述の有効性について、語るスレです。

プログラムやプロトコルの仕様の、
フォーマルな記述方法っていくつかありますが、
どれくらい有効なんでしょうか？

形式的仕様記述を有効活用するには、
どんな知識が必要なんでしょうか？

おめぇーら、知っていることを書け！

２げっとずざー

VHDLについて誰か教えてください

BNF

Z

LOTOS

おめぇーら、単語だけじゃなくて、、、

意味とかポインターとかも書いておいて下さい。

VHDLのエミュレータのちょこっとした説明
http://mentai.2ch.net/test/read.cgi/sim/981553632/

char*

料理は愛情！
技術は経験！

スタジオにお返ししま〜す！

ちゃんと使えるドメイン（仕様が形式化でき，かつ仕様が満たすべき特性も形式化
できるような）では強力．もちろんコードが仕様を満たしていることも検証しやす
いような言語なら最強．

こういうスレを待っていた！
で、Zってなによ＞５

Zは仕様記述言語だよ

Ｚ　仕様記述言語
http://saeki-www.cs.titech.ac.jp/~ugai/Z/z-faq.html
こんくらいしか見つかんなかった。

禁断のぜっと〜、ってなんだっけ？

しらんわいｗ

(´_｀) .｡oＯ(やっとこさ仕事場が静かになったので、
　　　　　　　「仕様の『抜け』検出」について考察してマウス...)

http://www.zuser.org/

つーかUMLじゃだめなのか？

あっちに書いたんですが...(こぴぺ
http://mentai.2ch.net/test/read.cgi/infosys/1011618439/83

83：非決定性名無しさん ：02/02/13 09:28
基礎となる数学理論、というのはよく分かりませんが、
・状態遷移　　　　ペトリネットとかオートマトンとの対比
・仕様記述・検証　意味論の記述に集合論とか代数の概念を援用
とかしているのでしょうか？

＃最近のUML拡張で、OCL (Object Constraint Language)
＃による事前条件・事後条件の記述機能が追加され、
＃　http://www.amazon.co.jp/exec/obidos/ASIN/0201379406/ref=sr_aps_d_1_1/250-4956143-4769858
＃状態遷移の検証等が可能らしいですが、
＃きちんとした仕様記述・検証には 言語Z を使用するという方もおられるそうです。
＃
＃「UMLの意味論」をきちんと扱おうとすると、別の形式的仕様記述が必要そうですね。

>>18を見たときに誰かが僕の頭の中で「2げっとzuser」とささやきました。

cafeobjは？

>>21
それ、妖怪「空耳」だ、うちにもよく来るよ。

というかこのスレ立てたの情死す板のカレースレの人じゃんｗ

>>22
國産品を愛用しませう！

カへおーびーじぇー、すんごく興味あります。
特にコンポーネント関係の研究してる辺り。

2月末の報告会聞きいきますんで、もし見てたらよろしくお願い致しまし。

隠蔽代数を勉強しておくとよいかも >>26

>>20
OCLは何で現場で使われないんだ？
数学に疎いエンジニアの為に作った
って仕様書に書いてあるのに、現場で
使ってるのなんてみたことないぞ

*.exeをだぶるくりっく
うぃんどうがでる
ぼたんをおす
しゅうりょう

>>28
処理系がないからでそ

OBJ, OBJ3, CafeOBJ どうちがうんだ？
わかってる、わかってるよ。論文読めってんだろ...そりゃわかってんだけどさ。

>>28, >>30
サブセットっぽいけど、処理系ならあるでそ
(ArgoUMLのこぴーらいとからこぴぺ)
　 Frank Finger's (TU-Dresden) OCL-Compiler (dresden-ocl.sourceforge.net)

アプリケーションはこのあたり。
　・ArgoUML
　・EJB 2.0 EQL

モデルチェッキングの話が出てこないな。

ここだけの話、使えるＦＭって今はモデルチェッキング。
やっぱ、オートマチックに動かないとね。

こないだ某所で話したＮさんはSPINつかってるらしい。

「関係者さんと話すＮさん」にビビってしまった厨房な私...

このあたりっすか？
　　http://www.ipsj.or.jp/members/SIGNotes/Jpn/09/2000/129/article014.html

「EJB仕様書から仕様記述を作り検証する」って凄そうなんですけど、、、
アーキテクチャ云々するほど洗練度の高くない仕事でも使えますか？

>>34

>>33は、「Ｎさんがある会合でお話をした」ってことです。
私は直接お話したことはありませ〜ん

http://www.shinsahara.com/www/sigfm/

お話の件ですが基本的には有限状態機械として表現できれば大丈夫かと。

はぁー、「有限状態機械(FSM)」っすか。

明示的にあるいは本質的に、FSMとして表現されていない部分は、
仕様検証の対象外になるんでしょーか。疑問ばっかりですんません。

>>36

まず、明示されてないものはチェックできないでしょうね。

また、有限状態機械では表せない場合には、
今のモデルチェッキングを超える方法が
必要でしょうね。

興味あるのであげ
このスレが伸びてくれれば2chも捨てたものではない

とか言ってみる

>>38
2ch見てないで論文読み漁る方が
はるかに早いと思います。
もし知識があるならご自身で
なにか書き込んでみてはいかが
でしょうか？

形式的仕様記述という観点で先行しているのは HDL ではないでしょうか
所詮，ソフトはライフサイクルが短くて，品質には甘いので...

そういえば，Haskell 板で苦労している monad は，プログラム記述と，
仕様記述の中間のような気がしますね

>>37
元の系が有限状態でなくても、抽象解釈して有限状態として検査するのが
「今のモデルチェッキング」の流行りでは？といってみるテスト。

ペトリネットの検証系ってどんなのがある？

以前フォーマルメソッドの講演会に参加したことあるけど
正直言って難しかった．
こんなに数学寄りの話だったなんて知らなかったよ．

>>42 ペトリネットの検証系ってどんなのがある？

漏れも、その件引っかかっています。
詳細わすれちまったんですけど、
実際によく目にするプログラムは、
有限状態機械より、ペトリネットに近いみたいですんで、
それをどうやって検証するのか？
(FSMに翻訳 or ペトリネット向けの検証系)
興味あります。

でも、聞いてばかりでは自分の理解も進まないようですので(笑
自分が勉強してから解くべき課題にしておこうかな？

>>41

それって例えばAlloyとか？

昨日は形式仕様記述のお話を聞けて、
今日は Amazonから Catalysis本と OCL本が届いたので、
記念age

Alloy : MIT方面で開発されたものでしょうか？
　　　　もしかすると、ソフトウェア工学のゼミでは、
　　　　普通に扱う題目なんでしょうか？>>非FSMのモデルチェッキング
　　　　(漏れは専門外)

SQL:　　形式仕様記述に近いものだ、とお聞きしますが、
　　　　それはどのような意味でしょうか？(制約論理関連？)
　　　　＃EJB2.0でも、問合せ言語EQLとしてOCLを使うそうですが...

＃揚がってないし...

>>46

AlloyはMITのDaniel Jackson等によるものですね。
有限モデルの存在をチェックするものと認識してます。
（私も最近知ったので、詳しいことは分かりませんが）

非FSMのモデルチェッキングは今は研究段階だと思います。

VDMTools は結構使える。
http://www.ifad.dk/Products/vdmtools.htm

age

>>20
国内でどのくらい使用例あるのかな？Ｚ
大学の時の先生がＺの専門家だったんだけど、社会に出て一回も聞いたことないよ

あげ

なんか今日は、UML祭りでー、
OCLでアクション・モデル記述してる、MDA製品ベンダーの人とか、
リアルタイム組込システムでFormalMethodを導入してる、UMLの偉い人とか、
なんかスゴイ人ばっかり見たんで記念アゲ。

ホーアCSP理論も噛んでる？
Eiffelの表明なんかも「仕様記述」と考えていい？

＞ホーアCSP理論も噛んでる？
ホーアのCSPは、プロセス代数的仕様記述で、
INMOSトランスピュータ近辺の応用例が有名みたい。(例が古すぎ？)

＞Eiffelの表明なんかも「仕様記述」と考えていい？
どうなんでしょ？「プログラム検証に役立つ一機能」かなー。
Eiffelで仕様記述するって聞かないし、
形式的手法の一応用例かと、漏れは思うのですが...

手元の本に、形式的仕様記述の分類があったので、
要約してコピペしてみます。

＃でも、モデルチェッキングとか、
＃Alloyとか OCLも載ってないんだよなー。古いのかなー
　------------------------------------------------------------
　Z,VDM:
　　　「モデル・ベース」の仕様記述
　　　　集合論とか使って、抽象モデルを記述
　OBJ,PLUSS,LARCH,FOOPS:
　　　「代数的手法」を使った仕様記述
　　　　等式論理を使い、より抽象度の高い記述をする。
　CSP,CCS,π計算:
　　　　プロセス代数。代数的アプローチによる並列性の記述。
　　　　CSPの応用事例：OCCAM言語、INMOS TransputerのFPU開発
　LOTOS,OBJSA,RSL:
　　　　「プロセス代数」系のハイブリッド言語。

　Object-Z,VDM++等:
　　　　「モデル・ベース」形式手法を、
　　　　オブジェクト指向技術へ適用するための仕様記述言語。
　　　　OOA手法の SyntropyではZ,　FusionではVDM、を使用していた...
　------------------------------------------------------------

（ θ○θ；）

(^Д^)ｹﾞﾗ

「形式的仕様記述」って、こんなやつ↓のこと？


まだ若かりし、小学生の頃
↓
母にポテチをねだる
↓
却下される
↓
ぐれる
↓
極道の世界へ
↓
数年後
↓
母から一袋のポテチが届く
↓
兄弟から母が死んだと電話が入る
↓
母の遺言から母の真意を知る
↓
「あの子は体が弱いからあまりジャンクフードは食べさせたくない」
↓
泣く
↓
足を洗う
↓
ポテチを食う
↓
(ﾟдﾟ)ｳﾏｰ

Lyeeが入ってねーじゃん（ｗ

なーんだ、ここにも春厨か。
>>60 なにそれ？変な奴

結局2ちゃんねるは、
何処へいっても春厨だらけ。

ここはどうせ漏れのメモ用紙みたいなもんだから、
なんか間違いあったら適当に直しといてね。

んじゃ

日本語で読めるものはゼロ？

誤爆？

生真面目です

形式仕様記述の前に読む本：
　「プログラム言語理論への招待--正しいソフトウェアを書くために」,Bartrand Meyer,二木厚吉(監訳),酒匂寛(翻訳)
　http://www.amazon.co.jp/exec/obidos/ASIN/4756103170/qid%3D1017229588/249-9598832-5139562
ってのしか知らない。中身は、プログラム言語意味論。

>>67
それはプルグラム言語の話ではなくて？
おれはもっと要求定義を形式的にやるような学問があるのかと
思ってたけど、ちゃいますか？

要求仕様工学ってのもあるみたいっすね。
CMM方面とか、ユースケース駆動方面で、
その重要性が認識され始めたけど、
まだ分析・設計手法ほどメジャーになっていないみたい...

>>59 ってユースケース記述？

なんでプログラマって形式って言葉を馬鹿にするですかね。
むしろ萌え萌えな感情を掻き立てるものであるべきと思うですが。

>>70
なんででしょうね？
漏れは昔から、計算論とか意味論とか萌え萌えなんで、
Formalizmって言葉に違和感はないけど。

かくいう漏れも、UMLは便利だと思って前からよく使ってたけど、
「開発方法論」とか「形式仕様記述」の方はつい最近まで、
「(自分の守備範囲ではどーせ)使いものにならん」とか
勝手に決め込んで、封印してたんだけど。


あと、答え忘れてた、、、
>>68　>>67の本は、
プログラム言語意味論の形式的記述≒形式仕様記述って立場で、
意味論の勉強しといてくれよって目的で、翻訳されたんだと思う。

前書きに酒匂＠SRAさんが、そんなような事書いてた。

>>71(56)
日々の仕事においてやっている作業の類似性になんとなく
気が付くものの、それをどう統一した方法で扱えばいいのかを
考えると全然分からなくなる。そういうのは多くの人が思ってる
ことなんじゃないかな。かといって今のままでいいとはとても
思えない。反復的開発なんてやっている人なら分かると思うが
手探りでなんらかの答えを導きましょうという考えには変りない。
個々人の経験に大きく左右されるようなもの。危険です。

おれも上のリストからどれか勉強します。

＞反復的開発なんてやっている人なら分かると思うが
＞手探りでなんらかの答えを導きましょうという考えには変りない

まずは軽〜く、一通りの処理が流れるように作って、
仕様変更や設計変更の余地を残しておき、
それからマターリと細部を作るという感じではないかなー。

もっと殺伐としてるべき！

OBJをWebで色々と見てるけどさっぱり分からん

漏れはFDT専門だが自己批判的に言わせてもらうと，

まず､FDTはごくごく限られた単純な（綺麗な）ターゲットでないと使えない。
実用アプリだと形式仕様を書くほうが実際のコーディング以上に大変。間違えるし。
たとえばWindowsをFDTで設計すりゃ良さそうなもんだが､そんなことはできない。
ついでながら､検証しか目に入ってない研究者が気がつかないのは､現場の誰が形式仕様
記述と検証をするのかということ。作るだけでも精一杯なのに､そんな余剰人員はおらん。

次に､FDTの研究が世の中のアプリを主導しているのでは決してなくて､アプリが常に先行して
先端アプリを検証するためにFDTが研究されるという後追いになるから､研究の目処がついた
ころには､そのFDT手法で検証できるアプリはすごい時代遅れのものになってしまう。
結果的に一番検証したいものが検証できない。

もちろんFDTを全否定するわけではないが（自分の首がしまるしな）､FDT研究者の多くは
自分で実用プログラムを書いた経験がほとんどなく､FDTの理論世界に閉じこもっている。
それが一番の問題。

>>76
Executable UML とか MDA みたいな技術については
どう捉えられているんでしょうか？

OMGとか Rational は、UML+Action記述を、
第一級のプログラミング言語に仕立て上げたがっているようですが…

少しスレの趣旨とは違うけどこれはどうでしょう？
http://pvs.csl.sri.com/
使ってる人いますか？

ごめんなさい、関数言語スレのどっかで名前が挙がってて、
興味はあるけれど、まだホームページちらっと眺めただけ。

高いの？便利？特徴は？

(勝手に)義兄弟スレ【Verilog,VHDL等のＨＷ記述言語のシミュレータ 】
　http://mentai.2ch.net/test/read.cgi/sim/981553632/
＃もしかして、ExecutableUMLって、
＃ハードウェア記述言語とかの影響下から出てきたのかなー？
＃あっちの分野は、それなりに実用に使われているよ、ね？

プロセス代数に興味を持ったけど今のところ日本語で
読めるものは皆無ですよね。やっぱり英語の本を買うしかないかな？
http://www.amazon.co.jp/exec/obidos/search-handle-url/index=books-us&rank=+salesrank&field-keywords=process%20algebra&bq=1/ref=sr_aps_alleb__/249-9422025-1082728
これらの中でお勧めの一冊とかあれば教えてください。

>>80
3. Handbook of Process Algebra が一冊あれば事足りる．高いけど．
初心者なら 2. Introduction to Process Algebra が読みやすいです．

>>81
うぉ、どうもありがとう。ところで、
こういうの大学の授業にもぐりこんで勉強したけど
都内でどこかいいところ知りませんか？

勉強したいんだけど　　でした、ｽﾏｿ

>>79
漏れはハード屋だが､形式仕様記述なんかしてるハード屋は見たことないよ。
HDLは設計とシミュレーションのために使うもの。
まあ何をもって仕様と言うかにもよるけど､仕様記述を目的にHDLを使うハード屋はいないよ。

>>84
いや、もふこのスレは形式仕様記述なんてものは対象に入ってないでしょ（ｗ。
プログラム仕様の形式記述というところを理解するだけで精一杯というか。

>>84
>漏れはハード屋だが､形式仕様記述なんかしてるハード屋は見たことないよ。
Intelがやってたはず。どっかの学会でしゃべってた。
Pentiumとかのバグでこりたらしい(w

>>86
あー分かった､それは仕様記述のことじゃなくて､モデルチェッキングを使った機能検証だね。
でもモデルチェッキングもほとんど普及してないよ。
ハード界で一番普及してるのは等価性チェック。CADの入力と出力の等価性をチェックするため。

どっちにしても大LSIメーカでやっとあるかなというレベルだから､一般に普及してるなんてとてもとても。

>>85 あいたたた、本業がどうもそっちの方向にいかなくて、
　放置状態でいたら、痛い所をつかれてしまった。

>>85,>>87
「形式仕様記述」と「プログラム言語の仕様記述」
「形式仕様記述」と「モデルチェッキングを使った機能検証」と「等価性チェック」
の違いなど簡単に説明していただけると助かりますです、はぃー

http://www.brics.dk/mona/

(・∀・) MONAﾓﾅｰ？

>>82
学部の授業で形式仕様を扱っている大学という意味ですか？
ちょっと聞いたことがないですね．都内に限らず．

ある関数の処理内容を形式的に記述することなんて
できないものかなぁ？インターフェイスだけじゃ動作の
互換性なんて、実際に動かすまで分からんし。

ホーア／フロイト論理はどうよ？　preconditionやらpostconditionやら
invariant conditionやら、すべて記述するのはｶﾅｰﾘ面倒だが。

>>82>>91
プロセス計算とかホーア論理なら、前は東大の理学部情報科学科で学部の３年生や４年生に
教えてたけど、まだやってるのかなあ？　もちろんみんな爆死してたけど…

漏れはおおざっぱにいって
「形式仕様記述」⊃「プログラム言語の仕様記述」
「形式仕様記述」⊃「モデルチェッキングを使った機能検証」⊃「等価性チェック」
だと思った。モデル検査をするには満たすべき性質（＝仕様）を与えないといけないし、
等価性チェックをするにも等価になるべき相手（＝仕様）を与えないといけないし。
87は何か特定の種類の「仕様記述」が念頭にあったと思われ。

>>93
実際にプログラム組んでテストするより難しいのは、
だめだってことだよね。しかも習得に異様に時間がかかる。

数学としてはどんな分野の知識が必要になるんでしょうか？

>>96
習得が大変（つーか普通のプログラマには無理？）なのは事実だと思う。

ただ「実際にプログラム組んでテスト」だと、あくまで有限（一部）の
入力についてしかテストできないけど、ホーア論理とかなら無限（全部）の
入力について検証できる。

だから、「実際にテストするよりも難しい」と直ちに
「形式的仕様検証 ＜＜＜ 実際にテスト」といえるわけでもない。

あと、プログラムの完全な仕様じゃないけど、配列の添え字とか例外処理とか
一部だけ検証するなら、http://research.compaq.com/SRC/esc/みたいな
もっと「お手軽」なアプローチもある。

>>97
数学というか記号論理学と思われ。∀とか∃とか∧とか∨とか¬とか、
そういうの（笑）。

∀といってもこういうの↓じゃないぞ

(・∀・)

>>98
最近それに見えてしまって困ってるんです（まじ深刻

(・∀・)　(・∃・)　(・∧・)　(・∨・)

(゜¬゜)

>>101-102
やめてくれ、これからそういう記号を扱う講義があるんだから…（笑）

��(゜Д゜

(・∧・)混同イクナイ

>>101 >>102
面白すぎ。けっこう使えるような気がする（笑

>>88 >>95
しばらく見てなかったんで遅レススマソ。

なんにせよ､仕様って何のことなの？､ってのをはっきりさせないと話が混乱するよね。
とくにrefinementする場合は､ある段階の実装が次の仕様になったりするんで､何が仕様で
何が実装かは相対的なものだし。
形式言語とプログラミング言語の違いって何？､ってのもある。プログラミング言語だって
考えようによっては形式言語の一種（曖昧な自然言語ではなく､意味がそれなりに一意に
定まって論理との対応も可能な言語という意味合いで）だから。

閑話休題。
それで､言語として何を使うかは別として､｢仕様｣としては関数や回路コンポーネントの
入出力関係に関する何らかの記述､｢実装｣としては関数や回路のコーディングしたものを
指す､という定義のもとで､
｢仕様記述｣はあくまで仕様を形式言語で書く行為､｢モデルチェッキングや等価性｣は仕様
と実装の関係を検証する行為と漏れは認識しております。

モデルチェッキングは仕様として実装の動的性質（の一部ないし全部）が与えられたとき､
それが実装において成立するかを調べること（論理学的には別の意味合いがあるが､ちょ
っとそれは置いといて）。等価性検証は､仕様としてはrefinement前の中間実装（たとえば
ハードならRTL）がおもな対象で､その動作とrefinementされた実装（たとえばハードなら
ネットリスト）の動作が同じかを調べること。こちらは静的手法でかなり調べられる。
別種の議論として､仕様それ自体があっているかというのも問題だけど､現場的にはそこま
で形式手法でやるのは手が回ってない。

まあ､単に仕様を書くだけではなくて､書いた仕様から実装が導出できるなり､形式検証が
できるなりのメリットがないと､わざわざ形式仕様記述する意味は少ないかと。
あと､数学の関数みたいな演算処理なら仕様として入出力定義を明確にかけるし論理との
相性もいいけど､世の中のソフトやハードの大半ってそういうものじゃなくて､何かのプロ
トコルとかプロセス制御とかシーケンス制御が多いからねえ。そういうのだと､形式仕様
を精密に書いているうちにコーディングとあまり変わらなくなってしまって､それなら最
初からコーディングすればいいじゃん､となってしまう事情もあるよ。

(・∀・) 不死鳥のようにage (・∃・)

CやC++のある言語は静的な検証はどこまで可能なのかしら？
形式仕様の話とは無関係ですまそ。

無関係でもあるまい。もうすぐPLDI 2002で発表されるようだが、

> Flow-Sensitive Type Qualifiers
> Jeffrey S. Foster, Tachio Terauchi, Alex Aiken (University of California at Berkeley, USA)

なんかどうよ？　型システムに基づく静的検証で、Linuxカーネルのバグをいくつか見つけたらしいぞ。
ロックまわりとか。検索したらwebにも論文があったような。なんか定式化が微妙に変だったけど…
（Aikenがちゃんとチェックしなかったのか？）

あ、俺、寺内って人じゃないからね。自作自演じゃないよ。(w
この人、どういう人なんだろ。聞いたことがなかったんだけど。
PLDIに行けば会えるんだろうけど、うちにそんな金はねえ…

>>109
ああ、俺、それ聞いたよ。
特にbuffer over runなどの境界条件に起因するバグを見つけられるそうな。

http://sunshine.cs.uni-dortmund.de/~knoop/PLDI2002/pldi2002_main.html
これってどんな団体なんですか？

>>112
ACMっていうコンピュータサイエンスの国際学術団体の中の、
SIGPLANっていうプログラミング言語の専門研究部会が主催してる、
学術会議の一つ。毎年一回、これぐらいの時期に開催される。

http://citeseer.nj.nec.com/impact.html

なんかを見ても、レベルは高い。
論文の採択率はいつも20%ぐらい（＝5本に1本しか通らない）。
日本からだと、IBMの基礎研がJavaの関係でよく頑張ってるような気がする。

保守sage
>>109
Linuxのバグを見つけるなんてすごいね。頭のいい人はいるもんだな。
おれも興味ある。勉強してみようかな。でも自分で作ったカーネルの
デバッグが出来ないとかいう頭の悪そうな動機じゃだめかもね（ﾜﾗ

定理証明系やってる、はぎゃー先生が、
>>114みたいな動機を思いっきりこき下ろした「つかみ」書いてたっけ

NHKの教育番組は最高だがね〜
あどけない女の子がいっぱいだがね〜
興奮してローソクが垂れちゃっただがね〜
汚しちゃっただがね〜、ヒヒヒ・・・

漫画、読んだ事ないので文章が間違ってたら
すんまそん。
http://www.h4.dion.ne.jp/~k.seed/index.html

age

>>116を形式化してください

>>116 のバグをモデルチェッカーで撲滅してくらさい

"SEAMAIL" 2002/5 に、
FormalApproachの中心人物で VDMの開発者でもある
Bjorner先生の論文が載っていたのであげ。

>>1 はどうした？
少しは勉強が進んだかね？

申し訳ない。
ガッコに居た時からの懸案なのですが、進んでません。
「証明的プログラミング」とか「構成的プログラミング」には興味があったのだけど、
形式仕様記述をやるモチベーションが足りなくて...。

最近Lyee上司は、KMとか言い出しちゃってて、
＃それはそれで「ソフトウェア再利用」「ソフトウェア部品」よりは幾分ﾏｼなんだけど、
KMの限界とか突破口とかを見極めようと四苦八苦しているのが、現状です。

あ、あと >>120 は良さそげなので、きちんと読んだ上で ﾈﾀにしたいと思います(ｦｲｦｲ

最近形式仕様の勉強少しはじめた者です。
ビジネス系の開発現場で、OCL使っている方いますか？
実開発でiContractとか使いたいのですが、使った経験のある方とかいます？なんかハマりそうなのですが。

保守あげ

ほしゅ

保守といえば、形式仕様を保守フェーズで有効に利用する方法とかって、何かいい文献ある？

なんか形式仕様の話は大抵がプログラムの構成まで、せいぜいバグ取りまでで、
その後に控えてる長〜い保守についてはあまり語られてないような気がするのだが。

ほっしゅほっしゅぼっしゅぼっしゅしゅっぽしゅっぽしゅっぽっぽ

>>81
Handbook of Process Algebraを注文しましたー。
でもひとりで勉強出来るか心配です。
なにかお勧めのニュースグループなんかはありますか？

>67 プログラム言語理論への招待

確かに仕様記述に入門する前に、formalの世界の基礎となるいくつかの事項を学ぶことができる本です。
一方で誤りが非常に多い本です。原書からしてそうですし、翻訳にも多数の問題点を発見しました。
具体的には以下のページをご参照ください。
　ttp://katsu.watanabe.name/review/intro_theory.txt

この本は、徐々に積み重ねていったことを、クライマックスとしてハノイの塔のプログラムの正しさの証明で
花開かせる構成とみてとれます。ところが、なんとそのクライマックスの証明が完全な誤りなのです。
真面目な学習者ほどがっかりするのではないかと心配です。その一方で、誤りに気をつけてさえ読めば、
クライマックスまで話の筋が見えやすいので面白く基礎が学べるんじゃないかと思います。

訳者の酒匂寛さんは、訳本の出版当時私の直属の上司だったのですが、
　「Knuthっぽく、一箇所間違い見つけるごとに10円出そうか？」なんて言っていました。
上のページをまとめたあとで、「あの10円という話は本当ですかぁ？」とツツいてみたら、
本当に10円*約300箇所=三千なにがし円を下さいました。一箇所ごとに倍という話に
しておけば、2^300だから、えーと...新しいノートパソコンとかが買えたかな。

>>130
神ｷﾀｰｰｰｰｰｰｰｰｰｰｰｰｰｰｰｰｰｰ!!!!
この本は間違いが多いので、代替としてお勧めできるような本って
ありますか?

PVSバージョン3のβが出てます。
http://pvs.csl.sri.com/
関係者というわけじゃないけど、
最近使い始めたので、密かに宣伝。。。

保全上げ

http://shemesh.larc.nasa.gov/fm/fm-humor.html

あげついでに教えてほしいんだけど、
ここのみなさんはどうやって勉強してるの？
それとも大学に残ってるような人がこのスレに
書き込んでたとか？

どうも取っ掛かりがつかめなくてねえ。
上に書いてあるPVS3.0をemacsにインストール
してみたけど、これ慣れるまでに1,2ヶ月ぐらい
かかりそう。サイトにもまともに使えるように
なるのに半年とか書いてあるし。。。

PVSの前にもっと理論について詳しくならないと
だめだなあと思って、>>130さんの言っている
プログラミング言語理論への招待を再び読み始めました。
初等数学、抽象構文、形式意味論入門、λという5章までを
なんとか理解しようと何回も読んで問題解いたりしてます。
本を半分にぶっちぎって仕事中も読んでます（藁

ところでこれの演習問題の模範解答ってどこかに
ないかな？ちまちま生成規則を書いたりしてるのは
いいんだけど、どうもあってるかどうか自信無し…
海外のサイトでもいいのでもしあれば教えてください。
自分でも探したのですが、見当たりませんでした。
またはこれに似たような本で大学のテキストとして
使われている（答えも公開されている）ようなものが
あればおしえてください。

>>136
和書だと岩波『計算モデルの基礎理論』とか共立『プログラム意味論』とか。

>>137
それって演習問題とかついてます？
章末の問題ってアホウのしりを叩いて
くれるから良いんですね（藁。

計算モデル〜は絶版でした。。。
横内さんの本は前になんかのスレで
よい本だと書いてあったような。
帰りに本屋さんに行って見て来ます。

それにしても独学はしんどいですね。
自分でなんらかの処理系を書かないと
ものにならないのかも。ってかこれは
学生も同じか。

学部生はどんなもの作るんでしょうか？

>>138
演習問題はどうだったろう。覚えてない。
つーか数学の本を読むときは演習問題を解くよりも
そこに載ってる証明を何も見ないで再構成できるようになるまで
完全に把握する方が良いと思われ。
それから先は実装みたいな具体的な問題に取り組んで、
そこで分からない点を解決するために専門書とか論文とかを探して読む。

>つーか数学の本を読むときは演習問題を解くよりも
>そこに載ってる証明を何も見ないで再構成できるようになるまで
>完全に把握する方が良いと思われ。
なるほど。ちなみに今読んでるMeyerさんの本は日下部氏の
「作って分かる〜」みたいなノリなんですよね（藁。
数学的に詳細な説明が必要だと思われるとこでは、
これこれについてはこの論文でって形で逃げる。
簡単な数学は使われているけど数学それ自体に
ついては何も書かれていないんです。
だからおれみたいなどきゅそでもなんとか読めるんだけど。。。汗
もう少し突っ込んで勉強するにはちゃんとした工学書や論文を
よまにゃならなそうですねえ。まぁ来年の話ですが。

勉強のヒントになりました。ありがとうございます。
Meyerさんより簡単な本は無さそうだということで、
まずはこれを暗記するぐらい読んでみたいです。

度重なるスレ違いで申し訳ないのですが、
みなさん論文はどうやって探されていますか？
やっぱりgoogleですか？何かコツのようなものが
あれば、、、教えて欲しいです。
正直、今読んでる本のお勧め論文、古すぎて検索
しても出てきません（T_T

大学の図書館じゃないと無理なものは多い。大学間では取り寄せが可能。
学外の人間の閲覧がどれくらい可能かは大学による。
近くの公立図書館に相談するのも手。

なるほど〜公立の図書館でも論文がゲットできるんですねー
それは知りませんでした。今度都内の図書館どっか行ってみます。

さーてとそろそろ帰ります。横内さんの本あるかな。
今日は色々とありがとうございました。感謝です。

>>143
いやできるかどうか分からないけど、相談するならまず公立図書館だということ。
大学は国とかワタクシなので公図−大図にネットワークががあるかは不明。
その次に大学の図書館に問い合わせ、それでも駄目なら、
専門家を探して丁寧な相談の手紙を大学宛に郵送するというのも考えられる。
最終手段としては聴講生になるという手がある。
厳密にいえば論文の複写は合法ではないので
こういうややこしいことをする必要がある。

>>144
どうもです。まだ図書館にも行ってないし横内さんの本も買ってません。
なぜなら、Meyer本なかなか読めません。8章の再帰的定義が使える条件
みたいなのを調べるのに不動点方程式を使っているあたりでつまずいた
ままなのです。なにいってんだかさっぱり分かりません。マジ脂肪です（汗

もう少しねばってみます。

C 以外は糞!!

風呂茶ー戸

>>145
倉田令二朗先生の数学基礎論シリーズ嫁
基礎の前に応用やっても意味無し
全巻読んでから出直して来い

スカトロ先生はむしろ好きだが汎関数の不動点を理解するのに
河合のシリーズは助けにならんつーか基礎づけの目標が違う

糞ループ状態かよ

中島玲二著
数理情報学入門　スコット・プログラム理論
朝倉書店　数理科学ライブラリー３
なんてどうでしょうかね？

>>151
悪くないが、それならこの2冊を薦める。どうせいずれ欲しくなる本だし。
■Stoy, "Denotational Semantics - The Scott-Strachey approach to
programming language theory", MIT Press (1997)
■Barendregt, "The lambda calculus - its syntax and semantics",
North-Holland (1984)

あと Scott domain を理解するなら位相の教科書は多分必要。
いろんな概念(少なくともT0位相)が易しい証明つきで載ってる英語の本は
一冊ないと不便。Barendregtの本はかなり親切だが。
■Gemignani, "Elementary Topology", 2nd ed., Dover Publications (1990)
■Birkhoff, "Lattice theory", 3rd ed., AMS, (1979)

http://www.amazon.com/exec/obidos/tg/detail/-/0444875085/
Barendregtの本は少し高い。
http://www.cs.kun.nl/~henk/papers.html
ここにあるのをいつくか読んでから考えた方がいいかも。
おれもいま読んでます。

http://www.cs.kun.nl/~henk/papers.html にあるのって
おもしろそうだけど The lambda calculus を買うための
判断材料にどれだけなるかはちょっと疑問

通報しますた

誤爆？

>>156
155 は 100 スレくらい上げ荒らしした奴だよ。単に。

日本語で読めるものはゼロ?

>>158
>>152 が挙げてる本の邦訳は多分ないと思う。
まだ挙がってないのだと丸善「形式的モデルと意味論」とか。
古い本では伊藤貴康「プログラム理論」(コロナ社)というのもある。
前者はサーベイ集、後者は入門書。どちらも証明は少ない。

「コンピュ-タ基礎理論ハンドブック - 形式的モデルと意味論」って、この第二分冊？
　http://www.maruzen.co.jp/cgi-bin/mis?Cgifrom=m2-ezy-03&MBN=MJ94008073&Dbs=MPW

＃だいぶ前に、bitでネタになってたような

>>160
> この第二分冊？
そうそう

> ＃だいぶ前に、bitでネタになってたような
そりゃえらく前だな

>>148
こういった議論にどんな風に基礎論が関わってくるのでしょうか？

は？

伊田哲雄・田中二郎　編
続　新しいプログラミングパラダイム　共立出版 1990
を読んでいたら，
「第４章　抽象データ型とOBJ2　（二木厚吉・中川中）」で
代数的仕様記述法の解説がありました．

かへぇおーびーじぇ

http://pvs.csl.sri.com/
pvs 3.0 release age

↑ウェー、ハッハッハ

情けない話だ。
結局社会の言い成りか。マスコミに煽られてビビってるようじゃ駄目だな。

IＰログを取らない「完全匿名掲示板」は、
管理者にとって訴訟リスクが多すぎるので、消滅

Z

大阪ｷﾀ━━━━━━(ﾟ∀ﾟ)━━━━━━ !!!!!

諦めな。

======2==C==H======================================================

　　　　　　　　　２ちゃんねるのお勧めな話題と
　　　　　ネットでの面白い出来事を配送したいと思ってます。。。

===============================読者数： 138720人　発行日：2003/1/9

年末年始ボケがそろそろ収まり始めた今日このごろのひろゆきです。

そんなわけで、年末に予告したIP記録ですが実験を開始しています。

「２ちゃんねる20030107」
こんな感じで各掲示板の最下部に日付が入ってるんですが、
20030107以降になってるところはログ記録実験中ですー。

んじゃ！

────────────────────────Age2ch─
■この書き込みは、Age2chを使って配信されています。
────────────────────────────
Keep your thread alive !
http://pc3.2ch.net/test/read.cgi/software/1041952901/l50
────────────────────────────

>>760
クッキーとアクセスログの参照を有効にしる！

>>598
Mオナニーヨヨイ

>>187
いつも早朝つか明け方に現われるだよ＜ＴＳＢ
このまえの隊長とのボクシング試合のときも、Kityと絡んでたｗ

>時間の約束が守れない奴はどんなに偉かろうが人間的にもうだめぽ

呼びました？

その具体的な理由として社長は、こう話す。
「2ちゃんねるはボランティアの削除人が書き込みをチェックして、
好ましくない書き込みを一所懸命削除している、
ということになっているが、あれはウソ。
削除人には給料が支払われ、その給料の原資となっているのが、
まずいことを書き込まれた企業が削除要求とともに渡す裏金。
これはまさに、総会屋の構図そのものだ。
これまで裁判になっているのは金額で折り合えなかったり、
裏金を出さない強い態度の企業とだけだ」

>>696
モルモット＋金蔓

>>628
名前欄に半角でfusianasann

ボケと突っ込みわかる人　キター

ひろゆきタン、ｶｺｲｲ！

IP記録されても、串刺してれば大丈夫なんじゃないの？

ペット嫌い板は、２ちゃんねるの鬼門だったな。

　あたったね

大阪のほうに差別問題に関する組織があるのだが
そういうところが訴えてきそうで怖いな
ちびくろサンボを差別だ、といったりカルピスの黒人が描いてあるラベルを
問題だと騒ぎ立てるような連中だからな

======2==C==H======================================================

　　　　　　　　　２ちゃんねるのお勧めな話題と
　　　　　ネットでの面白い出来事を配送したいと思ってます。。。

===============================読者数： 139038人　発行日：2003/1/10

なにやら、連日メルマガだしてるひろゆきです。

そんなわけで、ログ記録実験ですが、いちいちサーバ指定するのが面倒なので、
全部のサーバに入れてみました。

重くなって落ちたりしてもご愛嬌ってことで。。。

んじゃ！

────────────────────────Age2ch─
■この書き込みは、Age2chを使って配信されています。
────────────────────────────
Keep your thread alive !
http://pc3.2ch.net/test/read.cgi/software/1041952901/l50
────────────────────────────

さすがに私企業にログ公開はしないでしょ。

侮辱罪で訴えるます

　そうかもね。

198 ：ひろゆき ◆3SHRUNYAXA ：03/01/11 05:48 ID:kSb7xo24
ふ、、勝てば官軍。

199 ：マァヴ ◆jxAYUMI09s ：03/01/11 05:49 ID:ScPwdn5W
そういうヤツなんだよな(^_^;)ひろゆきって

あと、どんな人にも多少の「火」はあるもの。
それを勝手にネットに広めていいとは限らない。

漏らすバカが出るだろうというのが一番の問題なんだよ

それって2000年4月20日くらいからずっとコピペされてるけど
誰もナマのカキコを見てないし
それについての議論もされていないことから
ネタだと思われる

すいません教えてください。
IPを記録されると絶対に個人が限定されるのですか？

ご愛嬌・・・
被害の大きさに差がありそうだけども。
誹謗中傷一番垂れ流しってどこかねぇ？

近藤朋（享年１５）
今日午前４時前、幸田駅の線路脇の道路でキャッチボールしていた中学３年生４人組がいた。
ところが、ボールが線路に入った。
幸田駅の線路に、ボールを取りに入った、中学３年生の女子１名が、貨物列車に
ばばばばばピィー―　　きゃ〜！　　ブァプアあああああああー―――――――ン！！！！！！

６ｃｈ見ろ、高校教師やってるぞ

フュージャネイザン

侵害の事実があったかどうかの確認の意味で閲覧するのは
代理人たる弁護士がやりゃ十分と違うか？？

全部ポセイドンという罠(^_^;)

保守

既知外増殖警報！！！

218.145.25.77:80
218.145.25.14:80
50.51.32.202.ts.2iij.net:80
cache146.156ce.scvmaxonline.com.sg:8080
cache50.156ce.scvmaxonline.com.sg:8080
12.119.64.42:80
ce590-gdl01.terra.net.mx:80
seton03.terra.net.mx:80
218.65.110.14:80
ce590-gdl02.terra.net.mx:80

（＾＾）

訴えられたら捕まる？(^_^;)なんか勘違いしてるでしょ

（＾＾）

comp.specification.zをよく見てるのだけど全然流れてこｔない。
ForamlMethodをやってるひとはどこに生息してるの？
それとも一般ユーザーはもうなかったことにしたいのかな？

（＾＾）

hoge

こういったのってもうビジネスにならないというのが
はっきりしちゃったよね。結局ソフトウェア業界なんて
計算機科学の基礎的な知識のない人が過半数を占めているわけで
いくら有用なツールが出てきたところで、その辺りの人が
使えなければ意味ないよね。萩谷先生なんかも生物学とか
そっちにいっちゃったしなあ。もう終わりかね。終わらないにしても
仕事とは関係のないものかな。

でも、今後ソフトウェアが大規模化すると、しっかり仕様記述して検証しない訳にはいかなくなると思うです。
そういった状況は、実際の開発現場からあがってくるので、大学の研究室に閉じ籠って研究している段階から移りつつある鴨。

>>213
でもどうだろう。
ソフトウェアの規模がでかくなるとそれに比例して
検証もむちゃくちゃ大変になるという。
そもそもそのような仕様記述ができると見込めるSEはどれだけいるのか？

つーか主なアプリは回路設計に移行してるんでは。

>>214
もっと簡単に仕様記述できるツールや手法が開発されるで章。
それでも仕様記述できないSEは生き残れなくなるで章。
但し、それらの手法／ツールは現場に近い場所（大学の研究室でなく）で開発されるで章。

>>215
回路設計業界はソフトウェア業界に比べて健全な証拠

形式的仕様記述の産業界での応用例として
パリの地下鉄がよくあげられるけど
これってかなり昔の話だよね．
最近の例はないの？

最近の最新流行は、人海戦術。これだね。
んでもって予算少な目。これ最強。

ソフトウェア開発の業務そのものに理解が無かった＆業界が急成長した事により、
初期に優秀な人材が集まらなかった⇒現在の管理職は糞⇒アフォな戦術の繰り返し
という事ではなかろうか。
回路設計業界は初期にもそれなりに優秀な人材がいたので現在でもそれなりに健全

ネットワークのプロトコル設計なんかでまあまあ使われてるとかいないとか。
あとセキュリティー方面。こういうのってやっぱり最後は天才の職人芸に
落ち着く気がするんだけど。

J2EE/EJB2.2の検索言語 EQLが、
UML系の仕様記述言語oclをベースにしてる、らしいよ。(このスレ立てた当時の情報では)

形式化

それは技術者の夢

上の方でLinuxのカーネルのバグがどうとか書いてあるけど、
もっとさ、カーネルの柔軟な構成のためにこういった手法が
なんか役にたたんものなの？いまの状態だとあっちを弄れば
こっちににも影響が出てって言う感じで、もうわけわかめ。
そこでマイクロカーネルが〜なんていったところで結局
モノリシックのパフォーマンスには絶対に勝てないし。。。
Linuxはもうカオスですなあ。それでもパフォーマンスだけは
下手によくて、*BSD,Solarisよりもいいからなあ。困ったもんです。

>>217
＞形式的仕様記述の産業界での応用例

いくとこいけばあるよ。例えばＮＡＳＡとか。
ＰＶＳ使った事例が結構あったよ。

>>212
＞結局ソフトウェア業界なんて計算機科学の基礎的な知識のない人が
＞過半数を占めているわけで

でも計算機科学（というかソフトウェアサイエンス）の基礎知識なんて
大したもんじゃないって。それにそんなのは論文書いて大学の先生に
なるためのもんだよ。例えば立命館の高山先生とか（笑）

＞いくら有用なツールが出てきたところで、
＞その辺りの人が使えなければ意味ないよね。

それはそうだね。
モデルチェッキングはツールとして有用な気がするけど
証明系はどうかな。

>>225は高山先生本人と見た！ age

藁

このスレも高山先生の人気に飲まれてしまったか・・・

自分が数学板にリンクを貼ったのがまずかったらしい…
つか最近厨房だらけだよあそこは．はぁ〜

http://www.atmarkit.co.jp/news/200302/21/devsummit.html
モデルチェッキングは有用。

証明系が神道するにはあと30年はかかるだろうな。
PVSなんかのプロトタイプ検証系にしても常人にはかなり辛いし。
証明系が使えると判断されて、それに対する教育コストを惜しまない
ような雰囲気が出てくることがまずは先決か。

＞証明系が神道するにはあと30年はかかるだろうな。
＞PVSなんかのプロトタイプ検証系にしても常人にはかなり辛いし。

ＰＶＳをマスターすること自体は３ヶ月もあれば十分だよ。
難しいのは、証明すべき定理となる仕様を思いつくこと。

証明を書くのが大変だというけど、プログラムを書く以上に
大変なわけではないよ。証明はプログラムでもあるわけだから。

>>232
>証明を書くのが大変だというけど、プログラムを書く以上に
>大変なわけではないよ
それはどうかな。Eiffelのassertionのようなものでも人は
難しい、かつめんどくさいと感じる。人がプログラムを組んでいる
ときに、全ての条件を想定しているわけではないという事実を
もっとよく見ておく考えておく必要がある。

>>233
＞Eiffelのassertionのようなものでも
＞人は難しい、かつめんどくさいと感じる。

＞人がプログラムを組んでいるときに、
＞全ての条件を想定しているわけではない

確かに。でもそれは言い訳じゃないかな。
ちゃんとデバッグする気があるんなら、
条件を想定するよね。全てとは限らないから
全部省略していいということにはならないよね。
わかっていることだけでも書かなかったら
なんにも情報がないよね。

…と少々強気に出た。

>>234
>ちゃんとデバッグする気があるんなら、
>条件を想定するよね
時間がないということがいいたいんじゃない。ただ全ての条件を
想定するような仕事のためには別途どこかを削ってそれを割り当てる必要がある。
それはどこかと言えばテスト。assertionによってテストにかかる
工数を確実に減らせるということが認知されればいいんだけど、
なかなかねえ。そこにかかる時間の量と、その無駄の多さは誰しも
感じているところだろうけど。。。
少し大げさな話だけど、人文科学が実験できないという
意味で、ソフトウェア開発も実践を通して反省するという
点は同じかと。スパイラルモデルにしても一度やってみないと
その有効性は実感できない。それと同じで開発手法としての
Eiffelも試してみたいんだけどなあ。この不景気だと強気な
仕事より、失敗しない仕事が優先されるからね。そんなものは
とうてい無理か。

assertionを記述することは、デバッグにおける
原因探索の無駄を省くとは思うが、「コード化」
だけを考えたら、直接の御利益はないかもね。

とはいえ、バグっても人が死なないシステムなら
ゴメンナサイとか謝っちまえばいいのか（笑）

Design by Contract (DbC) 周りで、
制約条件をOCLで記述する iContract が流行っているらしい。(JavaWorldで既出)

単なるassertionだけでなく、実装コードを埋め尽くすつまんない条件分けコード
を一掃するのに使えれば、いいのかな？

iContract、AspectJ (@www.eclipse.org) に組み込んで使えるらしい。
下のFAQによると、複数のクラスにまたがるinvariants(invariants cross-cutting)
を扱えるようになるのがメリットらしい。
　http://www.reliable-systems.com/tools/iContract/FAQ.htm

個人的には、複数のAspect間の干渉を排除するヒント情報として活用できたらいいと思った

京大の「コンピュータ・サイエンス入門講義」講義ページで
意味論のノートがダウンロードできるみたいです．（試験問題も）
http://www.kurims.kyoto-u.ac.jp/~cs/csnyumon/

http://www.kurims.kyoto-u.ac.jp/~cs/lecture/

自分は情報系じゃなかったんで，テスト問題見てるといろいろ面白いです．

プログラム意味論じゃなくてzについてそろそろ勉強したいのですが、
どの本がいいのでしょうか？

http://dmoz.org/Computers/Programming/Languages/Z/Books/
何気に沢山あるので迷いますね

http://iskig11.is.noda.tus.ac.jp/~enomotolab/

プログラム意味論ってこの10年間殆ど進歩してないよな。
っていうかこれまで進歩らしい進歩があったわけでもないけど。

（＾＾）

　　 ∧＿∧
　　（　　＾＾ ）＜ ぬるぽ（＾＾）

>>244
なんで進歩しないの？
意味論の進歩が無意味になった（尽くされた）からかな？
＃無意味論しる！

　　　 　∧＿∧
ﾋﾟｭ.ｰ　(　　＾＾ ） ＜これからも僕を応援して下さいね（＾＾）。
　　＝〔~∪￣￣〕
　　＝ ◎――◎ 　　　　　　　　　　　　　　　　　　　　　山崎渉

ここを読め！
Z言語のサンプルもあるぞ！

ユニシス技報60
http://www.unisys.co.jp/tec_info/tr60/60home.htm

>>241
もう日本にZの本は存在しません。
唯一日本語で書かれた本がありましたが、絶版になりました。

Amazon.co.jpのデータベースには無いので、cbook24.comより

ソフトウェア仕様記述の先進技法 - Z言語
http://www.cbook24.com/bm_detail.asp?sku=00092314

>>250

いや、Zの本は多数あるよ。
学習参考書コーナーに行ってごらん。

>>251
それはZ会だな

いや、実はZ言語の本も多数あるんだよ。
洋書で。日本には0

ZはZFCのZですか？

>>254
そうらしい。ZFC（公理的集合論）のZと同じ。
さらに元をたどれば、ZFCもZ言語も人名のイニシャル。

Zermeloは集合論の公理系を考えたひとですよね？
でもそれだけでは何がなんだかよく分らんですねえ。

http://ysserve.cs.shinshu-u.ac.jp/Lecture/SetTheory3/settheory01/node1.html

>>250,>>253
その本、Z言語の名前を始めて知ったきっかけだけど、
発売当時は浮世離れした象牙の塔の本、って感じて買い逃したな。
確か洋書を古本屋で入手したけど。

あと、Z言語以外の仕様記述言語本は、結構残ってる。
例えば、http://www.cutt.co.jp/book/index.html#Communication

ところで、Web上で、サハラ伸センセーの仕様記述レクチャーが始まったんで、あげ。
　http://www.jfits.co.jp/column01/33.htm

Nice Age

綺麗なおっぱいがいっぱい♪きっとモミモミしたくなるよ♪
二日間無料で見れるからの覗いて見てね。
http://angelers.free-city.net/page001.html

形式あげ

プログラム言語意味論は証明論やモデル理論とはどんな関係があるの？
その辺りまとめてあるような本や論文ある？

◆◇◆◇　海外サイトだから安心無修正　◇◆◇◆
http://upbbs.s2.x-beat.com/linkvp/linkvp.html

　↑　
ココは丸見え！　今ならまだ消されてないよ。たぶん・・・

　__∧＿∧_
　|（　　＾＾ ）|　＜寝るぽ（＾＾）
　|＼⌒⌒⌒＼
　＼ |⌒⌒⌒~|　　　　　　　　　山崎渉
　　 ~￣￣￣￣

http://www.zuser.org/

こういう知識があるひとも2chを見てるんだろうけど
なぜ、このスレにレスしてくれないのか、その理由が分った気がした。

（＾＾）

仮にプログラム製造の劇的な工数削減に成功する技術があったとする。
それは本当に市場に受け入れられるだろうか？個人的には疑問が残る。
これだけ大きくなったIT産業を壊滅させるようなものは
到底受け入れられないのではないか。Lyeeに対する過剰な反応を見ていると
そんな気にさせられる。

アメリカは軍事産業を維持していくためだけに戦争をする。つまり
主要産業>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>戦争
なのである。2ch的な言い方でいえば。
IT産業にも同じように莫大な資金、人員が注ぎ込まれている。
これを、効率だけを追求した技術でもって、産業を縮小させるような
真似はできるはずもない。

IT産業を奴隷を使ったピラミッド製造になぞらえる向きがある。
だがしかし、それは巨大な産業が成熟期へと移行する必然的過程なのだろう。
ピラミッドは安定した権力の象徴。これを崩す何物も受け入れられない。
既におのおののポジションは決まっている。もうこの業界には夢はない。

自動車産業はフォードの開発したプロセスとともに始まった。
生産プロセスの改善そのものを肯定的に受け入れる文化がある。
だがしかし、この業界は不幸なことに、ソフトウェアの生産効率よりも
計算機資源の有効活用こそが至上命題という時代が長くつづいた。
未だにC系統の言語が広く使われている現実から見て、
悪しき文化は今後も続いていくことだろう。
インドのテニスコードの比喩で言えば、この業界の技術革新とは
ボール拾いの少年に対して、よりよい靴を開発することだといってよい。

>>266-268
　はぁ、なんのことやら
　最近は、このスレにも変な人が来てるのね

もともと文系板だしな

>>268
でも、リストラはバンバンされたわけじゃない。
開発者を削っても、市場が小さくなるわけでもないでしょ？
開発期間が短くなればソフトウェアを安くすることもできるし。

>>268
ﾊｧ？奴隷を使ったピラミッド製造？

ピラミッド製造は、(ナイル川氾濫による)農閑期の雇用確保政策
であって奴隷労働とは違う、というのが、最近の定説なんだが。

そして、国内の建設業界やIT業界の最大の目的は、
効率化による利潤確保などではなく「雇用確保」な訳だが。

>>271
　　仕様記述で生産性向上
って方向に、強引に結び付ける貴方の真意が理解できませんが、何か？
生産性向上ｸﾞﾙｰﾌﾟの方ですか？？？

>>270 名前：デフォルトの名無しさん ：03/08/12 09:24
＞もともと文系板だしな

カオスだ株だと、痛いスレ立てまくるオマエさんにゃー、言われたくねぇよ(藁

　　　 (⌒V⌒)
　　　│ ＾ ＾ │＜これからも僕を応援して下さいね（＾＾）。
　　⊂|　　　　|つ
　　　（＿）（＿）　　　　　　　　　　　　　　　　　　　　　　山崎パン

>>273
形式的仕様記述のスレで生産性の話を始めたのは>>268

DesignWaveでハードウェア・ロジックのベリフィケーションの記事が連載されている。
このスレの上の方には「形式仕様記述」で検証する技術は、
まだハードウェア業界でも普及していない、とおっしゃる御仁も居る。
ハードウェア業界における検証と形式仕様記述の検証って、何が違うの？？？

ハードウェア業界：論理回路検証〜物理シミュレーション〜試作チップ検証
形式仕様記述：　　なんか高尚な事狙ってるのか？仕様からプログラム/ハードウェアを自動合成とか（ｗ

漏れ的には、構成的プログラミング（ｗというのが近いのかな〜と妄想してみたり（ｗ

あげまん

（　´Д｀）/＜ 先生！！こんなのを見つけました。
http://www.hokekyoji.com/
http://www.yakuyoke.or.jp/
http://members.tripod.co.jp/hossyoji/index/
http://www.maap.com/tanjoh-ji/
http://www.honmonji.or.jp/
http://www.maap.com/tanjoh-ji/
http://www.kuonji.jp/
http://www.butsuzou.com/jiten/sanmen.html
http://www.butsuzou.com/list1/sanmen2.html
http://www.butsuzou.com/list1/sanmen3.html
http://www.butsuzou.com/keitai/sanmen-kz.html

２００３年
あなたの欲しいものは何ですか？
あなたの欲しいものを調べた後に
ランキングで紹介します。
お一人様　３品まで記入してください。
http://www.c-gmf.com/Quest.htm

Agile手法で仕様記述なし即コーティングする習慣を、
「プログラミング言語で仕様記述する手法」と見なしてはどうか
と提案する人達が居るらしい・・・
そしてその意見には、漏れも禿同。

1)要求定義ー2)仕様記述ー3)プログラム製造
っていう3段階におおざっぱに分けたとして、
1,2は各プログラマの脳内と意思疎通に使われた紙切れ
しかないわけだけど、ある意味FREENIXなんかの開発では
普通に行われているよね。ただしそれは既に要求定義ががっちりと
出来ているからこそ。UNIXという概念、文化が先にある。

形式的仕様記述はそういったものとはなんの関係もないよね。

形式的仕様記述って、どこが違うの？形式的手法の有無？
あと、仕様記述を通常のプログラミング言語で注意深く行った場合、
どんな相違があるのかなぁー？？？
子供だから（・∀・）ﾖｸ､ﾜｶﾝﾅｲﾔｧｰ!!!

高山先生、なんか書き込んでくれないかな。先生のファンなんだけど。

可換代数で果敢にAGE

形式的仕様記述言語で書きやすいドメインはなんですか？

だれかJMLって使ったことあります?

Java + Eiffelのassertion + VDM

みたいなもんらしいですが.

おまいら、セキュリティ仕様やデータ安全性の検証って、どうやってますか？
SSLプロトコルやらLinuxやら、はたまたEJBのセキュリティや仕様自体の曖昧さを、
形式仕様記述言語使って、実験的に検証した、とか聞くけど、どーなのよ？

VDMとかRAISE使うと出来るの？
ZやVDMじゃだめなんだろうね？

おまいらの情報、とっとと早く書けっ！！ほれほれっ

さもなきゃ形式仕様記述なんて、実用で使ってくれる所、滅多にないんだからさぁ

>>22
CafeOBJといえば学会でよくJAISTの人が発表してた。
なつかしいな。

LOTOSあげ

じっさいVDM++とか使えるん？

> ## 見たなぁ。
> ## 今あなたは、このファイルをエディタなりで見ていますね。
> ## そういう方には、ヘルプファイルの形式をお教えします。
> ## 頑張れば、自分専用のヘルプ情報にできます。
> ## コントロールキーの割当ての部分を変えるとか、Ｃの関数の仕様を
> ## ヘルプファイルに入れてしまうとか、そういうことをやって下さい。
> ## 大変だとは思いますが、頑張って作って下さい。
> ##
> ## 【ヘルプファイルの形式】
> ## 形式は、通常のMS-DOS標準テキストファイルである。
> ## 内容は、改頁コード(0CH)で区切られたページの集まりである。ひとつの
> ## ページは、ページ名、見出し行、本文、制御行からなり、見出し行、本文、
> ## 制御行はなくてもよい。
> ##
> ## <ヘルプファイル> ::＝ {<ページ>}
> ## <ページ> ::＝ <ページ名>{<見出し行>}{<本文>}{制御行}<改頁>
> ## <改頁> ::＝ 0CH
> ## <ページ名> ::＝ <検索対象ページ名>|<非検索対象ページ名>
> ## <検索対象ページ名> ::＝ <頁区切文字1><30文字以内の文字列><頁区切文字2>
... 以下略

以上, 新松のヘルプファイル先頭より。
後になってこの説明が BNF またはその variant だと知った。
ヘルプファイル自體は(簡易?)ハイパーテキスト形式であった
(さう言や K3 は當時簡易 SGML フォーマッタも作ってゐたとか)。
尚, このヘルプファイルの先頭部分は後の松からは削除された。
「巫山戯た事を書いて怪しからん」と苦情を言った(或は苦言を
呈したのか?)顧客が居たからだと何處かで讀んだ氣がする。
眞僞の程は知らない。
通りすがりにスレ汚しスマソ。沈んで來ます。

>>282 executable notation, executable documentation ってやつですね。

投稿台の冒険吸湿に最近入り浸ってたんだけど、
やつら未だに仕様奇術＝実装が可能だと信じ込んでるぞ。
実務的にはRational MDAの出現でFAなのに、チョト可哀想。

代数学を誰もが理解できるわけではないというこの現実から始めよう

助けてください。SOS
オカルト板で、バサバサ削除する削除人が
登場しています。こわいです。おそろしいです。SOS
http://qb2.2ch.net/test/read.cgi/sakud/1021962883/l50

>実務的にはRational MDAの出現でFAなのに、
この認識は実務レベルでもドキュソだと思うけど

>>298
どーでもいいけど。
じゃ、なんか提案してみて。

>>298
>>295は、「多少は実用的な MDAですら 『仕様＋スクリプト』で実装コード生成してる
のに、今更『仕様奇術＝実装』はねぇだろ」っつう意図で書いたんだが。

まさか・・・「MDAで仕様奇術＝実装が可能になった」とか「MDA実用的でｻｲｺｳ」とか
読み違えてるわけねぇよな(ﾜﾗ

いずれにせよ、より良き提案があれば、あなたの意見を受け付けます。
提案ができねぇようなら、さっさと氏ね

↑ちなみに、「氏ね」は「この場からサッサと立ち去れ」という意味の
　２ちゃん固有の煽り文句。生命を終了させろ、という意味とは違う

ましてや、実際のその言葉を口にした事は、これまで一度もない事は言うまでもない

ましてや、実際その言葉を口にした事は、これまで一度もない事は言うまでもない

実用レベルでつかっているとこあんの？

>>300
>>295のFAってどういう意味？
あと、>>299と>>300の「替わりになんか提案しろ」の論理が
よくわからんのですが…

>>304
ITU

形式的記述とはちょっと違うけど
プログラムの解析だか正当性の検査にデータフローを追うみたいなやり方ありませんでしたっけ。
まえどっかでチラッとそんな内容の本を見た記憶があるんだけど題名が思い出せないんです｡
Amazonでそれらしき単語入れてもヒットしないし。

>>305
ふりーえーじぇんと。

ま、ファイナルアンサーだと思うのだがな。
で、やつらは銀の弾丸を求めてるだけだからほっとけ。

あぼーん

↑頭の病気の人、とうとうこのスレにも進出してきたか。
　

>>308thx

キャッツの社長さんが書いたＵＭＬ動的モデルで組み込みモデリングの本、
なかなか面白そうですね。
システムＬＳＩ〜形式的手法の話まで触れていて、なかなか興味深いんで、早速買いました。。。
って、この本、１年前に発売されてたのね。。。
ウルシステムやオージスの本は知ってたけど、
キャッツの本、マジでこれまでずーっと目に止まりませんでした。
この本読んでおきゃ、去年一年無駄にせずに済んだものを。。。

あと、面白そうなのは、セマンティックWebで会社作って、星雲社からシリーズ本出してる人の本。
ここ数年、漏れが目標としながらなかなか形として実らなかったものが、着々と形になってきているんだな〜と強く感じた、春の夜。

よく分らんが、UMLみたいなモデリングに関するものって
形式的仕様記述と呼べる物なのか？おれは代数学を
使わないとそうは呼べないものだと思っていたが。論理で
ゴリゴリやるのもそう読んでいいかもしれんけど。

>>313
別にどう解釈してもえぇ〜んじゃねぇ〜？

仮にUMLが代数学と比べてショボい・低級なツールに見えるとして、
そのショボいツールで、LSI製造メーカがLSI設計しようとしているとしたら、
その意味はどこにあるのか、考えてみてはいかがでしょうねぇ。

今、国内で、それなりの規模と質の仕事で、形式的仕様記述を扱おうとしている所って、
どれくらいあるんでしょうね？

・旧鉄道総研系？
・証券のWebフロントエンドやってるあそこ
・SystemC＋UMLでツール作ってる↑あそこ
・組込系でExecutableUMLやってる所
・MDA周りは、形式的仕様記述ってのとは違うのかな？(大メーカ、大SIerもまだ模様眺めみたいですが。。。)

>>315
いやだからおれの言いたいのは、UMLはスレ違いなんじゃ
ないだろうかってこと。まあ過疎スレだから何書こうが
おれはどうでもいいけど。

>>313
Syntropy方法論でVDM使って形式仕様記述(つかHoare論理の記述なのかな？)したのが、
UML 1.1 Object Constraint Language 標準化の発端だとすれば、
OCL込みのUML、OCLと等価の仕様記述を持ったUMLも、形式仕様記述の一種と見ていいのではないかと。
後、Executable UML〜MDAの流れも。

あと、形式的仕様記述っつうと堅苦しく見えるけど、
Formal Method って言えば、いろいろバリエーションがある事は想像がつくでそ。
例えば、>>５６ のメモ参照。

どう思われますか。

>>317
あんたのレスは筋違い。
わかったふうなレスで、スレを荒らすな。
厨房はもう寝れ。

>>315
「人海戦術で厨房プログラマー集めて、雑多なシステムLSIを大量に設計させるのが目的。
　それが可能になったら、高学歴高収入のLSI設計者はリストラしたい」、とかなんとかだったら、
日本の将来は暗いねぇ〜ｗ

>>316
ttp://unit.aist.go.jp/informatics/ も入れよう.

>320
そもそも ITって、そんなもんでは?
「素人でも熟練者なみの○○ができる！」っていうか.

`>321

ぁ、AISTのシステム検証センターね。関西だっけ？
ちょっと前まで、ポス毒とテクニシャンの募集してたっけ。
たしか、テクニシャンの任期が最長2年、なんでちょっと(ry


で、IT云々の件、
メーカや総研やSIerで なんちゃってSE/コンサルやるなら、
その程度の認識でも結構でしょうけどｗ
俺は、そんな程度の奴とはお付き合いしたくないなぁ〜

理学者が、概念整理して体系を作って、
工学者が、それを素人でも扱える対象に焼きなおして、
そうやって食い散らかされた挙句の
「一見うまくいきそうだが、実は落とし穴だらけ」な「単純作業の荒野」
で、素人労働者の皆さんに、いかにいきいきとクリエイティブな仕事をして頂くか？
という観点も重要なんぢゃないか、と。

>>322
高学歴高収入なエンジニアは（おそらく）クリエイティブな設計をする為の訓練を受けてない,
落とし穴をひとつひとつ潰していく（ある種のデバッグ）事が高学歴高収入なエンジニアの仕事　⇒　自分の首を絞め...

ホントに工学部でスポイルされちまった、自称高学歴の職人さんより、
まっとうな学問的訓練の経験すら怪しい厨房プログラマ〜の方が、
ナンとやらも煽れば木に登る〜って感じで、オモロイ反応してくれるかもｗ

俺は厨房とは顔合わせるのもやだけどｗ

>>323
クリエイティブなLSI設計って、一体なんなんでしょう？

東芝-Sony-IBMのセル計画みたいなの？
それとも、いち早くMP3エンコーダ・チップや、MP4ビデオ・プレーヤや、新しい携帯電話付加機能を企画するような人の事？
はたまた、ヲズニアックみたく、シンプルで高機能な回路を設計する人の事？

よくわかんないっす。

マイクロ・プロセッサの開発：IntelとNEC (1970頃)
LSI設計のコンピュータ支援：(1970年代アメリカ)
DSPの開発：　　　　　　　　　　NEC (1980年代？)
PLDとかFPGAの開発：　　　　(多分海外っすね、これは)
とか見ると、日系企業では NECのクリエイティビティが結構高そうかなｗ

物性物理の新規分野開拓、てな意味では、日立とかNECとか、強いよね〜多分。

う〜ん、難しい問題ですな。
ただ、昔と今とでは状況が違う。
昔は、開発に携わる事ができる人がほんの一握りであって、
そんな仕事に就くには（信用が必要なので）高学歴であったけど、
今では、開発が非常に多くなって高学歴職人が揃えられなくなった,,,
厨房でも設計できるツールが必要≒高学歴高収入は不要

クリエイティブは、個人の感性とか経験が大事なので、学歴はあまり関係ない，
芸術に近いものだと思う。
学歴が感性を磨いたり経験を積んだりするのに役立たない教育過程の指標な訳だし。

なんか、スレ違いなので、この辺で...

頭いい人なら、自分で記述方法を考案してそれを使うよね。
他人の作ったものをありがたがるんじゃなくて。俺仕様の
害悪とはまた別の話になるけど。

>>322
AISTはDQ法化してから商売に走ってるからなあ。
でもまだ武家の商法ってところはあるね。

鉄道信号の場合は国際規格との絡みもあるからな。
ヨーロッパのメーカは差別化のために形式仕様を
宣伝してるから日本がこれに追従できないとこれから
海外で商売する場合に困るのは確かだね。

で、モデルチェッキングくらいなら素人でもすぐ使えるよ。
SPINとかSMVとか只で使えるツールもダウンロードできるし。
AISTはSMVつかってるね。あれはCTLで仕様を書くのかな。
SPINはLTLだね。どっちがいいかは一長一短あるけど。
使ってみると面白いからやってみたら？

形式仕様はクリエイティビティを阻害しないと思うよ。
それに、形式仕様って実はそんなに難しくないって。
今時は文系でも形式論理学教えてたりするからね。

一応修士修了の漏れがいうのもなんだけど
”高学歴”って確かに意味ないね。
クリエイティビティは学問の世界でも大事なはずだけど
実際には大学の教育はそういうこととは無縁なのは確か。
まあ、教育でどうこうできるのか？って疑問はあるけどね。

＞UMLみたいなモデリングに関するものって
＞形式的仕様記述と呼べる物なのか？
＞おれは代数学を使わないとそうは呼べないものだと思っていたが。

ま、代数を使うかどうかは別として、UMLの場合
モデルが満たすべき性質を陽に記述できないんで
その意味では形式仕様の記述っていう感じではない。
（OCLとかいう言語で性質を記述するとかいう話もあるが
　よく知らないので割愛。）

代数っていうのは例えばCafeObjみたいな
代数的仕様記述のこといってるのかな？
実は漏れ、あれのどこが代数なのか
よく分からないんだけど（笑）

>>329
論理学って、数理論理学以外は文系に分類されちまうらしいね。

それから、大学が、クリエイティビティを促進するか、阻害するか、は一概には決められないと思うよ。
そーゆーこと言う人って、いったいどこの学部/学科出身なんだろうね？情報系〜工学系？ｗ

>>330
UMLは、UML1.1以降のOCL込みで、形式仕様記述であろうとした、って感じだと。

>>331
いや、最近は文系でも数理論理学を教えてたりするよ。

大学がクリエイティビティを阻害するとは思わないけど
積極的に促進するって感じでもないでしょ。
もちろん、例外はいくらもあると思うよ。
そういうところにはがんばってほしいよね。
ちなみに漏れは理工系学部の情報系学科出身。
やってきたのは理論臭いことばっか。
だから漏れの見方も偏見に満ちてる。ｗ

>>331
そして、ExecutableUML〜MDA〜UML2.0で、ツールが自動コード生成するための、
グラフィカル・モデリング言語になったとさｗ

めでたしめでたし

昼弁当23時の問題

昼飯用に調理された弁当を、23時に食べても安全であるか否かという
前世紀初等に提出された有名な未解決問題。

IPA
セキュリティエンジニアリング
ソフトウェア開発者向けのページ

2. セキュアプロトコルと相互運用可能性確保
http://www.ipa.go.jp/security/awareness/vendor/software.html#2

IPAか。
あそこは結構腐ったネタを、文献調査してあとはせいぜいデモ・システム作って
研究と称してる感じがあるから、パスしときたいな。

いまどき、○×総研程度の連中ですら、
「検索エンジン使って情報集めるようなのは研究とは呼べない」だってさ。
連中がWebCrawlの研究開発に貢献した、という噂は一切聞いた事ないんだけどｗ

あんまり身のある議論も出なさそうだけど、とりあえずあげ