おめぇら、形式的仕様記述について知ってる事を書け
■ このスレッドは過去ログ倉庫に格納されています
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デフォルトの名無しさん
NGNG■ このスレッドは過去ログ倉庫に格納されています