【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 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 ですら理解するのは難しいと思うがね 125 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 23:15:08.44 .net] >>122に言えよ 126 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 23:23:18.69 .net] >>125を翻訳すると、 「>>122くんの言葉を真似しただけだから、僕ちゃん悪くないもん！！」 127 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 23:42:17.97 .net] >>124 選民意識も結構だが 「馬鹿には無理」みたいなこというから形式手法が馬鹿にされる ユーザに技術の存在を意識させないというのは 道具のあるべき姿の一つだが stealth formal methodsなんてフレーズが生まれるのは何かおかしい 128 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 00:48:45.39 .net] >>127 形式手法が何であって何ではないか、また形式手法では何ができて何ができないのか、 こんな基本的なことも>>123は分かっていないようだから、理屈よりも実践を、 つまり VDM Tools を触ることから/触れるレベルの学習から始めたほうがいいと アドバイスしてるだけだがね また>>127は「(形式手法の習得は)馬鹿には無理」と考えているようだけど、自分はそうは思わない 最低限必要なのは普通高校卒業程度の数学と教養であり、IT業界人やそれを目指す学生の大半が該当する ただし、本人にヤル気が無ければ無理だし、たとえあっても素直さと謙虚さは必要だがね 129 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 07:45:12.05 .net] >>123 つ 「型検査」 130 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 14:17:26.84 .net] 型検査なんかプログラミング言語で一般的過ぎて 期待も何もスタートラインだろ 整数（int, nat, nat1）とトークンだけで記述できる場合はまだしも レコードやクラスを使い始めると モダンなプログラミング言語に比べ使い勝手の悪さが目立つ さらに証明までやろうとすると証明責務が無理ゲーになる 結果としてユーザが気軽に型を作れない 131 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 14:34:04.62 .net] VDM++に関して言えば演算子オーバーロードはつけるべきだった メソッド名に全角の≦とかを使うなんてバッドノウハウは見るに耐えない インターフェイスやMix-inも言語レベルで対応してない テンプレートやジェネリクスもない これらはプログラマが楽するための道具に留まらず データ表現を抽象化してロジックに意識を集中させるために 仕様記述に有効な機能じゃなかろうか 132 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 16:58:56.24 .net] 証明しにくくするだけ 133 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 18:02:44.28 .net] 仕様を書く人が 証明のこと気にしないといけないのが未成熟な証 ASTなり中間言語にさえ落とし込めさえすれば あとは数学者やコンピュータサイエンティストの仕事だ 134 名前：デフォルトの名無しさん [2013/09/15(日) 18:22:03.16 .net] そりゃないわ。 135 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 18:35:46.84 .net] >>133 >あとは数学者やコンピュータサイエンティストの仕事だ いや、それはAI(人工知能)の仕事だよ 自然語で書かれた曖昧な仕様を、コンピュータが理解できる機械語へ変換するという もちろん、これが理想の姿であるのは理解するが、現時点では夢物語でしかない だから、自然言語で書く曖昧な(非形式的な)仕様の代わりに、 (数学を元にした)形式的な仕様記述を試みよう、という思想が形式手法の出発点にある >>133には、C.A.R. ホーアの言葉を送ろう： 　職業としてプログラミング業務を行うためには、基礎となる数学理論に基づき、 　すでに確立された他の工学分野の先例にならわなければならない。 　これは教育を改善することによって実現することができる。 　　　　　　　　　　　　　　　「プログラミング -- 魔術か科学か？」から引用 136 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 19:10:48.05 .net] 形式的な検証を目的に形式仕様を書くのなら 証明のことを気にするのは当然だろw 137 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 19:26:34.98 .net] >>135 だからそのAIを作るのは数学者やコンピュータサイエンティストで 言語のユーザでも言語屋さんでもないだろ >>136 気にした方が良い結果になることが多いだろうが 気にしないと使えないなら未熟だってこと 形式仕様を書くのは形式的な検証が主目的とは限らない 138 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 19:52:25.00 .net] 形式手法に限らず、大抵のものは「気にしないと使えない」だろ。 オブジェクト指向だって関数型だってCoqやAgdaだって、 記述目的を意識して書かないとクソな記述になるのと同じだろ。 139 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 20:06:00.03 .net] 程度問題だよ 少なくとも俺にとってはVDMとりわけVDM++は 仕様を記述するには気が利かないし面倒くさ過ぎる そのくせ証明による検証も大して期待できない 勿論そう思わない人もいるだろう そういう人は是非とも形式仕様記述を活用して普及に努めてもらいたい 140 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 21:08:48.08 .net] >>137 >だからそのAIを作るのは数学者やコンピュータサイエンティストで >言語のユーザでも言語屋さんでもないだろ もちろん、そのとおりだよ そして、AIの話題はスレ違いってことさ 141 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 21:25:23.64 .net] スレチってほどでもないと思うけど SATソルバの話題とかしてもいいんじゃね？ どうせ過疎ってるか 愚痴や揚げ足取りの応酬しかしてないんだし 142 名前：デフォルトの名無しさん mailto:sage [2013/09/16(月) 00:03:43.85 .net] そんなことより、皆さん、どうやってデッドロック回避してるの？ 143 名前：デフォルトの名無しさん mailto:sage [2013/09/16(月) 00:42:33.03 .net] >>139 そういう態度を、評論家とかコメンテータという まあ、自分で理解できないのを言語やツールのせいにするのが許されるのは、お子ちゃま迄だよ 144 名前：デフォルトの名無しさん mailto:sage [2013/09/16(月) 19:32:39.59 .net] どっちが先に根負けするか賭けようぜ 俺は最初の奴とみた 145 名前：デフォルトの名無しさん mailto:sage [2013/09/16(月) 20:44:16.20 .net] どっちって誰と誰だよ 146 名前：デフォルトの名無しさん mailto:sage [2013/09/16(月) 20:50:19.99 .net] ざーっと追ってあなたの思う両者でよかろう 傍観者的には、すでに1on1じゃなく途中から同意見者が混ざって混乱してる可能性もありそうに感じた 147 名前：デフォルトの名無しさん mailto:sage [2013/09/16(月) 21:05:43.76 .net] ４，５人が入り混じった乱戦だろｗ 148 名前：デフォルトの名無しさん mailto:sage [2013/09/16(月) 21:14:01.04 .net] このスレで興味もってざっとぐぐってるんですが、なかなか面白そうな分野ですね。 書籍やサイトのお勧めあったらご教示願えると幸いです 149 名前：デフォルトの名無しさん [2013/10/02(水) 09:58:39.78 .net] >>100 >>133 >>137 この人センスいいねえ >>111 >>136 この人は単なる学習者 150 名前：デフォルトの名無しさん mailto:sage [2013/10/03(木) 20:35:05.95 .net] へー（ニヤニヤ Zの言語仕様がデカいと思っている人のセンスがいいとか言うのって 本人以外考えられないけどw 151 名前：デフォルトの名無しさん [2013/10/03(木) 23:29:48.73 .net] ニヤニヤすんな 要らん言うてんやろ 152 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 07:56:58.26 .net] で、Zの言語仕様のどこがデカいわけ？ ぼくちゃん学習者なんで教えてくださいませ〜 153 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 08:42:40.94 .net] >>152 単一化と導出・融合だけの pure Prolog に較べると途方もなく大きいのではないか。 154 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 09:17:10.07 .net] Zの言語仕様には単一化もレゾリューションもNAFもないよ。 どうして実行機構を持たないZのほうが言語仕様がデカいと思うんだい？ 155 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 10:09:22.67 .net] 言語仕様の大きさは 処理系やツールを実装する人にとっては重要かもしれないけど ユーザにとっては重要じゃないよね。 何ができるか・何をしないといけないかが重要。 そしてそれは言語仕様の大きさと必ずしも対応しない。 言語仕様の大きさで議論しようというのがそもそも筋が悪い。 言語仕様を全部把握していないと使えない訳じゃあるまい。 156 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 10:19:02.52 .net] 結論：>>100は筋悪 157 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 10:20:01.06 .net] その>>100を「センスいい」と言っちゃう>>149も筋悪。 158 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 12:53:16.23 .net] すじわる、って将棋以外で聞かない単語だよね。 まあ筋が悪いとは普通に使うんだから字面を見てわかると思うけど。 159 名前：112 mailto:sage [2013/10/04(金) 15:11:02.46 .net] >>154 ここでいう言語仕様とは学習しなくてはならない範囲の 意味が強いと思う。そういう意味なら、一人で使う場合は 別だが、他者の形式仕様を読む場合にはひと通りは抑えて いなくてはならず、Zはその点やはり負担が大きい。 160 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 16:02:12.94 .net] Zは基本的に述語論理と型付集合論がわかってれば 覚えなければならない事はとても少ないだろ。 むしろVDMやAlloyあたりのほうが 述語論理や型付集合論以外の言語要素が多いと思う。 Zで苦労するのは他の言語/手法と比べてツールサポートが少ないことだろ。 161 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 16:30:35.19 .net] >>160 Zについては、全てはこの本の後遺症だと思う。 amazon.com/dp/481018563X 162 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 16:33:28.90 .net] www.amazon.co.jp/dp/481018563X かな。 163 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 21:30:59.69 .net] ＺもVDMも基本は70年代の言語だからなぁ 比較的新しい言語だとCafeOBJなんかがあるけど 二木先生の関わっていない利用例を知らない 164 名前：デフォルトの名無しさん [2013/10/04(金) 21:49:13.71 .net] >>155 >言語仕様の大きさは >処理系やツールを実装する人にとっては重要かもしれないけど >ユーザにとっては重要じゃないよね。 誰にとっても同じだ。 同じことをするんなら小さい方がよいのに決まっとる >>160 だからZは要らんと言っとる >>163 CafeOBJが新しいのか 165 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 21:58:38.09 .net] >>164 そんなに言語仕様が小さいのがいいのならBrainf*ckなんか最高だよね チューリング完全だから「計算可能性の観点においては」 他の言語と同等のことができるよ 166 名前：デフォルトの名無しさん [2013/10/04(金) 22:06:34.37 .net] 観点は計算可能性だけじゃないだろ まだチューリング完全なんて言ってるのか 167 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 22:10:26.71 .net] 観点は言語仕様の大きさだけじゃないだろ って話だよ チューリング完全ならどれも一緒だなんて誰も思っちゃいねーよ 168 名前：デフォルトの名無しさん [2013/10/04(金) 22:30:01.22 .net] だれかこの辺の議論のような口喧嘩のようなことを交通整理できる人はいないでしょうか 169 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 23:00:21.87 .net] そういった態度というのは単に自信が無いだけなので、 生暖かく放置すればいいのではないかと思われ 170 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 23:07:34.51 .net] ところで、Prologで仕様記述やその検証ができるなら試してみたいんだが、 その方法を解説した本やWebサイトとかあるのかな？ 「理論的にはできるはず」だけだとProlog自体よく知らない俺には無理だが。 171 名前：デフォルトの名無しさん [2013/10/04(金) 23:08:43.39 .net] あんたは自信があるのかい 172 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 23:32:01.69 .net] >>170 >ところで、Prologで仕様記述やその検証ができるなら できないんじゃね？ 過去には「できるはず...」という願望もしくは妄想に基づく意見(>>95-)はあったけど、 それに対する反論には何も意見を言えず議論を終えた 個人的には、型の無い純粋Prologを形式言語と呼ぶには無理があると考える Prologへの願望を語りたいという気持ちは理解できるが、 それはPrologスレで大いに語ればいい、それが妄想であってもいい 173 名前：デフォルトの名無しさん mailto:sage [2013/10/05(土) 05:30:54.75 .net] Prologで仕様記述しますなんていう例は山ほどある。 知らないんなら論文読まなさすぎ。 どれも結論は 「表現力不足だよね」 「表現上の制限が強すぎて、かえって表現が冗長になってダメだね」 「最低限FOLは必要だよね、やっぱし」 なわけだが。 174 名前：デフォルトの名無しさん mailto:sage [2013/10/05(土) 05:33:52.83 .net] >>164 >だからZは要らんと言っとる つまりZの言語仕様はデカくないという意見に反論できないってことね。 理由も言えずに「要らん」としか表現できない人が形式仕様とか、鼻で笑っちゃうねw 175 名前：デフォルトの名無しさん mailto:sage [2013/10/05(土) 08:56:49.36 .net] Alloyの本を読んでもちっとも頭に入っていきません。 この本を読むうえで必要な前提知識って何でしょうか？ また、その知識を得るのに最適な書籍があれば教えてください。 今は組込み関係の仕事（主に車関係）をしていて、知ってる言語はC言語のみです。 176 名前：デフォルトの名無しさん mailto:sage [2013/10/05(土) 10:07:18.70 .net] 知識はともかく 詳細仕様や実装仕様じゃなく 純粋なシステム仕様の読み書きをした経験がいるんじゃないかな 組込み関係だとシステム仕様と実装仕様がごっちゃになってる印象がある 実装仕様レベルの形式記述もできるけど そういうのは実装言語（C言語）のツールを使った方がいいと思う 177 名前：デフォルトの名無しさん [2013/10/05(土) 18:08:45.67 .net] >>174 その存在自体が無駄だと言っとるんだから、さらに何を言う必要がある？ Zや言語仕様の大きさなんていうくだらんことにどんだけ時間を浪費するんだ 178 名前：デフォルトの名無しさん mailto:sage [2013/10/05(土) 18:25:17.75 .net] Zを否定した根拠が「言語仕様のデカさ」だったのに 今更なにを喚いているんだい、負け犬くんw 179 名前：デフォルトの名無しさん mailto:sage [2013/10/05(土) 18:35:37.68 .net] 「C言語以外は全部無駄」とたいして変わらん主張 180 名前：デフォルトの名無しさん mailto:sage [2013/10/05(土) 22:31:33.47 .net] >>164は自分の主張が矛盾しているのに気付かない可哀想な子 >>160が言うように、Zは「述語論理と型付集合論」を知っていれば学習の壁は低い つまり、もしも>>164の言葉「同じことをするんなら小さい方がよいのに決まっとる」が正しければ、 仕様の小さなZは優れていていることになるが、その一方でツールサポートの少ない「Zは要らん」と言う では、ナゼそんな矛盾が生まれたのか？これは形式手法へ拒絶反応を起こす人によくあるパターンで、 形式手法を扱うのに前提となる素養(論理と集合)が欠けているからだろう だから>>164にはZの仕様が(とほうもなく)巨大に見えて尻込みしてしまう 逆にAlloyはツールで実際に動かしながら試行錯誤できるから容易い存在に見える 実際にはAlloyの全容は巨大で難解なものだけど、>>164には表層の一部しか見えていない おそらく、>>164はERM/OMT/UMLのような「仕様の視覚化手法(visualize method)」には 十分な経験と自信があるのだろう ところが残念なことに、その延長で「仕様の形式化手法(formal method)」を 理解しようとして、その狭間(ギャップ)で「もがいている」のだと思われる 181 名前：デフォルトの名無しさん [2013/10/05(土) 22:44:35.57 .net] >>175 述語論理ですかねー。あの変なシンタクスがオブジェクト指向と関係なくて、回りくどく表現された述語論理だと思うとたぶんわかってくる気がする。 あとAlloyだとたぶんその仕事にはあまり直接的に活かせないような。>>84-86に同じような話があるけど。 182 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 06:14:26.21 .net] >>180 そうだね、>>164みたいな人は10年か20年ぐらい前にもいたねえ。 「オブジェクト指向」でギャップに嵌ってる人達がね…（遠い目 UMLは図を「コトバ」として読む力が必要とされるんだけど、 形式手法では式を「コトバ」として読んじゃいけない。 式はあくまで記号列として読まないと「形式」の意味がわからない。 それができない人にはZは地獄のような言語かもしれない。 そういう人ほどZで徹底した形式主義を身につけたほうがいいと思うけど、 大抵は実行系中心の軽量形式手法で「これが形式手法かー」と思っちゃうんだよな… 183 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 10:50:33.15 .net] >>180 確かに、 Zは「述語論理と型付集合論」を知っていれば学習の壁は低いのだろうが、 そういう人材を一般企業では集められなかったからZは顧みられなかった のではないか。 184 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 11:30:50.49 .net] 述語論理も型付集合論も大学の教養レベルの数学で十分なのだから 「人材を集められなかった」のではないと思う。 単に、Zに限らず形式手法なしでもシステムを作れると思ってたんだろ。 だから、Zに限らずモデル規範型の形式手法は顧みられなかった。 185 名前：デフォルトの名無しさん [2013/10/06(日) 18:43:42.19 .net] >>182 >形式手法では式を「コトバ」として読んじゃいけない。 >式はあくまで記号列として読まないと「形式」の意味がわからない。 ここは何を言ってるの？記号列として読んでいるのでは意味が分かっていない と言われそうだけど。 186 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 22:31:52.02 .net] >>185 横レスだけど、形式手法の証明においては式に含まれる記号の意味は「無価値」だということ 記号の意味を分かる必要は無いし、 証明の過程で記号の意味は完全に無視され「形式(公理や定理)」だけが価値を持つ ソフトウェア仕様記述は現実世界のモヤモヤした実体(=モノ)をある体系でモデル化することから始まる たとえばUML等のOOA/OODでは現実世界をオブジェクトの集まりと捉え、オブジェクトの持つ属性や オブジェクト間の(継承や部分といった)関係を定義することによって(非形式的な)モデル化を進める ここでは実体をコトバとして抽象化する事を、具体的には定義するオブジェクト/属性/関係などの 命名(naming)を、つまり(人にとっての)直感的な意味を重要視する これによって(人にとって)分かりやすく、特に共同作業下における仕様イメージの統一的な共有化を図る これに対して、形式手法では現実世界をモデル化することは(視覚化手法と)同じだけれど、 数学という形式的な体系を用いる点が異なる つまり、ある式(=モデル)が直感的には(=人にとっては)いかに分かりやすくて正しく見えようとも、 いいかえるといかにOO的視点では優れた設計であっても、形式に矛盾があれば誤りであると見なす 187 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 22:55:41.08 .net] >>186 こっちも横レスだけど 証明は形式意味論のレイヤーで行われるけれど 形式仕様自体は現実世界の概念（「コトバ」）とリンクしている 「コトバ」であり「記号列」であることを理解できないと 形式仕様を理解したことにはならんだろう 188 名前：デフォルトの名無しさん [2013/10/06(日) 22:57:20.47 .net] >>186 >形式手法の証明においては式に含まれる記号の意味は「無価値」だということ それは証明器にとって、ということでしょう。人間にとってではない。 >これに対して、形式手法では現実世界をモデル化することは(視覚化手法と)同じだけれど、 そのモデル化の時点で、「意味」が介在するよね。 >形式に矛盾があれば誤りであると見なす それは当たり前。矛盾というのは形式的なものだからね。 だからといって「意味」が不要ということにはならない。 189 名前：デフォルトの名無しさん [2013/10/06(日) 23:01:03.54 .net] 「形式」手法 "form"-al method という言葉の意味からはじめないといけないようだな！ 190 名前：デフォルトの名無しさん [2013/10/06(日) 23:11:16.30 .net] >>189 およその意味はみんな分かってると思うが その厳密な定義もない（あるいは厳密に定義する意味もない）ことも含めて だがもし必要なら、そこからはじめてくれてもよいが 191 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 23:15:39.39 .net] みんな数学ガール／ゲーデルの不完全性定理 でも読んで和みたまえ（ステマ） 192 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 23:30:11.15 .net] >>187,188 現実世界を抽象化する過程に意味が伴うのはその通りで、視覚化手法も形式手法も同じ 形式手法にとっても抽象化の過程ではコトバの意味が大切なのに変わりはない 違うのは、抽象化の成果物である「仕様(設計書)の検証」において、視覚化手法では (人間が介在する)直感を頼りとしており、そこではコトバの意味が重要な位置を占める それに対して形式手法では仕様の検証に人の直感は介在せず、コトバの意味は無視する ここで、証明(=形式を元にした検証)を人力でやろうが証明器で自動化しようが同じ そして、もし証明が失敗すれば(仕様に矛盾を発見すれば)、現実世界の抽象化という前工程に立ち返る その時には、(数学としての)形式化の単純ミスもあるだろうけど、コトバの意味(の定義)の過ち、 つまり(抽象化の過程で)現実世界の解釈に何か誤りや漏れがあったことが発見できるだろう 193 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 23:45:46.18 .net] >>188 >>形式に矛盾があれば誤りであると見なす >それは当たり前。矛盾というのは形式的なものだからね。 いや、「非形式的な矛盾(=直感に基づく矛盾)」というのは存在する たとえばOOの仕様で、ある箇所では「XはYのサブクラスである」と記述され、 別の箇所では「YはXのサブクラスである」と記述されていれば、それは矛盾だろう ただし、サブクラスというオブジェクト間の関係は(人の)直感として定義されたものだから、 それは「形式的な矛盾」ではない 194 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 23:49:56.14 .net] この会話が成立していないのに 話が流れていく感じはすごいな 形式手法に言及しているのに 詭弁（誤謬）ばかりってのが皮肉 195 名前：デフォルトの名無しさん [2013/10/07(月) 06:12:47.77 .net] >>193 >「非形式的な矛盾(=直感に基づく矛盾)」というのは存在する 形式的に意味不明な言明だ。 論理的訓練が不十分のようだから指摘しておく。 >別の箇所では「YはXのサブクラスである」と記述されていれば、それは矛盾だろう 矛盾とはAかつ¬Aが帰結することだ。「XはYのサブクラスである」と 「YはXのサブクラスである」はまだ矛盾ではない。 >ただし、サブクラスというオブジェクト間の関係は(人の)直感として定義されたものだから、 そういう関係もまた形式的に記述するんだよ。 >>194 >形式手法に言及しているのに >詭弁（誤謬）ばかりってのが皮肉 意味不明。間違いがあれば指摘すればよい。 形式手法＝無謬ということではない。形式手法を偶像崇拝してる？ 196 名前：デフォルトの名無しさん [2013/10/07(月) 08:17:29.48 .net] >>192 概ね妥当なコメントと思うが 「視覚化手法」なんてものを形式手法と対比させるのはいかがなものか それから、ここでは皆矛盾矛盾と言うが、矛盾がないというのは最低限の条件に過ぎない 197 名前：デフォルトの名無しさん mailto:sage [2013/10/07(月) 08:39:38.60 .net] >>184 20年近く前に、私の周辺でZの研究会が次々と撃沈していったのを 知っている私としては、隔世の感ありだな。 198 名前：197 mailto:sage [2013/10/07(月) 08:43:06.72 .net] 研究会 -> 勉強会 199 名前：デフォルトの名無しさん [2013/10/07(月) 09:12:11.96 .net] >>197 撃沈の主な原因は何だったのですか？ そのころなら述語論理や集合論ではないと思うのですが 200 名前：デフォルトの名無しさん mailto:sage [2013/10/07(月) 09:27:05.81 .net] 計算機の性能だな 20年前のCPUの性能ではSAT SMTソルバーをぶん回すとかありえんだろう 201 名前：デフォルトの名無しさん mailto:sage [2013/10/07(月) 09:27:11.00 .net] >>199 隔世とは、大学の教養レベルの水準が上がっているのだなぁという 漠然とした印象です。 直接の原因はテキスト(>>162)にあったと思います。これに限らず、 勉強会がうまくいくかどうかには、早い段階で良い要約を誰かが 準備してくれるかどうかが大事ですが、それをしてくれる人が いなかった。それでほとんどの人に全貌が見えなかった。 202 名前：デフォルトの名無しさん mailto:sage [2013/10/07(月) 10:13:24.23 .net] >>195 スマン、言葉が足りなかったようだ >>193での「非形式的な矛盾」とは「(UMLのような)非形式手法における矛盾」のこと そして非形式手法においても矛盾(という概念)は(人間的な)直感として存在していることを言いたかった たとえそれが形式主義の視点では「意味不明な言明」であったとしても.... >>ただし、サブクラスというオブジェクト間の関係は(人の)直感として定義されたものだから、 >そういう関係もまた形式的に記述するんだよ。 形式手法であれば、構築しようとする体系(システム)におけるサブクラスという関係を (形式的に)定義するのは当然のことだね ここで、もしもサブクラスの(形式的な)定義に交換律を含めれば、 「XはYのサブクラスである」かつ「YはXのサブクラスである」(という仕様記述)は矛盾ではなくなる つまり、(形式手法の)証明ではサブクラス(というコトバ)から人が連想する直感的な意味は無視される たとえば、仮にサブクラス(というコトバ)の代わりに机や椅子(というコトバ)で仕様が記述されていても (無矛盾であることを)証明できるのが形式手法であり、それが非形式手法との違いになる 203 名前：デフォルトの名無しさん [2013/10/07(月) 12:14:52.74 .net] >>202 >交換律を含めれば 細かいのだが、ここは、反対称律を含めなければ、だな >つまり、(形式手法の)証明ではサブクラス(というコトバ)から人が連想する直感的な意味は無視される >たとえば、仮にサブクラス(というコトバ)の代わりに机や椅子(というコトバ)で仕様が記述されていても >(無矛盾であることを)証明できるのが形式手法であり、それが非形式手法との違いになる この辺り、ヒルベルト流の「形式主義」の説明なら妥当だが、ソフトウェア工学の「形式手法」の 説明としては相当ズレてると思う

---

---

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

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