- 1 名前：デフォルトの名無しさん mailto:sage [2013/01/05(土) 21:09:06.67 .net]
- スレがないので立ててみた
参考ページ
en.wikipedia.org/wiki/Formal_methods
ja.wikipedia.org/wiki/%E5%BD%A2%E5%BC%8F%E6%89%8B%E6%B3%95
- 15 名前：デフォルトの名無しさん [2013/01/19(土) 00:19:45.43 .net]
- >>14
なにが大差ないと言っているのかよくわからん。
- 16 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 01:08:35.95 .net]
- 費用や納期だけで評価したら大差ないってことでしょ
現状ソフトウェアの品質を正当に評価していない（できない）から
形式手法を導入するインセンティブが働かない
てかageる必要あんのか？
- 17 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 01:18:12.83 .net]
- >>15
とある情報システムを開発するのにかかるコスト
とか
予算や開発期間がオーバーするリスク
とか
- 18 名前：デフォルトの名無しさん [2013/01/19(土) 12:16:55.38 .net]
- >>11 >>14 >>17
確かに今までの形式手法ではそうだ。
論文を書きたいだけの奴にはそれでいいんだろ。
>>16
品質は費用納期に反映されるので、それは形式手法側の言い訳だ。
- 19 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 13:05:09.39 .net]
- >>18
論文と現場の乖離を示唆しながら
>品質は費用納期に反映される
はねぇだろ
営業や契約担当じゃないから実態は知らないが
発注元は
「フィールドバグ○件以下。超過した場合は違約金！」
とか契約文書に書けるの？
逆に請負側（候補）は
形式手法の適用が要件に入っていない案件で
「我が社は形式手法を導入しているのでちょっといいお値段です！」
で競争に勝てるというの？
「我が社で納期が短縮できるのは形式手法で開発の手戻りを低減するからです！
品質下げる訳じゃありません！」
とか発注元に説明すんの？
- 20 名前：デフォルトの名無しさん [2013/01/19(土) 13:53:26.32 .net]
- >>19
>「フィールドバグ○件以下。超過した場合は違約金！」
>とか契約文書に書けるの？
そりゃ書ける場合もあるよ。
それに、バグが多いと、当然後の注文もなくなってくるだろ。
>「我が社は形式手法を導入しているのでちょっといいお値段です！」
それは、顧客にとってのメリットを言っていないので、その時点でダメだよ。
>「我が社で納期が短縮できるのは形式手法で開発の手戻りを低減するからです>！品質下げる訳じゃありません！」とか発注元に説明すんの？
黙って短い納期でやればいいだけだろ。それは顧客にとってメリットだし、
こっちも短くなった分、他の仕事ができるし。
ほんとに使える形式手法とはこういうものなんだよ。
- 21 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 14:57:17.31 .net]
- 話が通じていないな
・ソフトウェアの品質を規定する統一的な指標がない
・既存の品質指標は開発手法に依存することが多い
（形式手法を適用した場合としない場合の公平な比較が困難）
・形式手法を要件に入れると対応できる業者が制限される
このため形式手法を導入するメリットが明確な「発注」がそもそも少ない
（メリットが明確なセーフティクリティカルやミッションクリティカルな案件では
現状でも形式手法が成果を上げている）
潜在的需要があっても表面上需要が無ければ
請負側に働く形式手法導入のインセンティブは弱い
- 22 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 15:15:19.07 .net]
- 請負側としては
同じ業者から大きな案件を頻繁に受注するケースは少ない
評判に期待して今回頑張っても次回の受注がいつなのかは分からない
いつ効果が表れるか不明確な投資はやりにくい
業界全体で評判になるほどの成果を上げるのは体力に余裕がないとできない
しかも形式手法が扱える業者は多くないが
形式手法だけで需要を独占できるほどの特殊性はない
- 23 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 15:23:25.33 .net]
- 請負側開発者・マネージャとしては
形式手法によりコストや納期を圧縮できるかもしれないが
勉強やらに費やした分だけ自分の給与が上がる保証はない
訳のわからない仕様書から解放されるといった
現場の幸せを要求しても経営判断には反映されにくい
- 24 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 15:44:33.85 .net]
- 高階関数とかのようなメタプログラミング機構がなくて言語としては貧弱なのも欠点
- 25 名前：デフォルトの名無しさん [2013/01/19(土) 16:08:35.77 .net]
- まあ今の形式手法の状況認識はそれでいいんじゃないか
>セーフティクリティカルやミッションクリティカルな案件では
現場にとってはそういうニッチなところで使うもので、
平凡な研究者にとっては、やればできると分かっている事をやれば少しは
論文が書けるというそんなものなんじゃないか？
それじゃつまらんけどね
- 26 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 19:06:51.37 .net]
- 新参で申し訳ないんだけど
形式言語で書いた仕様書は発注側が用意するの？
受注側が用意するの？
- 27 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 19:55:52.90 .net]
- 形式手法は商習慣まで関知せんよ
発注側「こういうもの作って」→受注側「言われたものを作りました」
という関係がものづくりとしては自然に思えるが
日本のICT業界は往々にしてこうはなっていない
上流で形式仕様を作成する場合
ユーザ企業はまずコンサル会社や大手ベンダに
「形式仕様作成と検証」といった発注を出すんじゃないかな
特に日本の場合は要求分析もセットになるかもしれない
- 28 名前：デフォルトの名無しさん [2013/01/19(土) 20:55:25.43 .net]
- C++の新規格のドラフトにaxiomsっていうのがあったんだけど
結局却下されちゃったんだよな
- 29 名前：デフォルトの名無しさん [2013/01/20(日) 18:35:51.46 .net]
- >>25
そっち方面の学界が腐敗とまでは言わんが競争がなく濁ってるんじゃないか？
だから一流人材が出て来ない。
- 30 名前：デフォルトの名無しさん mailto:sage [2013/01/20(日) 23:53:12.74 .net]
- >>29
ム板でいうのも何だけど
おまえ何様だよ
- 31 名前：デフォルトの名無しさん mailto:sage [2013/01/22(火) 23:33:47.71 .net]
- シンタックスはともかくセマンティクスにおいて
VDM++のまともな仕様って無いの？
曖昧さを持った言語で形式仕様記述とか欺瞞じゃね？
VDM-10のVDM++のが
枠組みはしっかりしてるけど事実上使えないし
Overture界隈はVDM-RTに傾倒してる感じだし
何かみんなおでこ広いし
- 32 名前：デフォルトの名無しさん mailto:sage [2013/01/26(土) 00:09:26.58 .net]
- >>13
> >人間が読み書きする形式言語
> >使い物になる日は来ないと思う
> そんなことはない。一流人材が参戦すれば変わる。
その一流の人材が膨大な人数どうやって確保するの？
形式仕様言語でフルに仕様を書けばプログラムコードと同じオーダーの行数になるという経験則がある。
つまり数人で作れるおもちゃのソフトウェアならともかく、社会の根幹を支えそれが故に信頼性が必須とされる
大きなソフトウェアは現在の大規模開発でプログラミングに関わってる膨大な人数と同じオーダーの
形式仕様記述者が必要になるってことだ。
それだけ莫大な人数のそんな高い質の人材が世界のどこにいるんだい？
寝言は寝てから言った方がいいよ。
それに数人のプロジェクトに限定しても、それを一流の人材で仕様記述しても
それで作られたソフトウェアの寿命がある間は、そいつのメンテナンスのために
ずっと一流の人材を貼りつけておかないと、彼らが書いた形式仕様なんて難しいものは
２流の人材じゃ読み書きできないから保守できないよね。ってことで一流の人材ほど
彼らが書いた仕様のお守をさせられて他の仕事ができなくなる。
これって素晴らしい才能の無駄遣い法だね。
- 33 名前：デフォルトの名無しさん mailto:sage [2013/01/26(土) 12:32:30.58 .net]
- 一流の人材を活用するとしたら
二流・三流の人が使える形式手法の技術を確立することだろうね
そういう意味では一流の人材は既に集まっている
ただ二流・三流が何たるかを理解できていない可能性はある
- 34 名前：デフォルトの名無しさん mailto:sage [2013/01/26(土) 19:14:58.59 .net]
- 用語定義で「名前： 2chに書き込むときの名前」てなこと書いておきながら
本編に「家で飼っているぬこの名前は〜」
とかしれっと書く奴はメタメタにしてやんよ！
軽量形式手法なんて形式手法じゃねぇと思ってたが
名を捨てて実を取ることも必要だと感じた。
- 35 名前：デフォルトの名無しさん [2013/01/27(日) 23:46:08.13 .net]
- >>32
>形式仕様言語でフルに仕様を書けばプログラムコードと同じオーダーの行数に
>なるという経験則がある。
だからあ！そういう今の形式仕様言語が糞なんだよお！まだ分からんのかあ！
- 36 名前：デフォルトの名無しさん mailto:sage [2013/01/28(月) 01:17:16.05 .net]
- >>35
> >>32
> >形式仕様言語でフルに仕様を書けばプログラムコードと同じオーダーの行数に
> >なるという経験則がある。
> だからあ！そういう今の形式仕様言語が糞なんだよお！まだ分からんのかあ！
ならば、形式仕様でフルに仕様記述するのが現実に可能だと主張したいのならば、
今のクソのでない形式仕様言語を現実に作ってからにしろ。
現実に存在しない夢のような形式仕様言語の存在を前提として>>13を主張するのは
単なる精神病患者だよ、誇大妄想と言う名前のな。
形式仕様屋にはこの手の誇大妄想患者が多すぎる。だから信用をなくして来たんだよ。
- 37 名前：デフォルトの名無しさん mailto:sage [2013/01/28(月) 01:22:14.84 .net]
- >>13は今のクソでない形式仕様言語を現実に作るために、一流人材が参加すれば可能だと述べているんだろ。
とはいえ、この論旨を許せば一流人材とやらがいれば世界征服すら可能になるが。
- 38 名前：デフォルトの名無しさん [2013/01/28(月) 08:48:24.11 .net]
- いまはむしろ誇大妄想がいないのが痛い。
だからユーザがプログラムと同じじゃないかと当たり前の苦情を言っても、
夢のような期待をするなと逆切れしてくる。
- 39 名前：デフォルトの名無しさん [2013/01/28(月) 08:56:42.23 .net]
- >>37
クソでない形式言語を作るのは世界征服と並ぶほど難しいことなのでしょうか？
- 40 名前：デフォルトの名無しさん mailto:sage [2013/01/28(月) 18:52:03.46 .net]
- フルフル君さ、ちょっと聞きたいんだけど、どういう意味で「フル」って言ってる？
フルに詳細化された仕様？
そりゃロクに抽象せずに詳細化された仕様をベタに書けばプログラムソースと同様になるわなw
- 41 名前：デフォルトの名無しさん [2013/01/28(月) 19:23:10.47 .net]
- また抽象なんて甘いこと言って逃げるｗ
ベタに書いたらプログラムと同等なるならダメなんよ
- 42 名前：デフォルトの名無しさん mailto:sage [2013/01/28(月) 19:29:38.21 .net]
- 逃げるも何も、それが仕様記述言語のポイントだろ…（呆
- 43 名前：デフォルトの名無しさん mailto:sage [2013/01/28(月) 19:31:37.37 .net]
- で、フルってどういう意味で言ってんの？
- 44 名前：デフォルトの名無しさん [2013/01/28(月) 19:41:09.93 .net]
- よし。アンタの言う仕様記述言語のポイントは何か、逃げずに言ってみろ。
- 45 名前：デフォルトの名無しさん mailto:sage [2013/01/28(月) 20:14:25.27 .net]
- フルフル君でもそれに噛みついている人でもないが
記述量は確かに実用上の課題ではあるけども
プログラムコードと同じオーダーなら駄目で短いならOKって
単純な話ではないと思うんだが
自然言語による仕様書の記述・検証の工数を無視しているのは意図的か？
それに形式的検証まで含むか否かで大きく変わる
証明された信頼性とテストによる確率的な信頼性は比較できない
自動コード生成が可能かどうかでも大きく変わる
- 46 名前：デフォルトの名無しさん mailto:sage [2013/01/30(水) 07:46:32.50 .net]
- PGが仕様記述言語でプログラム書いてるから、
プログラムと同じ長さになるんじゃね？
- 47 名前：デフォルトの名無しさん [2013/01/30(水) 18:32:23.88 .net]
- その「仕様記述言語」は、もはや一種のプログラミング言語じゃ？
- 48 名前：デフォルトの名無しさん mailto:sage [2013/01/30(水) 20:20:25.03 .net]
- プログラム言語を含んでいる仕様記述言語は多いね。
プログラム言語部分だけで仕様を書いちゃう人が
仕様がプログラムと同量だとか言い出すんだろうね。
- 49 名前：デフォルトの名無しさん [2013/01/30(水) 22:00:41.42 .net]
- >>45 >>46 >>47 >>48
仕様記述言語とプログラミング言語はどこが違うものなの？
- 50 名前：デフォルトの名無しさん mailto:sage [2013/01/30(水) 23:21:07.11 .net]
- >>49
目的が違う
実際のところ言語やターゲットとなる案件によっては
プログラミング言語でも仕様記述は不可能ではないし
仕様記述言語で実行可能なコードを書くこともできる
道具として両者を近づける試みも多数なされているが
仕様と実装をごっちゃにしようという話ではない
あくまで仕様と実装は別の概念
- 51 名前：デフォルトの名無しさん mailto:sage [2013/01/31(木) 04:28:00.46 .net]
- 適切な抽象度を設定すればいいんだろうけど
仕様と設計がごっちゃになってくるから
「俺は今何を書いてるんだろう」ってなってしまう…
VDMどうのこうのより、そもそもの設計経験とか抽象化の力が足りないってのが問題
- 52 名前：デフォルトの名無しさん mailto:sage [2013/01/31(木) 21:59:30.67 .net]
- 曖昧だったり矛盾を含んだりしている
自然言語の仕様書が幅を利かせすぎという面もある
世の中の仕様書が如何にいい加減か実感できるという点だけでも
形式的仕様記述を「体験」する意義は十分だと思うね
- 53 名前：デフォルトの名無しさん [2013/01/31(木) 23:37:20.78 .net]
- >世の中の仕様書が如何にいい加減か実感できるという点だけでも
>形式的仕様記述を「体験」する意義は十分だと思うね
形式的仕様ってその程度で満足してもらえるんだ。進まんはずだ。
- 54 名前：デフォルトの名無しさん mailto:sage [2013/02/01(金) 00:36:31.59 .net]
- >>53
形式的仕様が誰かor何かに満足してもらえる
なんて話はしていないと思うんだが
意図的なのか読解力がないのか分からんが
オナニーなら一人でやってくれ
他人を使うな
- 55 名前：デフォルトの名無しさん mailto:sage [2013/02/01(金) 04:35:25.45 .net]
- >>53
>形式的仕様ってその程度で満足してもらえるんだ。進まんはずだ。
ほら、この日本語文1つ取っても書いた本人以外には意味不明だろ？
- 56 名前：デフォルトの名無しさん mailto:sage [2013/02/01(金) 06:55:33.02 .net]
- 自然言語で契約交わすからこそ
世の中まわるという事実を無視されてもな…
まぁクリティカル系はしらんが
一般には無用だよな
- 57 名前：デフォルトの名無しさん mailto:sage [2013/02/01(金) 20:30:05.57 .net]
- 別に契約書を形式言語で書くわけじゃあるまいし
自然言語で契約する＝>世の中まわる
が真であろうと偽であろうと
形式的仕様の有用性を否定する理由にはならんよ
もちろん肯定する理由にもならないが
- 58 名前：デフォルトの名無しさん mailto:sage [2013/02/01(金) 20:32:08.41 .net]
- 契約書に形式仕様が記載された例もあるらしいぞw
- 59 名前：デフォルトの名無しさん [2013/02/02(土) 21:42:41.80 .net]
- >>54 >>55
だから
>世の中の仕様書が如何にいい加減か実感できるという点だけでも
こんなことはたいしたことじゃないと言ってるんだよ
つまらんこと言うな
- 60 名前：デフォルトの名無しさん mailto:sage [2013/02/02(土) 22:44:26.94 .net]
- たかが「体験する価値」にそんな高い敷居を設定するのか
つまらん奴だな
- 61 名前：デフォルトの名無しさん mailto:sage [2013/02/03(日) 08:34:30.94 .net]
- 形式言語で仕様を記述したら
テストパターンが自動生成されて
テストツールに食わせたら自動でテストやってくれる
ようになったら勉強しよう
- 62 名前：デフォルトの名無しさん mailto:sage [2013/02/03(日) 19:55:15.40 .net]
- >>61
お望みのレベルに達していないだろうけど
テスト自動生成なら既に実施例や商品があるよ
産総研でも研究してたはず
モデル検査でSATソルバ使うのが流行ってるっぽいんで
テストケース生成技術・ツールはもう少し発展しそう
形式手法ではないがテストを仕様に近づけるというアプローチでBDDというのもある
ただC++で使いやすいフレームワークは知らない
- 63 名前：デフォルトの名無しさん mailto:sage [2013/02/12(火) 20:50:42.97 .net]
- 実装がフレームワークとかで制限されているときって、VDMとかどう使うのがベターなんだろうか？
VDM仕様も制限するのか、VDMと実装との差はしょうがない、ってするのか
よくわかんにゃい
- 64 名前：デフォルトの名無しさん mailto:sage [2013/02/12(火) 23:28:00.22 .net]
- とりあえずinv, pre, postで十分に制約がかけられているんなら
関数・操作の中身が実装と異なっても問題ないんじゃね
あとは使い方次第としか
そのフレームワークの特性にも依存するし
- 65 名前：デフォルトの名無しさん mailto:sage [2013/02/14(木) 19:11:21.64 .net]
- とりあえず、そのフレームワークに食わせるハンドラやコンポーネントの
インターフェースを陰仕様で固めてみたら？
- 66 名前：デフォルトの名無しさん mailto:sage [2013/02/14(木) 21:53:35.90 .net]
- >>64 >>65
ありがとうございます。まずは陰仕様ってことですね
とにもかくにも書く目的をしっかりしないとダメですね
- 67 名前：デフォルトの名無しさん [2013/02/22(金) 11:18:28.53 .net]
- こういう従順な人はしばらく騙せるかもしれんが、まあ今の仕様記述言語は
使えんことはこのスレを見ていてもすぐにわかるな。
>一般には無用だよな
そうだな。
一生懸命擁護弁護しようとしているのがいるがなんでなの？
だからスレも伸びん
- 68 名前：デフォルトの名無しさん mailto:sage [2013/02/23(土) 00:41:19.99 .net]
- 具体的な提案もなしに絡んでくるのがいるがなんでなの？
駄目だと思うのは勝手だし2chに愚痴を書くのも勝手だが
批判できる立場かね？
擁護弁護したいんじゃない議論がしたいんだよ
- 69 名前：デフォルトの名無しさん mailto:sage [2013/02/23(土) 00:51:39.71 .net]
- SIL4クラスの安全にかかわる案件に絡んでいるが
優秀な人間が何人も集まって検討した仕様にすら穴がある
これはもう自然言語でやっている限りどうにもならないだろう
現状の形式手法では十分なソリューションたりえないのも事実だが
期待できるのは形式手法くらいしかないのも事実だ
現状が駄目だからといって将来が絶たれてよい技術ではない
- 70 名前：デフォルトの名無しさん mailto:sage [2013/02/25(月) 04:48:36.69 .net]
- 仕様の情報伝達力不足は SysML とかで補えばいいんでないの？
- 71 名前：デフォルトの名無しさん mailto:sage [2013/02/26(火) 04:49:05.67 .net]
- 誤解しているようだが
そういうのについてのスレなんだが
- 72 名前：デフォルトの名無しさん [2013/03/01(金) 20:47:27.99 .net]
- >現状の形式手法では十分なソリューションたりえないのも事実だが
>期待できるのは形式手法くらいしかないのも事実だ
そうなんだが、あまりに不満足な現状だとはおもわんか？
- 73 名前：デフォルトの名無しさん [2013/03/16(土) 23:22:52.05 .net]
- それみろ。まったくスレがのびんだろ
ＶＤＭはもちろんＡｌｌｏｙですらその程度なんだよｗ
- 74 名前：デフォルトの名無しさん mailto:sage [2013/03/17(日) 00:29:32.18 .net]
- テストしにくいコードをテストする方法教えて下さい
toro.2ch.net/test/read.cgi/tech/1334408391/
でテストケースの自動生成で賑わってるけど同じ人？
- 75 名前：デフォルトの名無しさん mailto:sage [2013/03/17(日) 06:38:43.65 .net]
- 2chなんかでクダ巻いて形式手法を批判した気になってるような低能は
そもそもVDMやAlloyを始めることすらしないからじゃないかな
- 76 名前：デフォルトの名無しさん [2013/03/17(日) 09:55:15.86 .net]
- >>75
おまえは家来か
- 77 名前：デフォルトの名無しさん mailto:sage [2013/03/17(日) 10:04:04.95 .net]
- Alloy本読んで勉強中だが、結局のところ現実の問題をどうモデル化するかって
ところがまだよくわからん。
例題でさらっとキャッシュメモリのモデルなんか挙げていたが、あんなの思いつかん。
そのへん、なんかいい参考書ないかねぇ？
- 78 名前：デフォルトの名無しさん mailto:sage [2013/03/17(日) 13:16:00.02 .net]
- Alloyで数独を解くのが昔一部で話題になったけど
そういう数理パズルとかで遊んでみるとか
- 79 名前：デフォルトの名無しさん [2013/03/17(日) 18:09:45.06 .net]
- >>77
そもそもふつうに思いつかんようなのがよいモデル化かな？
キャッシュメモリってどんな例題だったけ
ちょっと見てみるかな
- 80 名前：デフォルトの名無しさん mailto:sage [2013/06/02(日) 21:23:41.48 .net]
- 業務ロジックを仕様記述言語で書くことは可能かな？
なんか、例を見てると並列処理の時の云々かんぬんとかかなりアルゴリズム的だったり、詳細よりだったりする例が多いのが気になる。
仕様のバグで一番多いのは論理矛盾だったりするので、
その辺が検出できそうなら導入してみたいんだよね。
- 81 名前：デフォルトの名無しさん mailto:sage [2013/06/02(日) 22:55:50.61 .net]
- 業務ロジックがどういうものか知らないけど仕様記述自体はできると思うよ
ただ形式仕様記述ができることと
論理矛盾の検出ができることの間には大きな隔たりがあるのが現状
状態の数が限られているならなんとかなるけど
状態変数に実数とか時間を持つとなると途端に検証が困難になる
- 82 名前：デフォルトの名無しさん mailto:sage [2013/06/04(火) 02:08:31.54 .net]
- おお、そうなんだ。サンクス。
あんまりたいそうなロジックを扱ってるわけじゃないけど
取引ができる日がn日からm日で、そのうち取引ができるのはステータスがxの人で...
とか、まあ、そういったものの組み合わせが多いかな。
最悪、論理矛盾の自動検出が出来なくても、曖昧性の無い記述ができるなら
仕様漏れとかが減ったりしないかなぁ。
- 83 名前：デフォルトの名無しさん [2013/06/29(土) 13:32:51.16 .net]
- >>80 >>81 >>82
> 業務ロジックを仕様記述言語で書くことは可能かな？
ていうか、そのためのものなんだがｗ
いまの仕様記述を見てたらそんなことも分かりにくいが
- 84 名前：デフォルトの名無しさん [2013/06/29(土) 13:57:51.79 .net]
- 組込みっていうか車載開発（ボディ系）でAlloyを個人的に使おうと思ったが、
難しくて挫折しそうになった。。。C言語しか知らないとつらい。。。
- 85 名前：デフォルトの名無しさん mailto:sage [2013/06/29(土) 19:20:26.45 .net]
- >>84
組込み系であれば、(Alloy/VDM/Zなどよりも)
「振る舞い」の検証を重視するCSPやCCSのほうが
(多くのケースでは)適しているのではないかと思われ
もしもこれら形式的記述スタイルに慣れていないのなら、
PROMELA(およびその処理系であるSPIN)はいかが？
C言語とステートマシンの知識があれば、直感で理解できる
最近は、PROMELA/SPINに関する日本語書籍もいくつかあるよ
- 86 名前：デフォルトの名無しさん mailto:sage [2013/06/29(土) 21:00:02.42 .net]
- アドバイスありがとうございました。
積読状態ですが、VDMにAlloyにSPINに書籍は購入済みですので、
一度読んでみます。
Alloyに手を出したのは、VDMやSPINの両方のおいしいところを合わせたのと、
手軽にモデリングできると聞いたからです。
・・・でも私には簡単ではなかったorz
- 87 名前：デフォルトの名無しさん mailto:sage [2013/06/30(日) 23:16:19.56 .net]
- 世界的には業務ロジックの構築=DSL(ドメイン記述言語)の流れじゃなかったけ。
- 88 名前：デフォルトの名無しさん mailto:sage [2013/07/06(土) NY:AN:NY.AN .net]
- DSLと形式手法は普通に両立すると思うが？
- 89 名前：デフォルトの名無しさん [2013/07/16(火) NY:AN:NY.AN .net]
- Rodinはまともなチュートリアルないんか。
Event Bの理論は本読んでどうにかするとして、ツールとしてのRodinの使い方が公式のチュートリアル見てもよくわからん。
- 90 名前：デフォルトの名無しさん mailto:sage [2013/08/28(水) NY:AN:NY.AN .net]
- Code Contractsはこのスレの範疇？
- 91 名前：デフォルトの名無しさん mailto:sage [2013/08/29(木) NY:AN:NY.AN .net]
- いいんじゃね？
- 92 名前：デフォルトの名無しさん mailto:sage [2013/08/31(土) NY:AN:NY.AN .net]
- 形式手法が実用にならないと言われる中で
Code Contractsは計算機科学とソフトウェア工学の中庸にあると思うけど
あんまり話題にならないね
Code Contracts目当てにProfessional買うことはないだろうから
Express Editionにも対応してくれればいいのに
- 93 名前：デフォルトの名無しさん mailto:sage [2013/08/31(土) NY:AN:NY.AN .net]
- 乞食と思われると残念だから補足するけど
利用するライブラリが契約されてないと利用者側が馬鹿を見るので
みんな契約すればいいのに！的な意味で
- 94 名前：デフォルトの名無しさん mailto:sage [2013/09/09(月) 00:32:04.39 .net]
- C++1yではConcepts復活すんのかな
- 95 名前：デフォルトの名無しさん mailto:sage [2013/09/12(木) 18:51:59.14 .net]
- prologじゃダメなの？（DSLも含めて）
- 96 名前：デフォルトの名無しさん mailto:sage [2013/09/12(木) 21:25:52.57 .net]
- >>95
そうね。少なくともDSLを記述して実行させるくらいなら
最初からPrologで書いてしまった方が気が利いていますね。
- 97 名前：デフォルトの名無しさん mailto:sage [2013/09/12(木) 22:36:29.89 .net]
- Prologで書かれた仕様を実装に落とし込むのは
自然言語で書かれた仕様を実装に落とし込む時とは
別の危うさがあるように思える
バックエンドに使うんなら何でもいいけど
- 98 名前：デフォルトの名無しさん mailto:sage [2013/09/12(木) 22:38:55.18 .net]
- 具体化prz
- 99 名前：デフォルトの名無しさん mailto:sage [2013/09/12(木) 22:49:54.07 .net]
- ？
- 100 名前：デフォルトの名無しさん mailto:sage [2013/09/12(木) 23:22:19.80 .net]
- スプレッドシードに書かれた自然言語の仕様書よりか、
prologの方が危ういって形式手法の危うさでも指すの？
wikipedia読む限り、形式手法が集合論と述語論理を扱う設計手法みたいだし、
その限りじゃprologで十分だよねとは思ったのだけれども、一体、何が悲しくて
alloyやZみたく仕様がデカくて、ノウハウを使い回せない言語が乱立してんだろ
- 101 名前：デフォルトの名無しさん mailto:sage [2013/09/12(木) 23:47:46.69 .net]
- 自然言語よりPrologの方が危ういなんて書いてないだろ
Prologで十分だというのが仮に事実だとしてそれが何なの？
その事実はPrologが優秀であることの証明にはならないし
他の技術を否定する正当性も与えない
- 102 名前：デフォルトの名無しさん [2013/09/13(金) 00:20:22.87 .net]
- 述語論理を書くならprologは有力なツールでしょうね。
でも、そもそも我々は述語論理を扱いたいんじゃないんです。
むしろ触れずに済むなら、その方がきっといいんです。
目的を忘れて手段を論じても無益でしょう。
- 103 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 07:56:11.25 .net]
- 集合論や述語論理を徹底的に研究した人はそんなにはいない。
あまりこれに拘った仕様の言語は大半の人には使い難い。
Prologくらい世俗的で下支えとしては述語論理がありますよ
くらいの言語の方が万人向きでしょう、という話ですよ。
- 104 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 11:55:09.39 .net]
- は？徹底的に研究する必要なくてソフトウェア開発の道具として利用するだけ
そもそも、集合論や述語論理のABCすら理解しないでAlloyやZを使う馬鹿いないだろ
- 105 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 11:59:30.78 .net]
- >>104
そうだと思いますよ。
- 106 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 12:20:24.26 .net]
- >>101
prologの優秀さは、その簡潔かつ可読性の高いコード。
無駄に仕様の大きな言語って、学習コストが高く、バグを誘発するだけ
少し前に途絶えた良い例がperlとcommon lisp
形式手法が集合論と述語論理を取り扱い、
その要件を満たす最小セットの記述がprologで済むのではないかと仮定したとき、
それに対するalloyやZがprologに対して如何なるアドバンテージがあるか
って書いたの
>他の技術を否定する正当性も与えない
技術を否定しない技術者って技術者に向いてないんじゃないの？
人権屋とか宗教家にでも転職したら？
>>102
目的が形式手法への適応で、そこに集合論と述語論理が含まれるので述語論理を扱います。
そもそも述語論理のABCを理解してない非技術者がalloyやZを使うのか疑問です
目的を忘れて仕様の膨れあがったツールがalloyやZではないのかといったのが、
>>100のレスにおける核となる主張であり、疑問です。
が、その達観した無益なレスを書いて気持ち良いですか？
- 107 名前：デフォルトの名無しさん [2013/09/13(金) 20:09:03.07 .net]
- つか、Prologで仕様記述なんてどこでやってんの
- 108 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 20:34:26.75 .net]
- >>106
>形式手法が集合論と述語論理を取り扱い、
>その要件を満たす最小セットの記述がprologで済むのではないかと仮定したとき、
その仮定「Prologは形式手法の要件を満たす」が間違っているんじゃないかね
述語論理だけを取り扱う、いわゆる純粋Prologの表現力は極めて乏しいものだ
Prologプログラミングでは、カットや高階述語(assertなど)の非純粋な操作が必然となる
結果からすると、形式手法の要件である「検証」をPrologは満たさないことになる
また、Prologは型付けの弱い言語だ
仕様を記述できたとしても、それに矛盾が無いことを「検査」できない
形式的な立場であれば、ある集合の要素はすべて同じ種類でなければならないが、
この種類、つまり型の一貫性をPrologでは保証できない点は、形式言語としては致命的な欠陥
- 109 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 20:42:25.00 .net]
- >>108
「仕様が記述できたとしても、それに矛盾がないことを「検査」できない」
はおかしいだろう。
質問として実行すればいいのではないかな。定理証明の過程なのだから。
- 110 名前：デフォルトの名無しさん [2013/09/13(金) 20:47:12.33 .net]
- では来週からPrologで仕様を書いてください。
- 111 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 21:04:25.47 .net]
- >>109
やはり形式手法という概念そのものが理解できていないようだね
仕様を実行して振る舞いを確認するのは「シミュレーション(模倣)」と呼ばれる手法であり、
「(形式手法における)検証」ではない
定理証明の過程において、対象となる仕様は「一切実行されない」ことを理解しなければならない
これを実現するために、形式手法では厳密な数学を基礎に置き、それを元に証明を進める
- 112 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 21:16:04.80 .net]
- >>111
なるほどね。わかった。
動的言語云々ということが書かれていたので検査が実行されるのだと
思ってしまった。
- 113 名前：112 mailto:sage [2013/09/13(金) 21:22:31.21 .net]
- まちがえた。
動的云々ではなく、「型付けの弱い言語云々」でした。
- 114 名前：デフォルトの名無しさん [2013/09/13(金) 22:19:56.75 .net]
- でも形式手法をそういう言い方にするとAlloyやVDMの微妙さが際立ってしまうのだ
- 115 名前：デフォルトの名無しさん [2013/09/13(金) 22:56:23.06 .net]
- >>108
型や集合なら事実を加えるなりの規約程度で、どうにか出来そうなイメージ
てか、形式手法って検証なんてステップあるのね。こうなると専用の言語つかった方がはやそう
けれど誰かプレーンなprologで時相論理のサブセットとか書いてないのかな
第五世代のprolog hackerたちが、このスレを通ることに期待age
|
 |
