おめぇら、形式的仕様記述について知ってる事を書け
■ このスレッドは過去ログ倉庫に格納されています
0001素人な部外者
NGNGプログラムやプロトコルの仕様の、
フォーマルな記述方法っていくつかありますが、
どれくらい有効なんでしょうか？
形式的仕様記述を有効活用するには、
どんな知識が必要なんでしょうか？
おめぇーら、知っていることを書け！
0159デフォルトの名無しさん
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
■ このスレッドは過去ログ倉庫に格納されています