おめぇら、形式的仕様記述について知ってる事を書け
■ このスレッドは過去ログ倉庫に格納されています
0001素人な部外者
NGNGプログラムやプロトコルの仕様の、
フォーマルな記述方法っていくつかありますが、
どれくらい有効なんでしょうか？
形式的仕様記述を有効活用するには、
どんな知識が必要なんでしょうか？
おめぇーら、知っていることを書け！
0002２
NGNG0003デフォルトの名無しさん
NGNG0004デフォルトの名無しさん
NGNG0005デフォルトの名無しさん
NGNG0006デフォルトの名無しさん
NGNG0007デフォルトの名無しさん
NGNG意味とかポインターとかも書いておいて下さい。
0008デフォルトの名無しさん
NGNGhttp://mentai.2ch.net/test/read.cgi/sim/981553632/
0009デフォルトの名無しさん
NGNG0010デフォルトの名無しさん
NGNG技術は経験！
スタジオにお返ししま〜す！
0011デフォルトの名無しさん
NGNGできるような）では強力．もちろんコードが仕様を満たしていることも検証しやす
いような言語なら最強．
0012デフォルトの名無しさん
NGNGで、Zってなによ＞５
0013デフォルトの名無しさん
NGNG0014デフォルトの名無しさん
NGNGhttp://saeki-www.cs.titech.ac.jp/~ugai/Z/z-faq.html
こんくらいしか見つかんなかった。
0015デフォルトの名無しさん
NGNG0016デフォルトの名無しさん
NGNG0017デフォルトの名無しさん
NGNG「仕様の『抜け』検出」について考察してマウス...)
0018デフォルトの名無しさん
NGNG0019デフォルトの名無しさん
NGNG0020デフォルトの名無しさん
NGNGhttp://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の意味論」をきちんと扱おうとすると、別の形式的仕様記述が必要そうですね。
0021デフォルトの名無しさん
NGNG0022デフォルトの名無しさん
NGNG0023デフォルトの名無しさん
NGNGそれ、妖怪「空耳」だ、うちにもよく来るよ。
0024デフォルトの名無しさん
NGNG0025デフォルトの名無しさん
NGNG國産品を愛用しませう！
0026デフォルトの名無しさん
NGNG特にコンポーネント関係の研究してる辺り。
2月末の報告会聞きいきますんで、もし見てたらよろしくお願い致しまし。
0027デフォルトの名無しさん
NGNG0028デフォルトの名無しさん
NGNGOCLは何で現場で使われないんだ？
数学に疎いエンジニアの為に作った
って仕様書に書いてあるのに、現場で
使ってるのなんてみたことないぞ
0029デフォルトの名無しさん
NGNGうぃんどうがでる
ぼたんをおす
しゅうりょう
0030デフォルトの名無しさん
NGNG処理系がないからでそ
0031デフォルトの名無しさん
NGNGわかってる、わかってるよ。論文読めってんだろ...そりゃわかってんだけどさ。
0032デフォルトの名無しさん
NGNGサブセットっぽいけど、処理系ならあるでそ
(ArgoUMLのこぴーらいとからこぴぺ)
Frank Finger's (TU-Dresden) OCL-Compiler (dresden-ocl.sourceforge.net)
アプリケーションはこのあたり。
・ArgoUML
・EJB 2.0 EQL
0033関係者
NGNGここだけの話、使えるＦＭって今はモデルチェッキング。
やっぱ、オートマチックに動かないとね。
こないだ某所で話したＮさんはSPINつかってるらしい。
0034デフォルトの名無しさん
NGNGこのあたりっすか？
http://www.ipsj.or.jp/members/SIGNotes/Jpn/09/2000/129/article014.html
「EJB仕様書から仕様記述を作り検証する」って凄そうなんですけど、、、
アーキテクチャ云々するほど洗練度の高くない仕事でも使えますか？
0035関係者
NGNG>>33は、「Ｎさんがある会合でお話をした」ってことです。
私は直接お話したことはありませ〜ん
http://www.shinsahara.com/www/sigfm/
お話の件ですが基本的には有限状態機械として表現できれば大丈夫かと。
0036デフォルトの名無しさん
NGNG明示的にあるいは本質的に、FSMとして表現されていない部分は、
仕様検証の対象外になるんでしょーか。疑問ばっかりですんません。
0038デフォルトの名無しさん
NGNGこのスレが伸びてくれれば2chも捨てたものではない
とか言ってみる
0039デフォルトの名無しさん
NGNG2ch見てないで論文読み漁る方が
はるかに早いと思います。
もし知識があるならご自身で
なにか書き込んでみてはいかが
でしょうか？
00408080A
NGNG所詮，ソフトはライフサイクルが短くて，品質には甘いので...
そういえば，Haskell 板で苦労している monad は，プログラム記述と，
仕様記述の中間のような気がしますね
0041デフォルトの名無しさん
NGNG元の系が有限状態でなくても、抽象解釈して有限状態として検査するのが
「今のモデルチェッキング」の流行りでは？といってみるテスト。
0042デフォルトの名無しさん
NGNG0043デフォルトの名無しさん
NGNG正直言って難しかった．
こんなに数学寄りの話だったなんて知らなかったよ．
004434
NGNG漏れも、その件引っかかっています。
詳細わすれちまったんですけど、
実際によく目にするプログラムは、
有限状態機械より、ペトリネットに近いみたいですんで、
それをどうやって検証するのか？
(FSMに翻訳 or ペトリネット向けの検証系)
興味あります。
でも、聞いてばかりでは自分の理解も進まないようですので(笑
自分が勉強してから解くべき課題にしておこうかな？
0045デフォルトの名無しさん
NGNGそれって例えばAlloyとか？
0046デフォルトの名無しさん
NGNG今日は Amazonから Catalysis本と OCL本が届いたので、
記念age
Alloy : MIT方面で開発されたものでしょうか？
もしかすると、ソフトウェア工学のゼミでは、
普通に扱う題目なんでしょうか？>>非FSMのモデルチェッキング
(漏れは専門外)
SQL: 形式仕様記述に近いものだ、とお聞きしますが、
それはどのような意味でしょうか？(制約論理関連？)
＃EJB2.0でも、問合せ言語EQLとしてOCLを使うそうですが...
0047デフォルトの名無しさん
NGNG004845
NGNGAlloyはMITのDaniel Jackson等によるものですね。
有限モデルの存在をチェックするものと認識してます。
（私も最近知ったので、詳しいことは分かりませんが）
非FSMのモデルチェッキングは今は研究段階だと思います。
0049デフォルトの名無しさん
NGNGhttp://www.ifad.dk/Products/vdmtools.htm
0050デフォルトの名無しさん
NGNG国内でどのくらい使用例あるのかな？Ｚ
大学の時の先生がＺの専門家だったんだけど、社会に出て一回も聞いたことないよ
0052デフォルトの名無しさん
NGNG0053デフォルトの名無しさん
NGNGOCLでアクション・モデル記述してる、MDA製品ベンダーの人とか、
リアルタイム組込システムでFormalMethodを導入してる、UMLの偉い人とか、
なんかスゴイ人ばっかり見たんで記念アゲ。
0054デフォルトの名無しさん
NGNGEiffelの表明なんかも「仕様記述」と考えていい？
0055デフォルトの名無しさん
NGNGホーアのCSPは、プロセス代数的仕様記述で、
INMOSトランスピュータ近辺の応用例が有名みたい。(例が古すぎ？)
＞Eiffelの表明なんかも「仕様記述」と考えていい？
どうなんでしょ？「プログラム検証に役立つ一機能」かなー。
Eiffelで仕様記述するって聞かないし、
形式的手法の一応用例かと、漏れは思うのですが...
0056デフォルトの名無しさん
NGNG要約してコピペしてみます。
＃でも、モデルチェッキングとか、
＃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、を使用していた...
------------------------------------------------------------
0057デフォルトの名無しさん
NGNG0058デフォルトの名無しさん
NGNG0059デフォルトの名無しさん
NGNGまだ若かりし、小学生の頃
↓
母にポテチをねだる
↓
却下される
↓
ぐれる
↓
極道の世界へ
↓
数年後
↓
母から一袋のポテチが届く
↓
兄弟から母が死んだと電話が入る
↓
母の遺言から母の真意を知る
↓
「あの子は体が弱いからあまりジャンクフードは食べさせたくない」
↓
泣く
↓
足を洗う
↓
ポテチを食う
↓
(ﾟдﾟ)ｳﾏｰ
0060デフォルトの名無しさん
NGNG0061デフォルトの名無しさん
NGNG>>60 なにそれ？変な奴
0062デフォルトの名無しさん
NGNG何処へいっても春厨だらけ。
006356
NGNGなんか間違いあったら適当に直しといてね。
んじゃ
0064デフォルトの名無しさん
NGNG006556
NGNG0066デフォルトの名無しさん
NGNG006756
NGNG「プログラム言語理論への招待--正しいソフトウェアを書くために」,Bartrand Meyer,二木厚吉(監訳),酒匂寛(翻訳)
http://www.amazon.co.jp/exec/obidos/ASIN/4756103170/qid%3D1017229588/249-9598832-5139562
ってのしか知らない。中身は、プログラム言語意味論。
0068デフォルトの名無しさん
NGNGそれはプルグラム言語の話ではなくて？
おれはもっと要求定義を形式的にやるような学問があるのかと
思ってたけど、ちゃいますか？
006956
NGNGCMM方面とか、ユースケース駆動方面で、
その重要性が認識され始めたけど、
まだ分析・設計手法ほどメジャーになっていないみたい...
>>59 ってユースケース記述？
0070デフォルトの名無しさん
NGNGむしろ萌え萌えな感情を掻き立てるものであるべきと思うですが。
007156
NGNGなんででしょうね？
漏れは昔から、計算論とか意味論とか萌え萌えなんで、
Formalizmって言葉に違和感はないけど。
かくいう漏れも、UMLは便利だと思って前からよく使ってたけど、
「開発方法論」とか「形式仕様記述」の方はつい最近まで、
「(自分の守備範囲ではどーせ)使いものにならん」とか
勝手に決め込んで、封印してたんだけど。
あと、答え忘れてた、、、
>>68 >>67の本は、
プログラム言語意味論の形式的記述≒形式仕様記述って立場で、
意味論の勉強しといてくれよって目的で、翻訳されたんだと思う。
前書きに酒匂＠SRAさんが、そんなような事書いてた。
0072デフォルトの名無しさん
NGNG日々の仕事においてやっている作業の類似性になんとなく
気が付くものの、それをどう統一した方法で扱えばいいのかを
考えると全然分からなくなる。そういうのは多くの人が思ってる
ことなんじゃないかな。かといって今のままでいいとはとても
思えない。反復的開発なんてやっている人なら分かると思うが
手探りでなんらかの答えを導きましょうという考えには変りない。
個々人の経験に大きく左右されるようなもの。危険です。
おれも上のリストからどれか勉強します。
00731じゃないけど...
NGNG＞手探りでなんらかの答えを導きましょうという考えには変りない
まずは軽〜く、一通りの処理が流れるように作って、
仕様変更や設計変更の余地を残しておき、
それからマターリと細部を作るという感じではないかなー。
0074デフォルトの名無しさん
NGNG0075デフォルトの名無しさん
NGNG0076デフォルトの名無しさん
NGNGまず､FDTはごくごく限られた単純な（綺麗な）ターゲットでないと使えない。
実用アプリだと形式仕様を書くほうが実際のコーディング以上に大変。間違えるし。
たとえばWindowsをFDTで設計すりゃ良さそうなもんだが､そんなことはできない。
ついでながら､検証しか目に入ってない研究者が気がつかないのは､現場の誰が形式仕様
記述と検証をするのかということ。作るだけでも精一杯なのに､そんな余剰人員はおらん。
次に､FDTの研究が世の中のアプリを主導しているのでは決してなくて､アプリが常に先行して
先端アプリを検証するためにFDTが研究されるという後追いになるから､研究の目処がついた
ころには､そのFDT手法で検証できるアプリはすごい時代遅れのものになってしまう。
結果的に一番検証したいものが検証できない。
もちろんFDTを全否定するわけではないが（自分の首がしまるしな）､FDT研究者の多くは
自分で実用プログラムを書いた経験がほとんどなく､FDTの理論世界に閉じこもっている。
それが一番の問題。
0077デフォルトの名無しさん
NGNGExecutable UML とか MDA みたいな技術については
どう捉えられているんでしょうか？
OMGとか Rational は、UML+Action記述を、
第一級のプログラミング言語に仕立て上げたがっているようですが…
0078デフォルトの名無しさん
NGNGhttp://pvs.csl.sri.com/
使ってる人いますか？
0079デフォルトの名無しさん
NGNG興味はあるけれど、まだホームページちらっと眺めただけ。
高いの？便利？特徴は？
(勝手に)義兄弟スレ【Verilog,VHDL等のＨＷ記述言語のシミュレータ 】
http://mentai.2ch.net/test/read.cgi/sim/981553632/
＃もしかして、ExecutableUMLって、
＃ハードウェア記述言語とかの影響下から出てきたのかなー？
＃あっちの分野は、それなりに実用に使われているよ、ね？
0080デフォルトの名無しさん
NGNG読めるものは皆無ですよね。やっぱり英語の本を買うしかないかな？
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
これらの中でお勧めの一冊とかあれば教えてください。
0081デフォルトの名無しさん
NGNG3. Handbook of Process Algebra が一冊あれば事足りる．高いけど．
初心者なら 2. Introduction to Process Algebra が読みやすいです．
008280
NGNGうぉ、どうもありがとう。ところで、
こういうの大学の授業にもぐりこんで勉強したけど
都内でどこかいいところ知りませんか？
008380
NGNG0084デフォルトの名無しさん
NGNG漏れはハード屋だが､形式仕様記述なんかしてるハード屋は見たことないよ。
HDLは設計とシミュレーションのために使うもの。
まあ何をもって仕様と言うかにもよるけど､仕様記述を目的にHDLを使うハード屋はいないよ。
0085デフォルトの名無しさん
NGNGいや、もふこのスレは形式仕様記述なんてものは対象に入ってないでしょ（ｗ。
プログラム仕様の形式記述というところを理解するだけで精一杯というか。
0086デフォルトの名無しさん
NGNG>漏れはハード屋だが､形式仕様記述なんかしてるハード屋は見たことないよ。
Intelがやってたはず。どっかの学会でしゃべってた。
Pentiumとかのバグでこりたらしい(w
0087デフォルトの名無しさん
NGNGあー分かった､それは仕様記述のことじゃなくて､モデルチェッキングを使った機能検証だね。
でもモデルチェッキングもほとんど普及してないよ。
ハード界で一番普及してるのは等価性チェック。CADの入力と出力の等価性をチェックするため。
どっちにしても大LSIメーカでやっとあるかなというレベルだから､一般に普及してるなんてとてもとても。
0088デフォルトの名無しさん
NGNG放置状態でいたら、痛い所をつかれてしまった。
>>85,>>87
「形式仕様記述」と「プログラム言語の仕様記述」
「形式仕様記述」と「モデルチェッキングを使った機能検証」と「等価性チェック」
の違いなど簡単に説明していただけると助かりますです、はぃー
0089デフォルトの名無しさん
NGNG0090デフォルトの名無しさん
NGNG0091デフォルトの名無しさん
NGNG学部の授業で形式仕様を扱っている大学という意味ですか？
ちょっと聞いたことがないですね．都内に限らず．
0092デフォルトの名無しさん
NGNGできないものかなぁ？インターフェイスだけじゃ動作の
互換性なんて、実際に動かすまで分からんし。
0093デフォルトの名無しさん
NGNGinvariant conditionやら、すべて記述するのはｶﾅｰﾘ面倒だが。
0094デフォルトの名無しさん
NGNGプロセス計算とかホーア論理なら、前は東大の理学部情報科学科で学部の３年生や４年生に
教えてたけど、まだやってるのかなあ？ もちろんみんな爆死してたけど…
009586
NGNG「形式仕様記述」⊃「プログラム言語の仕様記述」
「形式仕様記述」⊃「モデルチェッキングを使った機能検証」⊃「等価性チェック」
だと思った。モデル検査をするには満たすべき性質（＝仕様）を与えないといけないし、
等価性チェックをするにも等価になるべき相手（＝仕様）を与えないといけないし。
87は何か特定の種類の「仕様記述」が念頭にあったと思われ。
0096デフォルトの名無しさん
NGNG実際にプログラム組んでテストするより難しいのは、
だめだってことだよね。しかも習得に異様に時間がかかる。
0097デフォルトの名無しさん
NGNG0098デフォルトの名無しさん
NGNG習得が大変（つーか普通のプログラマには無理？）なのは事実だと思う。
ただ「実際にプログラム組んでテスト」だと、あくまで有限（一部）の
入力についてしかテストできないけど、ホーア論理とかなら無限（全部）の
入力について検証できる。
だから、「実際にテストするよりも難しい」と直ちに
「形式的仕様検証 ＜＜＜ 実際にテスト」といえるわけでもない。
あと、プログラムの完全な仕様じゃないけど、配列の添え字とか例外処理とか
一部だけ検証するなら、http://research.compaq.com/SRC/esc/みたいな
もっと「お手軽」なアプローチもある。
>>97
数学というか記号論理学と思われ。∀とか∃とか∧とか∨とか¬とか、
そういうの（笑）。
009998
NGNG(・∀・)
0100デフォルトの名無しさん
NGNG最近それに見えてしまって困ってるんです（まじ深刻
0101デフォルトの名無しさん
NGNG0102デフォルトの名無しさん
NGNG0103デフォルトの名無しさん
NGNGやめてくれ、これからそういう記号を扱う講義があるんだから…（笑）
0104デフォルトの名無しさん
NGNG0105デフォルトの名無しさん
NGNG010687
NGNG面白すぎ。けっこう使えるような気がする（笑
>>88 >>95
しばらく見てなかったんで遅レススマソ。
なんにせよ､仕様って何のことなの？､ってのをはっきりさせないと話が混乱するよね。
とくにrefinementする場合は､ある段階の実装が次の仕様になったりするんで､何が仕様で
何が実装かは相対的なものだし。
形式言語とプログラミング言語の違いって何？､ってのもある。プログラミング言語だって
考えようによっては形式言語の一種（曖昧な自然言語ではなく､意味がそれなりに一意に
定まって論理との対応も可能な言語という意味合いで）だから。
閑話休題。
それで､言語として何を使うかは別として､｢仕様｣としては関数や回路コンポーネントの
入出力関係に関する何らかの記述､｢実装｣としては関数や回路のコーディングしたものを
指す､という定義のもとで､
｢仕様記述｣はあくまで仕様を形式言語で書く行為､｢モデルチェッキングや等価性｣は仕様
と実装の関係を検証する行為と漏れは認識しております。
モデルチェッキングは仕様として実装の動的性質（の一部ないし全部）が与えられたとき､
それが実装において成立するかを調べること（論理学的には別の意味合いがあるが､ちょ
っとそれは置いといて）。等価性検証は､仕様としてはrefinement前の中間実装（たとえば
ハードならRTL）がおもな対象で､その動作とrefinementされた実装（たとえばハードなら
ネットリスト）の動作が同じかを調べること。こちらは静的手法でかなり調べられる。
別種の議論として､仕様それ自体があっているかというのも問題だけど､現場的にはそこま
で形式手法でやるのは手が回ってない。
まあ､単に仕様を書くだけではなくて､書いた仕様から実装が導出できるなり､形式検証が
できるなりのメリットがないと､わざわざ形式仕様記述する意味は少ないかと。
あと､数学の関数みたいな演算処理なら仕様として入出力定義を明確にかけるし論理との
相性もいいけど､世の中のソフトやハードの大半ってそういうものじゃなくて､何かのプロ
トコルとかプロセス制御とかシーケンス制御が多いからねえ。そういうのだと､形式仕様
を精密に書いているうちにコーディングとあまり変わらなくなってしまって､それなら最
初からコーディングすればいいじゃん､となってしまう事情もあるよ。
0107デフォルトの名無しさん
NGNG0108デフォルトの名無しさん
NGNG形式仕様の話とは無関係ですまそ。
0109デフォルトの名無しさん
NGNG> Flow-Sensitive Type Qualifiers
> Jeffrey S. Foster, Tachio Terauchi, Alex Aiken (University of California at Berkeley, USA)
なんかどうよ？ 型システムに基づく静的検証で、Linuxカーネルのバグをいくつか見つけたらしいぞ。
ロックまわりとか。検索したらwebにも論文があったような。なんか定式化が微妙に変だったけど…
（Aikenがちゃんとチェックしなかったのか？）
0110109
NGNGこの人、どういう人なんだろ。聞いたことがなかったんだけど。
PLDIに行けば会えるんだろうけど、うちにそんな金はねえ…
0111デフォルトの名無しさん
NGNGああ、俺、それ聞いたよ。
特にbuffer over runなどの境界条件に起因するバグを見つけられるそうな。
0112デフォルトの名無しさん
NGNGこれってどんな団体なんですか？
0113デフォルトの名無しさん
NGNGACMっていうコンピュータサイエンスの国際学術団体の中の、
SIGPLANっていうプログラミング言語の専門研究部会が主催してる、
学術会議の一つ。毎年一回、これぐらいの時期に開催される。
http://citeseer.nj.nec.com/impact.html
なんかを見ても、レベルは高い。
論文の採択率はいつも20%ぐらい（＝5本に1本しか通らない）。
日本からだと、IBMの基礎研がJavaの関係でよく頑張ってるような気がする。
0114仕様書無しさん
NGNG>>109
Linuxのバグを見つけるなんてすごいね。頭のいい人はいるもんだな。
おれも興味ある。勉強してみようかな。でも自分で作ったカーネルの
デバッグが出来ないとかいう頭の悪そうな動機じゃだめかもね（ﾜﾗ
0115デフォルトの名無しさん
NGNG>>114みたいな動機を思いっきりこき下ろした「つかみ」書いてたっけ
0116ミスター３
NGNGNHKの教育番組は最高だがね〜
あどけない女の子がいっぱいだがね〜
興奮してローソクが垂れちゃっただがね〜
汚しちゃっただがね〜、ヒヒヒ・・・
漫画、読んだ事ないので文章が間違ってたら
すんまそん。
http://www.h4.dion.ne.jp/~k.seed/index.html
0117デフォルトの名無しさん
NGNG0118デフォルトの名無しさん
NGNG0119デフォルトの名無しさん
NGNG0120デフォルトの名無しさん
NGNGFormalApproachの中心人物で VDMの開発者でもある
Bjorner先生の論文が載っていたのであげ。
0121デフォルトの名無しさん
NGNG少しは勉強が進んだかね？
0122ちょっと疲れてまして、支離滅裂でしたらスマソ
NGNGガッコに居た時からの懸案なのですが、進んでません。
「証明的プログラミング」とか「構成的プログラミング」には興味があったのだけど、
形式仕様記述をやるモチベーションが足りなくて...。
最近Lyee上司は、KMとか言い出しちゃってて、
＃それはそれで「ソフトウェア再利用」「ソフトウェア部品」よりは幾分ﾏｼなんだけど、
KMの限界とか突破口とかを見極めようと四苦八苦しているのが、現状です。
0123ちょっと疲れてまして、支離滅裂でしたらスマソ
NGNG0124デフォルトの名無しさん
NGNGビジネス系の開発現場で、OCL使っている方いますか？
実開発でiContractとか使いたいのですが、使った経験のある方とかいます？なんかハマりそうなのですが。
0125デフォルトの名無しさん
NGNG0126デフォルトの名無しさん
NGNG0127デフォルトの名無しさん
NGNGなんか形式仕様の話は大抵がプログラムの構成まで、せいぜいバグ取りまでで、
その後に控えてる長〜い保守についてはあまり語られてないような気がするのだが。
0128デフォﾉﾚトの名無しさん
NGNG0129デフォルトの名無しさん
NGNGHandbook of Process Algebraを注文しましたー。
でもひとりで勉強出来るか心配です。
なにかお勧めのニュースグループなんかはありますか？
0130渡邊克宏
NGNG確かに仕様記述に入門する前に、formalの世界の基礎となるいくつかの事項を学ぶことができる本です。
一方で誤りが非常に多い本です。原書からしてそうですし、翻訳にも多数の問題点を発見しました。
具体的には以下のページをご参照ください。
ttp://katsu.watanabe.name/review/intro_theory.txt
この本は、徐々に積み重ねていったことを、クライマックスとしてハノイの塔のプログラムの正しさの証明で
花開かせる構成とみてとれます。ところが、なんとそのクライマックスの証明が完全な誤りなのです。
真面目な学習者ほどがっかりするのではないかと心配です。その一方で、誤りに気をつけてさえ読めば、
クライマックスまで話の筋が見えやすいので面白く基礎が学べるんじゃないかと思います。
訳者の酒匂寛さんは、訳本の出版当時私の直属の上司だったのですが、
「Knuthっぽく、一箇所間違い見つけるごとに10円出そうか？」なんて言っていました。
上のページをまとめたあとで、「あの10円という話は本当ですかぁ？」とツツいてみたら、
本当に10円*約300箇所=三千なにがし円を下さいました。一箇所ごとに倍という話に
しておけば、2^300だから、えーと...新しいノートパソコンとかが買えたかな。
0131デフォルトの名無しさん
NGNG神ｷﾀｰｰｰｰｰｰｰｰｰｰｰｰｰｰｰｰｰｰ!!!!
この本は間違いが多いので、代替としてお勧めできるような本って
ありますか?
0132NetBSD房
NGNGhttp://pvs.csl.sri.com/
関係者というわけじゃないけど、
最近使い始めたので、密かに宣伝。。。
0133デフォルトの名無しさん
NGNG0134デフォルトの名無しさん
NGNG0135名無しさん＠Ｅｍａｃｓ
NGNGここのみなさんはどうやって勉強してるの？
それとも大学に残ってるような人がこのスレに
書き込んでたとか？
どうも取っ掛かりがつかめなくてねえ。
上に書いてあるPVS3.0をemacsにインストール
してみたけど、これ慣れるまでに1,2ヶ月ぐらい
かかりそう。サイトにもまともに使えるように
なるのに半年とか書いてあるし。。。
0136名無しさん＠Ｅｍａｃｓ
NGNGだめだなあと思って、>>130さんの言っている
プログラミング言語理論への招待を再び読み始めました。
初等数学、抽象構文、形式意味論入門、λという5章までを
なんとか理解しようと何回も読んで問題解いたりしてます。
本を半分にぶっちぎって仕事中も読んでます（藁
ところでこれの演習問題の模範解答ってどこかに
ないかな？ちまちま生成規則を書いたりしてるのは
いいんだけど、どうもあってるかどうか自信無し…
海外のサイトでもいいのでもしあれば教えてください。
自分でも探したのですが、見当たりませんでした。
またはこれに似たような本で大学のテキストとして
使われている（答えも公開されている）ようなものが
あればおしえてください。
0137デフォルトの名無しさん
NGNG和書だと岩波『計算モデルの基礎理論』とか共立『プログラム意味論』とか。
0138名無しさん＠Ｅｍａｃｓ
NGNGそれって演習問題とかついてます？
章末の問題ってアホウのしりを叩いて
くれるから良いんですね（藁。
計算モデル〜は絶版でした。。。
横内さんの本は前になんかのスレで
よい本だと書いてあったような。
帰りに本屋さんに行って見て来ます。
それにしても独学はしんどいですね。
自分でなんらかの処理系を書かないと
ものにならないのかも。ってかこれは
学生も同じか。
学部生はどんなもの作るんでしょうか？
0139デフォルトの名無しさん
NGNG演習問題はどうだったろう。覚えてない。
つーか数学の本を読むときは演習問題を解くよりも
そこに載ってる証明を何も見ないで再構成できるようになるまで
完全に把握する方が良いと思われ。
それから先は実装みたいな具体的な問題に取り組んで、
そこで分からない点を解決するために専門書とか論文とかを探して読む。
0140名無しさん＠Ｅｍａｃｓ
NGNG>そこに載ってる証明を何も見ないで再構成できるようになるまで
>完全に把握する方が良いと思われ。
なるほど。ちなみに今読んでるMeyerさんの本は日下部氏の
「作って分かる〜」みたいなノリなんですよね（藁。
数学的に詳細な説明が必要だと思われるとこでは、
これこれについてはこの論文でって形で逃げる。
簡単な数学は使われているけど数学それ自体に
ついては何も書かれていないんです。
だからおれみたいなどきゅそでもなんとか読めるんだけど。。。汗
もう少し突っ込んで勉強するにはちゃんとした工学書や論文を
よまにゃならなそうですねえ。まぁ来年の話ですが。
勉強のヒントになりました。ありがとうございます。
Meyerさんより簡単な本は無さそうだということで、
まずはこれを暗記するぐらい読んでみたいです。
0141名無しさん＠Ｅｍａｃｓ
NGNGみなさん論文はどうやって探されていますか？
やっぱりgoogleですか？何かコツのようなものが
あれば、、、教えて欲しいです。
正直、今読んでる本のお勧め論文、古すぎて検索
しても出てきません（T_T
0142デフォルトの名無しさん
NGNG学外の人間の閲覧がどれくらい可能かは大学による。
近くの公立図書館に相談するのも手。
0143名無しさん＠Ｅｍａｃｓ
NGNGそれは知りませんでした。今度都内の図書館どっか行ってみます。
さーてとそろそろ帰ります。横内さんの本あるかな。
今日は色々とありがとうございました。感謝です。
0144デフォルトの名無しさん
NGNGいやできるかどうか分からないけど、相談するならまず公立図書館だということ。
大学は国とかワタクシなので公図−大図にネットワークががあるかは不明。
その次に大学の図書館に問い合わせ、それでも駄目なら、
専門家を探して丁寧な相談の手紙を大学宛に郵送するというのも考えられる。
最終手段としては聴講生になるという手がある。
厳密にいえば論文の複写は合法ではないので
こういうややこしいことをする必要がある。
0145名無しさん＠Ｅｍａｃｓ
NGNGどうもです。まだ図書館にも行ってないし横内さんの本も買ってません。
なぜなら、Meyer本なかなか読めません。8章の再帰的定義が使える条件
みたいなのを調べるのに不動点方程式を使っているあたりでつまずいた
ままなのです。なにいってんだかさっぱり分かりません。マジ脂肪です（汗
もう少しねばってみます。
0146デフォルトの名無しさん
NGNG0147デフォルトの名無しさん
NGNG0148デフォルトの名無しさん
NGNG倉田令二朗先生の数学基礎論シリーズ嫁
基礎の前に応用やっても意味無し
全巻読んでから出直して来い
0149デフォルトの名無しさん
NGNG河合のシリーズは助けにならんつーか基礎づけの目標が違う
01501
NGNG0151デフォルトの名無しさん
NGNG数理情報学入門 スコット・プログラム理論
朝倉書店 数理科学ライブラリー３
なんてどうでしょうかね？
0152デフォルトの名無しさん
NGNG悪くないが、それならこの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)
0153デフォルトの名無しさん
NGNGBarendregtの本は少し高い。
http://www.cs.kun.nl/~henk/papers.html
ここにあるのをいつくか読んでから考えた方がいいかも。
おれもいま読んでます。
0154デフォルトの名無しさん
NGNGおもしろそうだけど The lambda calculus を買うための
判断材料にどれだけなるかはちょっと疑問
0155デフォルトの名無しさん
NGNG0156デフォルトの名無しさん
NGNG0157デフォルトの名無しさん
NGNG155 は 100 スレくらい上げ荒らしした奴だよ。単に。
0158デフォルトの名無しさん
NGNG0159デフォルトの名無しさん
NGNG>>152 が挙げてる本の邦訳は多分ないと思う。
まだ挙がってないのだと丸善「形式的モデルと意味論」とか。
古い本では伊藤貴康「プログラム理論」(コロナ社)というのもある。
前者はサーベイ集、後者は入門書。どちらも証明は少ない。
0160デフォルトの名無しさん
NGNGhttp://www.maruzen.co.jp/cgi-bin/mis?Cgifrom=m2-ezy-03&MBN=MJ94008073&Dbs=MPW
＃だいぶ前に、bitでネタになってたような
0161デフォルトの名無しさん
NGNG> この第二分冊？
そうそう
> ＃だいぶ前に、bitでネタになってたような
そりゃえらく前だな
0162デフォルトの名無しさん
NGNGこういった議論にどんな風に基礎論が関わってくるのでしょうか？
0163デフォルトの名無しさん
NGNG0164151
NGNG続 新しいプログラミングパラダイム 共立出版 1990
を読んでいたら，
「第４章 抽象データ型とOBJ2 （二木厚吉・中川中）」で
代数的仕様記述法の解説がありました．
0165デフォルトの名無しさん
NGNG0166デフォルトの名無しさん
NGNG0167デフォルトの名無しさん
NGNG0168デフォルトの名無しさん
NGNGpvs 3.0 release age
0169デフォルトの名無しさん
NGNG0170デフォルトの名無しさん
NGNG結局社会の言い成りか。マスコミに煽られてビビってるようじゃ駄目だな。
0171デフォルトの名無しさん
NGNG管理者にとって訴訟リスクが多すぎるので、消滅
0172デフォルトの名無しさん
NGNG0173デフォルトの名無しさん
NGNG0174デフォルトの名無しさん
NGNG0175デフォルトの名無しさん
NGNG２ちゃんねるのお勧めな話題と
ネットでの面白い出来事を配送したいと思ってます。。。
===============================読者数： 138720人 発行日：2003/1/9
年末年始ボケがそろそろ収まり始めた今日このごろのひろゆきです。
そんなわけで、年末に予告したIP記録ですが実験を開始しています。
「２ちゃんねる20030107」
こんな感じで各掲示板の最下部に日付が入ってるんですが、
20030107以降になってるところはログ記録実験中ですー。
んじゃ！
────────────────────────Age2ch─
■この書き込みは、Age2chを使って配信されています。
────────────────────────────
Keep your thread alive !
http://pc3.2ch.net/test/read.cgi/software/1041952901/l50
────────────────────────────
0176デフォルトの名無しさん
NGNGクッキーとアクセスログの参照を有効にしる！
0177デフォルトの名無しさん
NGNGMオナニーヨヨイ
0178デフォルトの名無しさん
NGNGいつも早朝つか明け方に現われるだよ＜ＴＳＢ
このまえの隊長とのボクシング試合のときも、Kityと絡んでたｗ
0179デフォルトの名無しさん
NGNG呼びました？
0180デフォルトの名無しさん
NGNG「2ちゃんねるはボランティアの削除人が書き込みをチェックして、
好ましくない書き込みを一所懸命削除している、
ということになっているが、あれはウソ。
削除人には給料が支払われ、その給料の原資となっているのが、
まずいことを書き込まれた企業が削除要求とともに渡す裏金。
これはまさに、総会屋の構図そのものだ。
これまで裁判になっているのは金額で折り合えなかったり、
裏金を出さない強い態度の企業とだけだ」
0181デフォルトの名無しさん
NGNGモルモット＋金蔓
0182デフォルトの名無しさん
NGNG名前欄に半角でfusianasann
0183デフォルトの名無しさん
NGNGボケと突っ込みわかる人 キター
0184デフォルトの名無しさん
NGNG0185デフォルトの名無しさん
NGNG0186デフォルトの名無しさん
NGNG0187デフォルトの名無しさん
NGNG0188デフォルトの名無しさん
NGNGそういうところが訴えてきそうで怖いな
ちびくろサンボを差別だ、といったりカルピスの黒人が描いてあるラベルを
問題だと騒ぎ立てるような連中だからな
0189デフォルトの名無しさん
NGNG２ちゃんねるのお勧めな話題と
ネットでの面白い出来事を配送したいと思ってます。。。
===============================読者数： 139038人 発行日：2003/1/10
なにやら、連日メルマガだしてるひろゆきです。
そんなわけで、ログ記録実験ですが、いちいちサーバ指定するのが面倒なので、
全部のサーバに入れてみました。
重くなって落ちたりしてもご愛嬌ってことで。。。
んじゃ！
────────────────────────Age2ch─
■この書き込みは、Age2chを使って配信されています。
────────────────────────────
Keep your thread alive !
http://pc3.2ch.net/test/read.cgi/software/1041952901/l50
────────────────────────────
0190デフォルトの名無しさん
NGNG0191デフォルトの名無しさん
NGNG0192デフォルトの名無しさん
NGNG198 ：ひろゆき ◆3SHRUNYAXA ：03/01/11 05:48 ID:kSb7xo24
ふ、、勝てば官軍。
199 ：マァヴ ◆jxAYUMI09s ：03/01/11 05:49 ID:ScPwdn5W
そういうヤツなんだよな(^_^;)ひろゆきって
0193デフォルトの名無しさん
NGNGそれを勝手にネットに広めていいとは限らない。
0194デフォルトの名無しさん
NGNG0195デフォルトの名無しさん
NGNG誰もナマのカキコを見てないし
それについての議論もされていないことから
ネタだと思われる
0196デフォルトの名無しさん
NGNGIPを記録されると絶対に個人が限定されるのですか？
0197デフォルトの名無しさん
NGNG被害の大きさに差がありそうだけども。
誹謗中傷一番垂れ流しってどこかねぇ？
0198デフォルトの名無しさん
NGNG今日午前４時前、幸田駅の線路脇の道路でキャッチボールしていた中学３年生４人組がいた。
ところが、ボールが線路に入った。
幸田駅の線路に、ボールを取りに入った、中学３年生の女子１名が、貨物列車に
ばばばばばピィー― きゃ〜！ ブァプアあああああああー―――――――ン！！！！！！
0199デフォルトの名無しさん
NGNG0200デフォルトの名無しさん
NGNG0201デフォルトの名無しさん
NGNG代理人たる弁護士がやりゃ十分と違うか？？
0202デフォルトの名無しさん
NGNG0203デフォルトの名無しさん
NGNG0204デフォルトの名無しさん
NGNG0205山崎渉
NGNG218.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
0206山崎渉
NGNG0207デフォルトの名無しさん
NGNG0208山崎渉
NGNG0209デフォルトの名無しさん
NGNGForamlMethodをやってるひとはどこに生息してるの？
それとも一般ユーザーはもうなかったことにしたいのかな？
0210山崎渉
NGNG0211デフォルトの名無しさん
NGNG0212デフォルトの名無しさん
NGNGはっきりしちゃったよね。結局ソフトウェア業界なんて
計算機科学の基礎的な知識のない人が過半数を占めているわけで
いくら有用なツールが出てきたところで、その辺りの人が
使えなければ意味ないよね。萩谷先生なんかも生物学とか
そっちにいっちゃったしなあ。もう終わりかね。終わらないにしても
仕事とは関係のないものかな。
0213デフォルトの名無しさん
NGNGそういった状況は、実際の開発現場からあがってくるので、大学の研究室に閉じ籠って研究している段階から移りつつある鴨。
0214デフォルトの名無しさん
NGNGでもどうだろう。
ソフトウェアの規模がでかくなるとそれに比例して
検証もむちゃくちゃ大変になるという。
そもそもそのような仕様記述ができると見込めるSEはどれだけいるのか？
0215デフォルトの名無しさん
NGNG0216デフォルトの名無しさん
NGNGもっと簡単に仕様記述できるツールや手法が開発されるで章。
それでも仕様記述できないSEは生き残れなくなるで章。
但し、それらの手法／ツールは現場に近い場所（大学の研究室でなく）で開発されるで章。
>>215
回路設計業界はソフトウェア業界に比べて健全な証拠
0217デフォルトの名無しさん
NGNGパリの地下鉄がよくあげられるけど
これってかなり昔の話だよね．
最近の例はないの？
0218デフォルトの名無しさん
NGNGんでもって予算少な目。これ最強。
0219デフォルトの名無しさん
NGNG初期に優秀な人材が集まらなかった⇒現在の管理職は糞⇒アフォな戦術の繰り返し
という事ではなかろうか。
回路設計業界は初期にもそれなりに優秀な人材がいたので現在でもそれなりに健全
0220デフォルトの名無しさん
NGNGあとセキュリティー方面。こういうのってやっぱり最後は天才の職人芸に
落ち着く気がするんだけど。
0221デフォルトの名無しさん
NGNGUML系の仕様記述言語oclをベースにしてる、らしいよ。(このスレ立てた当時の情報では)
0222デフォルトの名無しさん
NGNGそれは技術者の夢
0223デフォルトの名無しさん
NGNGもっとさ、カーネルの柔軟な構成のためにこういった手法が
なんか役にたたんものなの？いまの状態だとあっちを弄れば
こっちににも影響が出てって言う感じで、もうわけわかめ。
そこでマイクロカーネルが〜なんていったところで結局
モノリシックのパフォーマンスには絶対に勝てないし。。。
Linuxはもうカオスですなあ。それでもパフォーマンスだけは
下手によくて、*BSD,Solarisよりもいいからなあ。困ったもんです。
0224デフォルトの名無しさん
NGNG＞形式的仕様記述の産業界での応用例
いくとこいけばあるよ。例えばＮＡＳＡとか。
ＰＶＳ使った事例が結構あったよ。
0225デフォルトの名無しさん
NGNG＞結局ソフトウェア業界なんて計算機科学の基礎的な知識のない人が
＞過半数を占めているわけで
でも計算機科学（というかソフトウェアサイエンス）の基礎知識なんて
大したもんじゃないって。それにそんなのは論文書いて大学の先生に
なるためのもんだよ。例えば立命館の高山先生とか（笑）
＞いくら有用なツールが出てきたところで、
＞その辺りの人が使えなければ意味ないよね。
それはそうだね。
モデルチェッキングはツールとして有用な気がするけど
証明系はどうかな。
0226デフォルトの名無しさん
NGNG0227デフォルトの名無しさん
NGNG0228名無しさん＠Ｅｍａｃｓ
NGNG0229デフォルトの名無しさん
NGNGつか最近厨房だらけだよあそこは．はぁ〜
0230デフォルトの名無しさん
NGNGモデルチェッキングは有用。
証明系が神道するにはあと30年はかかるだろうな。
PVSなんかのプロトタイプ検証系にしても常人にはかなり辛いし。
証明系が使えると判断されて、それに対する教育コストを惜しまない
ような雰囲気が出てくることがまずは先決か。
0231デフォルトの名無しさん
NGNG＞PVSなんかのプロトタイプ検証系にしても常人にはかなり辛いし。
ＰＶＳをマスターすること自体は３ヶ月もあれば十分だよ。
難しいのは、証明すべき定理となる仕様を思いつくこと。
0232デフォルトの名無しさん
NGNG大変なわけではないよ。証明はプログラムでもあるわけだから。
0233デフォルトの名無しさん
NGNG>証明を書くのが大変だというけど、プログラムを書く以上に
>大変なわけではないよ
それはどうかな。Eiffelのassertionのようなものでも人は
難しい、かつめんどくさいと感じる。人がプログラムを組んでいる
ときに、全ての条件を想定しているわけではないという事実を
もっとよく見ておく考えておく必要がある。
0234デフォルトの名無しさん
NGNG＞Eiffelのassertionのようなものでも
＞人は難しい、かつめんどくさいと感じる。
＞人がプログラムを組んでいるときに、
＞全ての条件を想定しているわけではない
確かに。でもそれは言い訳じゃないかな。
ちゃんとデバッグする気があるんなら、
条件を想定するよね。全てとは限らないから
全部省略していいということにはならないよね。
わかっていることだけでも書かなかったら
なんにも情報がないよね。
0235デフォルトの名無しさん
NGNG0236デフォルトの名無しさん
NGNG>ちゃんとデバッグする気があるんなら、
>条件を想定するよね
時間がないということがいいたいんじゃない。ただ全ての条件を
想定するような仕事のためには別途どこかを削ってそれを割り当てる必要がある。
それはどこかと言えばテスト。assertionによってテストにかかる
工数を確実に減らせるということが認知されればいいんだけど、
なかなかねえ。そこにかかる時間の量と、その無駄の多さは誰しも
感じているところだろうけど。。。
少し大げさな話だけど、人文科学が実験できないという
意味で、ソフトウェア開発も実践を通して反省するという
点は同じかと。スパイラルモデルにしても一度やってみないと
その有効性は実感できない。それと同じで開発手法としての
Eiffelも試してみたいんだけどなあ。この不景気だと強気な
仕事より、失敗しない仕事が優先されるからね。そんなものは
とうてい無理か。
0237デフォルトの名無しさん
NGNG原因探索の無駄を省くとは思うが、「コード化」
だけを考えたら、直接の御利益はないかもね。
とはいえ、バグっても人が死なないシステムなら
ゴメンナサイとか謝っちまえばいいのか（笑）
0238デフォルトの名無しさん
NGNG制約条件をOCLで記述する iContract が流行っているらしい。(JavaWorldで既出)
単なるassertionだけでなく、実装コードを埋め尽くすつまんない条件分けコード
を一掃するのに使えれば、いいのかな？
0239デフォルトの名無しさん
NGNG下のFAQによると、複数のクラスにまたがるinvariants(invariants cross-cutting)
を扱えるようになるのがメリットらしい。
http://www.reliable-systems.com/tools/iContract/FAQ.htm
個人的には、複数のAspect間の干渉を排除するヒント情報として活用できたらいいと思った
0240151
NGNG意味論のノートがダウンロードできるみたいです．（試験問題も）
http://www.kurims.kyoto-u.ac.jp/~cs/csnyumon/
http://www.kurims.kyoto-u.ac.jp/~cs/lecture/
自分は情報系じゃなかったんで，テスト問題見てるといろいろ面白いです．
0241デフォルトの名無しさん
NGNGどの本がいいのでしょうか？
0242アシュル ◆adhRKFl5jU
NGNG何気に沢山あるので迷いますね
0243デフォルトの名無しさん
NGNG0244デフォルトの名無しさん
NGNGっていうかこれまで進歩らしい進歩があったわけでもないけど。
0245山崎渉
NGNG0246山崎渉
NGNG（ ＾＾ ）＜ ぬるぽ（＾＾）
0247デフォルトの名無しさん
NGNGなんで進歩しないの？
意味論の進歩が無意味になった（尽くされた）からかな？
＃無意味論しる！
0248山崎渉
NGNGﾋﾟｭ.ｰ ( ＾＾ ） ＜これからも僕を応援して下さいね（＾＾）。
＝〔~∪￣￣〕
＝ ◎――◎ 山崎渉
0249ハッカ飴
NGNGZ言語のサンプルもあるぞ！
ユニシス技報60
http://www.unisys.co.jp/tec_info/tr60/60home.htm
0250ハッカ飴
NGNGもう日本にZの本は存在しません。
唯一日本語で書かれた本がありましたが、絶版になりました。
Amazon.co.jpのデータベースには無いので、cbook24.comより
ソフトウェア仕様記述の先進技法 - Z言語
http://www.cbook24.com/bm_detail.asp?sku=00092314
0251デフォルトの名無しさん
NGNGいや、Zの本は多数あるよ。
学習参考書コーナーに行ってごらん。
0253ハッカ飴
NGNG洋書で。日本には0
0254デフォルトの名無しさん
NGNG0256デフォルトの名無しさん
NGNGでもそれだけでは何がなんだかよく分らんですねえ。
0258デフォルトの名無しさん
NGNGその本、Z言語の名前を始めて知ったきっかけだけど、
発売当時は浮世離れした象牙の塔の本、って感じて買い逃したな。
確か洋書を古本屋で入手したけど。
あと、Z言語以外の仕様記述言語本は、結構残ってる。
例えば、http://www.cutt.co.jp/book/index.html#Communication
ところで、Web上で、サハラ伸センセーの仕様記述レクチャーが始まったんで、あげ。
http://www.jfits.co.jp/column01/33.htm
0259デフォルトの名無しさん
NGNG0260デフォルトの名無しさん
NGNG二日間無料で見れるからの覗いて見てね。
http://angelers.free-city.net/page001.html
0261デフォルトの名無しさん
NGNG0262デフォルトの名無しさん
NGNGその辺りまとめてあるような本や論文ある？
0263デフォルトの名無しさん
NGNGhttp://upbbs.s2.x-beat.com/linkvp/linkvp.html
↑
ココは丸見え！ 今ならまだ消されてないよ。たぶん・・・
0264山崎 渉
NGNG__∧＿∧_
|（ ＾＾ ）| ＜寝るぽ（＾＾）
|＼⌒⌒⌒＼
＼ |⌒⌒⌒~| 山崎渉
~￣￣￣￣
0265デフォルトの名無しさん
NGNG0266デフォルトの名無しさん
NGNGなぜ、このスレにレスしてくれないのか、その理由が分った気がした。
0267山崎 渉
NGNG0268デフォルトの名無しさん
NGNGそれは本当に市場に受け入れられるだろうか？個人的には疑問が残る。
これだけ大きくなったIT産業を壊滅させるようなものは
到底受け入れられないのではないか。Lyeeに対する過剰な反応を見ていると
そんな気にさせられる。
アメリカは軍事産業を維持していくためだけに戦争をする。つまり
主要産業>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>戦争
なのである。2ch的な言い方でいえば。
IT産業にも同じように莫大な資金、人員が注ぎ込まれている。
これを、効率だけを追求した技術でもって、産業を縮小させるような
真似はできるはずもない。
IT産業を奴隷を使ったピラミッド製造になぞらえる向きがある。
だがしかし、それは巨大な産業が成熟期へと移行する必然的過程なのだろう。
ピラミッドは安定した権力の象徴。これを崩す何物も受け入れられない。
既におのおののポジションは決まっている。もうこの業界には夢はない。
自動車産業はフォードの開発したプロセスとともに始まった。
生産プロセスの改善そのものを肯定的に受け入れる文化がある。
だがしかし、この業界は不幸なことに、ソフトウェアの生産効率よりも
計算機資源の有効活用こそが至上命題という時代が長くつづいた。
未だにC系統の言語が広く使われている現実から見て、
悪しき文化は今後も続いていくことだろう。
インドのテニスコードの比喩で言えば、この業界の技術革新とは
ボール拾いの少年に対して、よりよい靴を開発することだといってよい。
0269デフォルトの名無しさん
NGNGはぁ、なんのことやら
最近は、このスレにも変な人が来てるのね
0270デフォルトの名無しさん
NGNG0272デフォルトの名無しさん
NGNGﾊｧ？奴隷を使ったピラミッド製造？
ピラミッド製造は、(ナイル川氾濫による)農閑期の雇用確保政策
であって奴隷労働とは違う、というのが、最近の定説なんだが。
そして、国内の建設業界やIT業界の最大の目的は、
効率化による利潤確保などではなく「雇用確保」な訳だが。
0273デフォルトの名無しさん
NGNG仕様記述で生産性向上
って方向に、強引に結び付ける貴方の真意が理解できませんが、何か？
生産性向上ｸﾞﾙｰﾌﾟの方ですか？？？
0274デフォルトの名無しさん
NGNG＞もともと文系板だしな
カオスだ株だと、痛いスレ立てまくるオマエさんにゃー、言われたくねぇよ(藁
0275山崎 渉
NGNG│ ＾ ＾ │＜これからも僕を応援して下さいね（＾＾）。
⊂| |つ
（＿）（＿） 山崎パン
0276デフォルトの名無しさん
NGNG形式的仕様記述のスレで生産性の話を始めたのは>>268
0277デフォルトの名無しさん
NGNGこのスレの上の方には「形式仕様記述」で検証する技術は、
まだハードウェア業界でも普及していない、とおっしゃる御仁も居る。
ハードウェア業界における検証と形式仕様記述の検証って、何が違うの？？？
ハードウェア業界：論理回路検証〜物理シミュレーション〜試作チップ検証
形式仕様記述： なんか高尚な事狙ってるのか？仕様からプログラム/ハードウェアを自動合成とか（ｗ
0278１
NGNG0279デフォルトの名無しさん
NGNG0280>>２ちゃんねらーの皆さん
NGNGhttp://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
0281○
NGNGあなたの欲しいものは何ですか？
あなたの欲しいものを調べた後に
ランキングで紹介します。
お一人様 ３品まで記入してください。
http://www.c-gmf.com/Quest.htm
0282デフォルトの名無しさん
NGNG「プログラミング言語で仕様記述する手法」と見なしてはどうか
と提案する人達が居るらしい・・・
そしてその意見には、漏れも禿同。
0283デフォルトの名無しさん
NGNGっていう3段階におおざっぱに分けたとして、
1,2は各プログラマの脳内と意思疎通に使われた紙切れ
しかないわけだけど、ある意味FREENIXなんかの開発では
普通に行われているよね。ただしそれは既に要求定義ががっちりと
出来ているからこそ。UNIXという概念、文化が先にある。
形式的仕様記述はそういったものとはなんの関係もないよね。
0284デフォルトの名無しさん
NGNGあと、仕様記述を通常のプログラミング言語で注意深く行った場合、
どんな相違があるのかなぁー？？？
子供だから（・∀・）ﾖｸ､ﾜｶﾝﾅｲﾔｧｰ!!!
0285デフォルトの名無しさん
NGNG0286デフォルトの名無しさん
NGNG0287デフォルトの名無しさん
NGNG0288デフォルトの名無しさん
NGNGJava + Eiffelのassertion + VDM
みたいなもんらしいですが.
0289そーいえばVDM調査で海外逝った人はどうなったの？
NGNGSSLプロトコルやらLinuxやら、はたまたEJBのセキュリティや仕様自体の曖昧さを、
形式仕様記述言語使って、実験的に検証した、とか聞くけど、どーなのよ？
VDMとかRAISE使うと出来るの？
ZやVDMじゃだめなんだろうね？
おまいらの情報、とっとと早く書けっ！！ほれほれっ
さもなきゃ形式仕様記述なんて、実用で使ってくれる所、滅多にないんだからさぁ
0290デフォルトの名無しさん
NGNGCafeOBJといえば学会でよくJAISTの人が発表してた。
なつかしいな。
0291デフォルトの名無しさん
NGNG0292デフォルトの名無しさん
NGNG0293BNF の思ひ出
NGNG> ## 今あなたは、このファイルをエディタなりで見ていますね。
> ## そういう方には、ヘルプファイルの形式をお教えします。
> ## 頑張れば、自分専用のヘルプ情報にできます。
> ## コントロールキーの割当ての部分を変えるとか、Ｃの関数の仕様を
> ## ヘルプファイルに入れてしまうとか、そういうことをやって下さい。
> ## 大変だとは思いますが、頑張って作って下さい。
> ##
> ## 【ヘルプファイルの形式】
> ## 形式は、通常のMS-DOS標準テキストファイルである。
> ## 内容は、改頁コード(0CH)で区切られたページの集まりである。ひとつの
> ## ページは、ページ名、見出し行、本文、制御行からなり、見出し行、本文、
> ## 制御行はなくてもよい。
> ##
> ## <ヘルプファイル> ::＝ {<ページ>}
> ## <ページ> ::＝ <ページ名>{<見出し行>}{<本文>}{制御行}<改頁>
> ## <改頁> ::＝ 0CH
> ## <ページ名> ::＝ <検索対象ページ名>|<非検索対象ページ名>
> ## <検索対象ページ名> ::＝ <頁区切文字1><30文字以内の文字列><頁区切文字2>
... 以下略
以上, 新松のヘルプファイル先頭より。
後になってこの説明が BNF またはその variant だと知った。
ヘルプファイル自體は(簡易?)ハイパーテキスト形式であった
(さう言や K3 は當時簡易 SGML フォーマッタも作ってゐたとか)。
尚, このヘルプファイルの先頭部分は後の松からは削除された。
「巫山戯た事を書いて怪しからん」と苦情を言った(或は苦言を
呈したのか?)顧客が居たからだと何處かで讀んだ氣がする。
眞僞の程は知らない。
通りすがりにスレ汚しスマソ。沈んで來ます。
0294デフォルトの名無しさん
NGNG0295ビヘービアコンパイラー萌え
NGNGやつら未だに仕様奇術＝実装が可能だと信じ込んでるぞ。
実務的にはRational MDAの出現でFAなのに、チョト可哀想。
0296デフォルトの名無しさん
NGNG0297sos
NGNGオカルト板で、バサバサ削除する削除人が
登場しています。こわいです。おそろしいです。SOS
http://qb2.2ch.net/test/read.cgi/sakud/1021962883/l50
0298デフォルトの名無しさん
NGNGこの認識は実務レベルでもドキュソだと思うけど
0299デフォルトの名無しさん
NGNGどーでもいいけど。
じゃ、なんか提案してみて。
0300デフォルトの名無しさん
NGNG>>295は、「多少は実用的な MDAですら 『仕様＋スクリプト』で実装コード生成してる
のに、今更『仕様奇術＝実装』はねぇだろ」っつう意図で書いたんだが。
まさか・・・「MDAで仕様奇術＝実装が可能になった」とか「MDA実用的でｻｲｺｳ」とか
読み違えてるわけねぇよな(ﾜﾗ
いずれにせよ、より良き提案があれば、あなたの意見を受け付けます。
提案ができねぇようなら、さっさと氏ね
0301いちおう一般人向けに解説しとくと
NGNG２ちゃん固有の煽り文句。生命を終了させろ、という意味とは違う
0302301
NGNG0303301
NGNG0304デフォルトの名無しさん
NGNG0306デフォルトの名無しさん
NGNGITU
0307
NGNGプログラムの解析だか正当性の検査にデータフローを追うみたいなやり方ありませんでしたっけ。
まえどっかでチラッとそんな内容の本を見た記憶があるんだけど題名が思い出せないんです｡
Amazonでそれらしき単語入れてもヒットしないし。
0308デフォルトの名無しさん
NGNGふりーえーじぇんと。
ま、ファイナルアンサーだと思うのだがな。
で、やつらは銀の弾丸を求めてるだけだからほっとけ。
0309あぼーん
NGNG0310デフォルトの名無しさん
NGNG0311デフォルトの名無しさん
NGNG0312デフォルトの名無しさん
NGNGなかなか面白そうですね。
システムＬＳＩ〜形式的手法の話まで触れていて、なかなか興味深いんで、早速買いました。。。
って、この本、１年前に発売されてたのね。。。
ウルシステムやオージスの本は知ってたけど、
キャッツの本、マジでこれまでずーっと目に止まりませんでした。
この本読んでおきゃ、去年一年無駄にせずに済んだものを。。。
あと、面白そうなのは、セマンティックWebで会社作って、星雲社からシリーズ本出してる人の本。
ここ数年、漏れが目標としながらなかなか形として実らなかったものが、着々と形になってきているんだな〜と強く感じた、春の夜。
0313デフォルトの名無しさん
NGNG形式的仕様記述と呼べる物なのか？おれは代数学を
使わないとそうは呼べないものだと思っていたが。論理で
ゴリゴリやるのもそう読んでいいかもしれんけど。
0314デフォルトの名無しさん
NGNG0315デフォルトの名無しさん
NGNG別にどう解釈してもえぇ〜んじゃねぇ〜？
仮にUMLが代数学と比べてショボい・低級なツールに見えるとして、
そのショボいツールで、LSI製造メーカがLSI設計しようとしているとしたら、
その意味はどこにあるのか、考えてみてはいかがでしょうねぇ。
0316デフォルトの名無しさん
NGNGどれくらいあるんでしょうね？
・旧鉄道総研系？
・証券のWebフロントエンドやってるあそこ
・SystemC＋UMLでツール作ってる↑あそこ
・組込系でExecutableUMLやってる所
・MDA周りは、形式的仕様記述ってのとは違うのかな？(大メーカ、大SIerもまだ模様眺めみたいですが。。。)
0317デフォルトの名無しさん
NGNGいやだからおれの言いたいのは、UMLはスレ違いなんじゃ
ないだろうかってこと。まあ過疎スレだから何書こうが
おれはどうでもいいけど。
0318デフォルトの名無しさん
NGNGSyntropy方法論でVDM使って形式仕様記述(つかHoare論理の記述なのかな？)したのが、
UML 1.1 Object Constraint Language 標準化の発端だとすれば、
OCL込みのUML、OCLと等価の仕様記述を持ったUMLも、形式仕様記述の一種と見ていいのではないかと。
後、Executable UML〜MDAの流れも。
あと、形式的仕様記述っつうと堅苦しく見えるけど、
Formal Method って言えば、いろいろバリエーションがある事は想像がつくでそ。
例えば、>>５６ のメモ参照。
どう思われますか。
0319デフォルトの名無しさん
NGNGあんたのレスは筋違い。
わかったふうなレスで、スレを荒らすな。
厨房はもう寝れ。
0320デフォルトの名無しさん
NGNG「人海戦術で厨房プログラマー集めて、雑多なシステムLSIを大量に設計させるのが目的。
それが可能になったら、高学歴高収入のLSI設計者はリストラしたい」、とかなんとかだったら、
日本の将来は暗いねぇ〜ｗ
0321デフォルトの名無しさん
NGNGttp://unit.aist.go.jp/informatics/ も入れよう.
>320
そもそも ITって、そんなもんでは?
「素人でも熟練者なみの○○ができる！」っていうか.
0322デフォルトの名無しさん
NGNGぁ、AISTのシステム検証センターね。関西だっけ？
ちょっと前まで、ポス毒とテクニシャンの募集してたっけ。
たしか、テクニシャンの任期が最長2年、なんでちょっと(ry
で、IT云々の件、
メーカや総研やSIerで なんちゃってSE/コンサルやるなら、
その程度の認識でも結構でしょうけどｗ
俺は、そんな程度の奴とはお付き合いしたくないなぁ〜
理学者が、概念整理して体系を作って、
工学者が、それを素人でも扱える対象に焼きなおして、
そうやって食い散らかされた挙句の
「一見うまくいきそうだが、実は落とし穴だらけ」な「単純作業の荒野」
で、素人労働者の皆さんに、いかにいきいきとクリエイティブな仕事をして頂くか？
という観点も重要なんぢゃないか、と。
0323デフォルトの名無しさん
NGNG高学歴高収入なエンジニアは（おそらく）クリエイティブな設計をする為の訓練を受けてない,
落とし穴をひとつひとつ潰していく（ある種のデバッグ）事が高学歴高収入なエンジニアの仕事 ⇒ 自分の首を絞め...
0324デフォルトの名無しさん
NGNGまっとうな学問的訓練の経験すら怪しい厨房プログラマ〜の方が、
ナンとやらも煽れば木に登る〜って感じで、オモロイ反応してくれるかもｗ
俺は厨房とは顔合わせるのもやだけどｗ
0325デフォルトの名無しさん
NGNGクリエイティブなLSI設計って、一体なんなんでしょう？
東芝-Sony-IBMのセル計画みたいなの？
それとも、いち早くMP3エンコーダ・チップや、MP4ビデオ・プレーヤや、新しい携帯電話付加機能を企画するような人の事？
はたまた、ヲズニアックみたく、シンプルで高機能な回路を設計する人の事？
よくわかんないっす。
マイクロ・プロセッサの開発：IntelとNEC (1970頃)
LSI設計のコンピュータ支援：(1970年代アメリカ)
DSPの開発： NEC (1980年代？)
PLDとかFPGAの開発： (多分海外っすね、これは)
とか見ると、日系企業では NECのクリエイティビティが結構高そうかなｗ
物性物理の新規分野開拓、てな意味では、日立とかNECとか、強いよね〜多分。
0326デフォルトの名無しさん
NGNGただ、昔と今とでは状況が違う。
昔は、開発に携わる事ができる人がほんの一握りであって、
そんな仕事に就くには（信用が必要なので）高学歴であったけど、
今では、開発が非常に多くなって高学歴職人が揃えられなくなった,,,
厨房でも設計できるツールが必要≒高学歴高収入は不要
クリエイティブは、個人の感性とか経験が大事なので、学歴はあまり関係ない，
芸術に近いものだと思う。
学歴が感性を磨いたり経験を積んだりするのに役立たない教育過程の指標な訳だし。
なんか、スレ違いなので、この辺で...
0327デフォルトの名無しさん
NGNG他人の作ったものをありがたがるんじゃなくて。俺仕様の
害悪とはまた別の話になるけど。
0328デフォルトの名無しさん
NGNGAISTはDQ法化してから商売に走ってるからなあ。
でもまだ武家の商法ってところはあるね。
鉄道信号の場合は国際規格との絡みもあるからな。
ヨーロッパのメーカは差別化のために形式仕様を
宣伝してるから日本がこれに追従できないとこれから
海外で商売する場合に困るのは確かだね。
で、モデルチェッキングくらいなら素人でもすぐ使えるよ。
SPINとかSMVとか只で使えるツールもダウンロードできるし。
AISTはSMVつかってるね。あれはCTLで仕様を書くのかな。
SPINはLTLだね。どっちがいいかは一長一短あるけど。
使ってみると面白いからやってみたら？
0329デフォルトの名無しさん
NGNGそれに、形式仕様って実はそんなに難しくないって。
今時は文系でも形式論理学教えてたりするからね。
一応修士修了の漏れがいうのもなんだけど
”高学歴”って確かに意味ないね。
クリエイティビティは学問の世界でも大事なはずだけど
実際には大学の教育はそういうこととは無縁なのは確か。
まあ、教育でどうこうできるのか？って疑問はあるけどね。
0330デフォルトの名無しさん
NGNG＞形式的仕様記述と呼べる物なのか？
＞おれは代数学を使わないとそうは呼べないものだと思っていたが。
ま、代数を使うかどうかは別として、UMLの場合
モデルが満たすべき性質を陽に記述できないんで
その意味では形式仕様の記述っていう感じではない。
（OCLとかいう言語で性質を記述するとかいう話もあるが
よく知らないので割愛。）
代数っていうのは例えばCafeObjみたいな
代数的仕様記述のこといってるのかな？
実は漏れ、あれのどこが代数なのか
よく分からないんだけど（笑）
0331デフォルトの名無しさん
NGNG論理学って、数理論理学以外は文系に分類されちまうらしいね。
それから、大学が、クリエイティビティを促進するか、阻害するか、は一概には決められないと思うよ。
そーゆーこと言う人って、いったいどこの学部/学科出身なんだろうね？情報系〜工学系？ｗ
>>330
UMLは、UML1.1以降のOCL込みで、形式仕様記述であろうとした、って感じだと。
0332デフォルトの名無しさん
NGNGいや、最近は文系でも数理論理学を教えてたりするよ。
大学がクリエイティビティを阻害するとは思わないけど
積極的に促進するって感じでもないでしょ。
もちろん、例外はいくらもあると思うよ。
そういうところにはがんばってほしいよね。
ちなみに漏れは理工系学部の情報系学科出身。
やってきたのは理論臭いことばっか。
だから漏れの見方も偏見に満ちてる。ｗ
0333デフォルトの名無しさん
NGNGそして、ExecutableUML〜MDA〜UML2.0で、ツールが自動コード生成するための、
グラフィカル・モデリング言語になったとさｗ
めでたしめでたし
0334フォーマリズムage
NGNG昼飯用に調理された弁当を、23時に食べても安全であるか否かという
前世紀初等に提出された有名な未解決問題。
0335デフォルトの名無しさん
NGNGセキュリティエンジニアリング
ソフトウェア開発者向けのページ
2. セキュアプロトコルと相互運用可能性確保
http://www.ipa.go.jp/security/awareness/vendor/software.html#2
0336デフォルトの名無しさん
NGNGあそこは結構腐ったネタを、文献調査してあとはせいぜいデモ・システム作って
研究と称してる感じがあるから、パスしときたいな。
いまどき、○×総研程度の連中ですら、
「検索エンジン使って情報集めるようなのは研究とは呼べない」だってさ。
連中がWebCrawlの研究開発に貢献した、という噂は一切聞いた事ないんだけどｗ
0337デフォルトの名無しさん
NGNG■ このスレッドは過去ログ倉庫に格納されています