- 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
- 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
>交換律を含めれば
細かいのだが、ここは、反対称律を含めなければ、だな
>つまり、(形式手法の)証明ではサブクラス(というコトバ)から人が連想する直感的な意味は無視される
>たとえば、仮にサブクラス(というコトバ)の代わりに机や椅子(というコトバ)で仕様が記述されていても
>(無矛盾であることを)証明できるのが形式手法であり、それが非形式手法との違いになる
この辺り、ヒルベルト流の「形式主義」の説明なら妥当だが、ソフトウェア工学の「形式手法」の
説明としては相当ズレてると思う
- 204 名前：デフォルトの名無しさん mailto:sage [2013/10/07(月) 17:30:11.68 .net]
- >>203
識別子の字面に引きずられるようなら、その時点で形式手法を使う意味は半減するよ。
形式仕様を読み書きする時には、字面が持つ自然言語的意味を無視して
あくまで記号操作の対象として扱う。
識別子の字面が大事になるのは、形式手法を知らない人に説明する時。
「形式的に」扱う訓練を受けていない人のために非形式的意味を使う。
非形式的な意味を持たせた時点で、その記述は形式仕様ではなくなる。
- 205 名前：デフォルトの名無しさん mailto:sage [2013/10/07(月) 20:32:26.92 .net]
- pi = 3.14159
e = 2.71828
と
e = 3.14159
pi = 2.71828
で「後者に違和感を持つのは間違い」という奴の
形式仕様は読みたくないな
形式仕様からプログラムコードを自動生成してメンテナンスフリーというならともかく
それがソフトウェアなり何なりの「仕様」を定めている以上
非形式的な意味は持たせてもいいし
それによって非形式的仕様になる訳じゃない
非形式的な意味は形式的検証の結果に影響を与えないのだから
- 206 名前：デフォルトの名無しさん [2013/10/07(月) 20:40:11.24 .net]
- >>205
>形式仕様を読み書きする時には、字面が持つ自然言語的意味を無視して
>あくまで記号操作の対象として扱う。
そんなことをは君（人間）は気にする必要はないのだ。
放っておいても証明器は完璧にそうしてくれる。
同じことを君（人間）がやってもそれこそ効果は半減する。
書くことは人間にしかできないのだが，そのとき「記号」で書いていては，
そもそもどういう対象を書いているかが分からないだろう？ｗ
>「形式的に」扱う訓練を受けていない人のために非形式的意味を使う。
訓練を受けているとかいないとかでなく、どんな相手だろうと、何を書いて
いるかを伝えるためには、単なる記号では伝わらないんだよ。
>非形式的な意味を持たせた時点で、その記述は形式仕様ではなくなる。
これも違う。人間がどういう読み方をしようと、machine readableであれば
形式仕様なんだよ。
あと、君が「形式手法を知らない人」「訓練を受けていない人」とよく
言ってるらしいのが気になるな。
- 207 名前：206 [2013/10/07(月) 20:42:57.52 .net]
- 誤 >>205 すまん
正 >>204
- 208 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 02:10:26.26 .net]
- ここで思いのたけを質問したらどうですか？
topse.or.jp/2013/10/2023
- 209 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 17:34:58.34 .net]
- >>206
>これも違う。人間がどういう読み方をしようと、machine readableであれば
>形式仕様なんだよ。
じゃあポインタをキャストしまくってるCのソースも形式仕様だねw
- 210 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 17:39:04.75 .net]
- >>206
>同じことを君（人間）がやってもそれこそ効果は半減する。
残念ながら、その形式言語の表現力がFOL以上であれば、
(非定理を含む)あらゆる式を自動的に証明可能なアルゴリズムは存在しない。
- 211 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 17:41:09.34 .net]
- >>205
>e = 3.14159
>pi = 2.71828
まさに、こういうまやかしに惑わされないために
先入観を排して記号を記号として扱う訓練が必要なんだよ。
- 212 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 18:46:34.06 .net]
- エラーや例外が発生しないプログラムが必ずしも「正しい」訳じゃないように
形式的に無矛盾な仕様が必ずしも「正しい」訳じゃない
無矛盾な証券決済システムの仕様は
鉄道運行管理システムの仕様としては全くもって正しくない
記号を記号として扱うのは機械でもできるし機械の方が得意だ
しかし形式意味論では扱わない記号に込められた「意味」を読み取るのは
現状では人間にしかできない
機械が得意なことは機械に任せて
人間は人間にしかできないことに力を入れる方が得策だろう
- 213 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 19:41:41.07 .net]
- >>212
なら自然言語とか図形言語で仕様書いてれば？
- 214 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 19:51:16.96 .net]
- 機械が形式仕様を書いてくれるようになったら
やってもいいかもね
- 215 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 20:22:13.24 .net]
- >>214
それが可能ならそれこそ形式仕様なぞ不要だな
そもそも何でも証明器で検証するのが前提になってる>>206は
形式手法にどんな夢を見ているんだ？
>>206
> 放っておいても証明器は完璧にそうしてくれる。
> 同じことを君（人間）がやってもそれこそ効果は半減する。
残念ながら証明器は放っておいても何もしてくれない。
証明器を有効に使うために必要なエフォートを知った上での
主張とは思えない。
> どんな相手だろうと、何を書いて
> いるかを伝えるためには、単なる記号では伝わらないんだよ。
piを「円周率」として読むレベルの厳密さで良いのであれば、
拘束文法による半形式仕様で十分だ。
- 216 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 20:40:26.34 .net]
- >>215
とりあえず俺は>>206じゃないが
複数の人間の発言を一緒くたにされても困る
>>そもそも何でも証明器で検証するのが前提になってる
証明器での検証を前提としない軽量形式手法においては
人間に意味が伝わらない仕様は使い物にならない
形式仕様は自然言語の曖昧さの排除が目的であって意味の排除じゃない
> 残念ながら証明器は放っておいても何もしてくれない。
人間が記号を記号として扱ってメタな意味を排除すると証明器は何かしてくれるの？
- 217 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:11:58.28 .net]
- >>216
> 証明器での検証を前提としない軽量形式手法においては
全てを証明器でやるわけではないからといって、
必ずしも証明器での検証を前提としないわけではないだろう。
形式仕様スレでこんな論理の基礎を指摘しなきゃいかんのか？
> 人間が記号を記号として扱ってメタな意味を排除すると証明器は何かしてくれるの？
はあ？
まだ証明器が何もかもやってくれるとでも思ってるのか。
証明器はドラえもんのポケットじゃないぞ。
- 218 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:17:28.76 .net]
- 言葉が通じないというか
相手の発言の意図を汲もうという気が感じられないな
- 219 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:19:40.69 .net]
- 発言の意図を汲み取ってクレクレ言う人が形式手法とは恐れ入った！
- 220 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:27:43.77 .net]
- 現行の証明器の能力が限られてることと
人間が非形式的な意味を排して形式仕様を読まなければいけないことの間に
随分と論理の飛躍があると思うんだけど
非形式的な意味を排して形式仕様を読める能力が必要だとして
形式仕様から非形式的な意味を読み取るor
形式仕様に非形式的な意味を書き記す能力が
同時に成立しない・成立させてはいけない理由は何？
両方の能力が必要なんじゃないの？
- 221 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:28:51.63 .net]
- >>212
>無矛盾な証券決済システムの仕様は
>鉄道運行管理システムの仕様としては全くもって正しくない
ミスリードが2つある。
1つ目は、無矛盾な証券決済システムの仕様があったとしても
その仕様が証券決済システムの仕様としてvalidとは限らない。
なのにあたかも証券決済システムとしてvalidであるかのように、
鉄道運行管理システムの仕様としてinvalidだと主張している。
2つ目は、条件なしに「全くもって正しくない」と書いていることから、
「全ての」無矛盾な証券決済システムの仕様が
鉄道運行管理システムの仕様として「完全にinvalid」だという主張になる。
これは正しくない。
無矛盾な証券決済システムの仕様のうちいくつかは
鉄道運行管理システムの仕様としてinvalidな部分がある、
というならば、それはそうだろう。
もっとも、
無矛盾な証券決済システムの仕様のうちいくつかは
証券決済システムの仕様としてinvalidな部分がある、
も正しいがな。
|
 |
