おめぇら、形式的仕様記述について知ってる事を書け
■ このスレッドは過去ログ倉庫に格納されています
0001素人な部外者
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
■ このスレッドは過去ログ倉庫に格納されています