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