【Alloy】形式言語による仕様記述【VDM】

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 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 116 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 23:21:23.48 .net] >>114 Wikipediaの「形式手法」で説明されているように、 形式手法にもレベルがあっていいじゃないかと で、伝統的なZやVDMは重量級で、Alloyなど最近は軽量級が注目されている Prologについては、(>>108で書いたように)純粋Prologの表現力と型付けの弱さという欠点が、 軽量な形式手法としても問題が多いと見る ただし、これは形式手法としての問題点であって、プログラミング言語としての問題ではない また、PrologにはDCGによるDSL(ドメイン記述言語)およびメタインタプリタの開発に 適しているという、優れた特性がある これを活かし、あるドメインに特化した軽量仕様記述言語と処理系を開発すれば、 先に述べた欠点を補うことができると思う 以下は、Prologで過去に開発した仕様記述言語で、2進カウンタを記述している： 　process binCounter(ins:in, outs:out, carry:out). 　　　state 0. 　　　from 0, 　　　　　when ins$0, output (outs$0, carry$0), to 0. 　　　　　when ins$1, output (outs$1, carry$0), to 1. 　　　from 1, 　　　　　when ins$0, output (outs$1, carry$0), to 1. 　　　　　when ins$1, output (outs$0, carry$1), to 0. 言語は通信プロトコルの仕様記述言語である Estelle を参考にしたステートマシンをモデルとし、 シミュレーション(=模倣)による振る舞いの確認が可能 最終的にはペトリネットへ変換して検証する予定だったけど、着手できぬまま放置している 117 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 01:22:47.81 .net] VDM ToolsもOvertureも証明の機能が不十分だから 形式手法のレベルで分類すればVDMはもっぱら軽量じゃね？ まあこの際どうでもいいが 118 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 13:12:05.22 .net] >>117 形式言語 VDM と形式言語処理系 VDM Tools をごっちゃにすべきではない 言語 C と 処理系 gcc(あるいは VC++) をごっちゃにするようなもの 言語としての VDM は形式的な証明が可能な体系 (ただし、それを機械的に適用できるか否かは別の話) そして、処理系としての「VDM Tools はもっぱら軽量じゃね？」ならば、同意する 119 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 13:32:16.32 .net] そりゃごっちゃにすべきじゃない文脈もあるだろうが C言語の喩えで言えば gccもVCも対応していない機能はないようなものでしょ C言語の仕様策定は実装ありきだから そのうち対応する見込みはあるけど VDMで証明とかOverture界隈も興味の対象から外れている感じだし先が見えん 120 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 15:56:52.26 .net] >>119 >C言語の喩えで言えば >gccもVCも対応していない機能はないようなものでしょ んなわきゃーない。なんのための言語規格だ。 121 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 16:17:21.73 .net] 言語規格だか何だか知らんが絵に描いた餅でも喰ってろ VDM-SLはISO化されたが VDM++に関しては文法こそ仕様はあるものの 挙動は実装が仕様みたいな状況だぞ 122 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 20:04:31.44 .net] 挙動なんて言ってる時点で 静的解析をガン無視してるのはVDM界隈じゃなくて>>121だということがわかる。 123 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 22:53:25.27 .net] だったらVDMの静的解析に期待を持てるような 実績や活用法の情報をくれよ 124 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 23:08:58.11 .net] >>123 「だったら」が何を指すのか意味不明だし、また静的解析みたいな曖昧な言葉を持ち出す まだ >>123 は(言語としての) VDM における検証や証明を扱うレベルに達していないので、 無理に背伸びはせず(処理系としての) VDM Tools を触ることから始めたほうがいいと思われ ただし、今のままでは軽量と言われる VDM Tools ですら理解するのは難しいと思うがね

---

---

[ 続きを読む ] / [ 携帯版 ]

read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef