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

■ このスレッドは過去ログ倉庫に格納されています
2013/01/05(土) 21:09:06.67
スレがないので立ててみた

参考ページ
http://en.wikipedia.org/wiki/Formal_methods
http://ja.wikipedia.org/wiki/%E5%BD%A2%E5%BC%8F%E6%89%8B%E6%B3%95
2013/03/17(日) 00:29:32.18
テストしにくいコードをテストする方法教えて下さい
http://toro.2ch.net/test/read.cgi/tech/1334408391/
でテストケースの自動生成で賑わってるけど同じ人？
2013/03/17(日) 06:38:43.65
2chなんかでクダ巻いて形式手法を批判した気になってるような低能は
そもそもVDMやAlloyを始めることすらしないからじゃないかな
76デフォルトの名無しさん
垢版 |
2013/03/17(日) 09:55:15.86
>>75
おまえは家来か
2013/03/17(日) 10:04:04.95
Alloy本読んで勉強中だが、結局のところ現実の問題をどうモデル化するかって
ところがまだよくわからん。
例題でさらっとキャッシュメモリのモデルなんか挙げていたが、あんなの思いつかん。
そのへん、なんかいい参考書ないかねぇ？
2013/03/17(日) 13:16:00.02
Alloyで数独を解くのが昔一部で話題になったけど
そういう数理パズルとかで遊んでみるとか
79デフォルトの名無しさん
垢版 |
2013/03/17(日) 18:09:45.06
>>77
そもそもふつうに思いつかんようなのがよいモデル化かな？
キャッシュメモリってどんな例題だったけ
ちょっと見てみるかな
2013/06/02(日) 21:23:41.48
業務ロジックを仕様記述言語で書くことは可能かな？
なんか、例を見てると並列処理の時の云々かんぬんとかかなりアルゴリズム的だったり、詳細よりだったりする例が多いのが気になる。

仕様のバグで一番多いのは論理矛盾だったりするので、
その辺が検出できそうなら導入してみたいんだよね。
2013/06/02(日) 22:55:50.61
業務ロジックがどういうものか知らないけど仕様記述自体はできると思うよ

ただ形式仕様記述ができることと
論理矛盾の検出ができることの間には大きな隔たりがあるのが現状

状態の数が限られているならなんとかなるけど
状態変数に実数とか時間を持つとなると途端に検証が困難になる
2013/06/04(火) 02:08:31.54
おお、そうなんだ。サンクス。

あんまりたいそうなロジックを扱ってるわけじゃないけど
取引ができる日がn日からm日で、そのうち取引ができるのはステータスがxの人で...

とか、まあ、そういったものの組み合わせが多いかな。
最悪、論理矛盾の自動検出が出来なくても、曖昧性の無い記述ができるなら
仕様漏れとかが減ったりしないかなぁ。
83デフォルトの名無しさん
垢版 |
2013/06/29(土) 13:32:51.16
>>80 >>81 >>82
> 業務ロジックを仕様記述言語で書くことは可能かな？
ていうか、そのためのものなんだがｗ
いまの仕様記述を見てたらそんなことも分かりにくいが
84デフォルトの名無しさん
垢版 |
2013/06/29(土) 13:57:51.79
組込みっていうか車載開発（ボディ系）でAlloyを個人的に使おうと思ったが、
難しくて挫折しそうになった。。。C言語しか知らないとつらい。。。
2013/06/29(土) 19:20:26.45
>>84
組込み系であれば、(Alloy/VDM/Zなどよりも)
「振る舞い」の検証を重視するCSPやCCSのほうが
(多くのケースでは)適しているのではないかと思われ

もしもこれら形式的記述スタイルに慣れていないのなら、
PROMELA(およびその処理系であるSPIN)はいかが？
C言語とステートマシンの知識があれば、直感で理解できる

最近は、PROMELA/SPINに関する日本語書籍もいくつかあるよ
2013/06/29(土) 21:00:02.42
アドバイスありがとうございました。
積読状態ですが、VDMにAlloyにSPINに書籍は購入済みですので、
一度読んでみます。

Alloyに手を出したのは、VDMやSPINの両方のおいしいところを合わせたのと、
手軽にモデリングできると聞いたからです。
・・・でも私には簡単ではなかったorz
2013/06/30(日) 23:16:19.56
世界的には業務ロジックの構築=DSL(ドメイン記述言語)の流れじゃなかったけ。
2013/07/06(土) NY:AN:NY.AN
DSLと形式手法は普通に両立すると思うが？
89デフォルトの名無しさん
垢版 |
2013/07/16(火) NY:AN:NY.AN
Rodinはまともなチュートリアルないんか。
Event Bの理論は本読んでどうにかするとして、ツールとしてのRodinの使い方が公式のチュートリアル見てもよくわからん。
2013/08/28(水) NY:AN:NY.AN
Code Contractsはこのスレの範疇？
2013/08/29(木) NY:AN:NY.AN
いいんじゃね？
2013/08/31(土) NY:AN:NY.AN
形式手法が実用にならないと言われる中で
Code Contractsは計算機科学とソフトウェア工学の中庸にあると思うけど
あんまり話題にならないね

Code Contracts目当てにProfessional買うことはないだろうから
Express Editionにも対応してくれればいいのに
2013/08/31(土) NY:AN:NY.AN
乞食と思われると残念だから補足するけど
利用するライブラリが契約されてないと利用者側が馬鹿を見るので
みんな契約すればいいのに！的な意味で
2013/09/09(月) 00:32:04.39
C++1yではConcepts復活すんのかな
2013/09/12(木) 18:51:59.14
prologじゃダメなの？（DSLも含めて）
2013/09/12(木) 21:25:52.57
>>95
そうね。少なくともDSLを記述して実行させるくらいなら
最初からPrologで書いてしまった方が気が利いていますね。
2013/09/12(木) 22:36:29.89
Prologで書かれた仕様を実装に落とし込むのは
自然言語で書かれた仕様を実装に落とし込む時とは
別の危うさがあるように思える

バックエンドに使うんなら何でもいいけど
2013/09/12(木) 22:38:55.18
具体化prz
2013/09/12(木) 22:49:54.07
？
2013/09/12(木) 23:22:19.80
スプレッドシードに書かれた自然言語の仕様書よりか、
prologの方が危ういって形式手法の危うさでも指すの？

wikipedia読む限り、形式手法が集合論と述語論理を扱う設計手法みたいだし、
その限りじゃprologで十分だよねとは思ったのだけれども、一体、何が悲しくて
alloyやZみたく仕様がデカくて、ノウハウを使い回せない言語が乱立してんだろ
2013/09/12(木) 23:47:46.69
自然言語よりPrologの方が危ういなんて書いてないだろ

Prologで十分だというのが仮に事実だとしてそれが何なの？
その事実はPrologが優秀であることの証明にはならないし
他の技術を否定する正当性も与えない
102デフォルトの名無しさん
垢版 |
2013/09/13(金) 00:20:22.87
述語論理を書くならprologは有力なツールでしょうね。

でも、そもそも我々は述語論理を扱いたいんじゃないんです。
むしろ触れずに済むなら、その方がきっといいんです。

目的を忘れて手段を論じても無益でしょう。
2013/09/13(金) 07:56:11.25
集合論や述語論理を徹底的に研究した人はそんなにはいない。
あまりこれに拘った仕様の言語は大半の人には使い難い。
Prologくらい世俗的で下支えとしては述語論理がありますよ
くらいの言語の方が万人向きでしょう、という話ですよ。
2013/09/13(金) 11:55:09.39
は？徹底的に研究する必要なくてソフトウェア開発の道具として利用するだけ
そもそも、集合論や述語論理のABCすら理解しないでAlloyやZを使う馬鹿いないだろ
2013/09/13(金) 11:59:30.78
>>104
そうだと思いますよ。
2013/09/13(金) 12:20:24.26
>>101
prologの優秀さは、その簡潔かつ可読性の高いコード。
無駄に仕様の大きな言語って、学習コストが高く、バグを誘発するだけ
少し前に途絶えた良い例がperlとcommon lisp
形式手法が集合論と述語論理を取り扱い、
その要件を満たす最小セットの記述がprologで済むのではないかと仮定したとき、
それに対するalloyやZがprologに対して如何なるアドバンテージがあるか
って書いたの
>他の技術を否定する正当性も与えない
技術を否定しない技術者って技術者に向いてないんじゃないの？
人権屋とか宗教家にでも転職したら？

>>102
目的が形式手法への適応で、そこに集合論と述語論理が含まれるので述語論理を扱います。
そもそも述語論理のABCを理解してない非技術者がalloyやZを使うのか疑問です
目的を忘れて仕様の膨れあがったツールがalloyやZではないのかといったのが、
>>100のレスにおける核となる主張であり、疑問です。
が、その達観した無益なレスを書いて気持ち良いですか？
107デフォルトの名無しさん
垢版 |
2013/09/13(金) 20:09:03.07
つか、Prologで仕様記述なんてどこでやってんの
2013/09/13(金) 20:34:26.75
>>106
>形式手法が集合論と述語論理を取り扱い、
>その要件を満たす最小セットの記述がprologで済むのではないかと仮定したとき、

その仮定「Prologは形式手法の要件を満たす」が間違っているんじゃないかね
述語論理だけを取り扱う、いわゆる純粋Prologの表現力は極めて乏しいものだ
Prologプログラミングでは、カットや高階述語(assertなど)の非純粋な操作が必然となる
結果からすると、形式手法の要件である「検証」をPrologは満たさないことになる

また、Prologは型付けの弱い言語だ
仕様を記述できたとしても、それに矛盾が無いことを「検査」できない
形式的な立場であれば、ある集合の要素はすべて同じ種類でなければならないが、
この種類、つまり型の一貫性をPrologでは保証できない点は、形式言語としては致命的な欠陥
2013/09/13(金) 20:42:25.00
>>108
「仕様が記述できたとしても、それに矛盾がないことを「検査」できない」
はおかしいだろう。

質問として実行すればいいのではないかな。定理証明の過程なのだから。
110デフォルトの名無しさん
垢版 |
2013/09/13(金) 20:47:12.33
では来週からPrologで仕様を書いてください。
2013/09/13(金) 21:04:25.47
>>109
やはり形式手法という概念そのものが理解できていないようだね
仕様を実行して振る舞いを確認するのは「シミュレーション(模倣)」と呼ばれる手法であり、
「(形式手法における)検証」ではない

定理証明の過程において、対象となる仕様は「一切実行されない」ことを理解しなければならない
これを実現するために、形式手法では厳密な数学を基礎に置き、それを元に証明を進める
2013/09/13(金) 21:16:04.80
>>111
なるほどね。わかった。
動的言語云々ということが書かれていたので検査が実行されるのだと
思ってしまった。
113112
垢版 |
2013/09/13(金) 21:22:31.21
まちがえた。
動的云々ではなく、「型付けの弱い言語云々」でした。
114デフォルトの名無しさん
垢版 |
2013/09/13(金) 22:19:56.75
でも形式手法をそういう言い方にするとAlloyやVDMの微妙さが際立ってしまうのだ
115デフォルトの名無しさん
垢版 |
2013/09/13(金) 22:56:23.06
>>108
型や集合なら事実を加えるなりの規約程度で、どうにか出来そうなイメージ
てか、形式手法って検証なんてステップあるのね。こうなると専用の言語つかった方がはやそう
けれど誰かプレーンなprologで時相論理のサブセットとか書いてないのかな
第五世代のprolog hackerたちが、このスレを通ることに期待age
2013/09/13(金) 23:21:23.48
>>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 を参考にしたステートマシンをモデルとし、
シミュレーション(=模倣)による振る舞いの確認が可能
最終的にはペトリネットへ変換して検証する予定だったけど、着手できぬまま放置している
2013/09/14(土) 01:22:47.81
VDM ToolsもOvertureも証明の機能が不十分だから
形式手法のレベルで分類すればVDMはもっぱら軽量じゃね？
まあこの際どうでもいいが
2013/09/14(土) 13:12:05.22
>>117
形式言語 VDM と形式言語処理系 VDM Tools をごっちゃにすべきではない
言語 C と 処理系 gcc(あるいは VC++) をごっちゃにするようなもの

言語としての VDM は形式的な証明が可能な体系
(ただし、それを機械的に適用できるか否かは別の話)
そして、処理系としての「VDM Tools はもっぱら軽量じゃね？」ならば、同意する
2013/09/14(土) 13:32:16.32
そりゃごっちゃにすべきじゃない文脈もあるだろうが

C言語の喩えで言えば
gccもVCも対応していない機能はないようなものでしょ

C言語の仕様策定は実装ありきだから
そのうち対応する見込みはあるけど
VDMで証明とかOverture界隈も興味の対象から外れている感じだし先が見えん
2013/09/14(土) 15:56:52.26
>>119
>C言語の喩えで言えば
>gccもVCも対応していない機能はないようなものでしょ

んなわきゃーない。なんのための言語規格だ。
2013/09/14(土) 16:17:21.73
言語規格だか何だか知らんが絵に描いた餅でも喰ってろ

VDM-SLはISO化されたが
VDM++に関しては文法こそ仕様はあるものの
挙動は実装が仕様みたいな状況だぞ
2013/09/14(土) 20:04:31.44
挙動なんて言ってる時点で
静的解析をガン無視してるのはVDM界隈じゃなくて>>121だということがわかる。
2013/09/14(土) 22:53:25.27
だったらVDMの静的解析に期待を持てるような
実績や活用法の情報をくれよ
2013/09/14(土) 23:08:58.11
>>123
「だったら」が何を指すのか意味不明だし、また静的解析みたいな曖昧な言葉を持ち出す

まだ >>123 は(言語としての) VDM における検証や証明を扱うレベルに達していないので、
無理に背伸びはせず(処理系としての) VDM Tools を触ることから始めたほうがいいと思われ
ただし、今のままでは軽量と言われる VDM Tools ですら理解するのは難しいと思うがね
2013/09/14(土) 23:15:08.44
>>122に言えよ
2013/09/14(土) 23:23:18.69
>>125を翻訳すると、

「>>122くんの言葉を真似しただけだから、僕ちゃん悪くないもん！！」
2013/09/14(土) 23:42:17.97
>>124
選民意識も結構だが
「馬鹿には無理」みたいなこというから形式手法が馬鹿にされる

ユーザに技術の存在を意識させないというのは
道具のあるべき姿の一つだが
stealth formal methodsなんてフレーズが生まれるのは何かおかしい
2013/09/15(日) 00:48:45.39
>>127
形式手法が何であって何ではないか、また形式手法では何ができて何ができないのか、
こんな基本的なことも>>123は分かっていないようだから、理屈よりも実践を、
つまり VDM Tools を触ることから/触れるレベルの学習から始めたほうがいいと
アドバイスしてるだけだがね

また>>127は「(形式手法の習得は)馬鹿には無理」と考えているようだけど、自分はそうは思わない
最低限必要なのは普通高校卒業程度の数学と教養であり、IT業界人やそれを目指す学生の大半が該当する
ただし、本人にヤル気が無ければ無理だし、たとえあっても素直さと謙虚さは必要だがね
2013/09/15(日) 07:45:12.05
>>123
つ 「型検査」
2013/09/15(日) 14:17:26.84
型検査なんかプログラミング言語で一般的過ぎて
期待も何もスタートラインだろ

整数（int, nat, nat1）とトークンだけで記述できる場合はまだしも
レコードやクラスを使い始めると
モダンなプログラミング言語に比べ使い勝手の悪さが目立つ

さらに証明までやろうとすると証明責務が無理ゲーになる

結果としてユーザが気軽に型を作れない
2013/09/15(日) 14:34:04.62
VDM++に関して言えば演算子オーバーロードはつけるべきだった
メソッド名に全角の≦とかを使うなんてバッドノウハウは見るに耐えない

インターフェイスやMix-inも言語レベルで対応してない
テンプレートやジェネリクスもない

これらはプログラマが楽するための道具に留まらず
データ表現を抽象化してロジックに意識を集中させるために
仕様記述に有効な機能じゃなかろうか
2013/09/15(日) 16:58:56.24
証明しにくくするだけ
2013/09/15(日) 18:02:44.28
仕様を書く人が
証明のこと気にしないといけないのが未成熟な証

ASTなり中間言語にさえ落とし込めさえすれば
あとは数学者やコンピュータサイエンティストの仕事だ
134デフォルトの名無しさん
垢版 |
2013/09/15(日) 18:22:03.16
そりゃないわ。
2013/09/15(日) 18:35:46.84
>>133
>あとは数学者やコンピュータサイエンティストの仕事だ

いや、それはAI(人工知能)の仕事だよ
自然語で書かれた曖昧な仕様を、コンピュータが理解できる機械語へ変換するという

もちろん、これが理想の姿であるのは理解するが、現時点では夢物語でしかない
だから、自然言語で書く曖昧な(非形式的な)仕様の代わりに、
(数学を元にした)形式的な仕様記述を試みよう、という思想が形式手法の出発点にある

>>133には、C.A.R. ホーアの言葉を送ろう：

　職業としてプログラミング業務を行うためには、基礎となる数学理論に基づき、
　すでに確立された他の工学分野の先例にならわなければならない。
　これは教育を改善することによって実現することができる。

　　　　　　　　　　　　　　　「プログラミング -- 魔術か科学か？」から引用
2013/09/15(日) 19:10:48.05
形式的な検証を目的に形式仕様を書くのなら
証明のことを気にするのは当然だろw
2013/09/15(日) 19:26:34.98
>>135
だからそのAIを作るのは数学者やコンピュータサイエンティストで
言語のユーザでも言語屋さんでもないだろ

>>136
気にした方が良い結果になることが多いだろうが
気にしないと使えないなら未熟だってこと
形式仕様を書くのは形式的な検証が主目的とは限らない
2013/09/15(日) 19:52:25.00
形式手法に限らず、大抵のものは「気にしないと使えない」だろ。
オブジェクト指向だって関数型だってCoqやAgdaだって、
記述目的を意識して書かないとクソな記述になるのと同じだろ。
2013/09/15(日) 20:06:00.03
程度問題だよ
少なくとも俺にとってはVDMとりわけVDM++は
仕様を記述するには気が利かないし面倒くさ過ぎる
そのくせ証明による検証も大して期待できない

勿論そう思わない人もいるだろう
そういう人は是非とも形式仕様記述を活用して普及に努めてもらいたい
2013/09/15(日) 21:08:48.08
>>137
>だからそのAIを作るのは数学者やコンピュータサイエンティストで
>言語のユーザでも言語屋さんでもないだろ

もちろん、そのとおりだよ
そして、AIの話題はスレ違いってことさ
2013/09/15(日) 21:25:23.64
スレチってほどでもないと思うけど
SATソルバの話題とかしてもいいんじゃね？
どうせ過疎ってるか
愚痴や揚げ足取りの応酬しかしてないんだし
2013/09/16(月) 00:03:43.85
そんなことより、皆さん、どうやってデッドロック回避してるの？
2013/09/16(月) 00:42:33.03
>>139
そういう態度を、評論家とかコメンテータという

まあ、自分で理解できないのを言語やツールのせいにするのが許されるのは、お子ちゃま迄だよ
2013/09/16(月) 19:32:39.59
どっちが先に根負けするか賭けようぜ
俺は最初の奴とみた
2013/09/16(月) 20:44:16.20
どっちって誰と誰だよ
2013/09/16(月) 20:50:19.99
ざーっと追ってあなたの思う両者でよかろう

傍観者的には、すでに1on1じゃなく途中から同意見者が混ざって混乱してる可能性もありそうに感じた
2013/09/16(月) 21:05:43.76
４，５人が入り混じった乱戦だろｗ
2013/09/16(月) 21:14:01.04
このスレで興味もってざっとぐぐってるんですが、なかなか面白そうな分野ですね。
書籍やサイトのお勧めあったらご教示願えると幸いです
149デフォルトの名無しさん
垢版 |
2013/10/02(水) 09:58:39.78
>>100 >>133 >>137
この人センスいいねえ

>>111 >>136
この人は単なる学習者
2013/10/03(木) 20:35:05.95
へー（ニヤニヤ
Zの言語仕様がデカいと思っている人のセンスがいいとか言うのって
本人以外考えられないけどw
151デフォルトの名無しさん
垢版 |
2013/10/03(木) 23:29:48.73
ニヤニヤすんな
要らん言うてんやろ
2013/10/04(金) 07:56:58.26
で、Zの言語仕様のどこがデカいわけ？
ぼくちゃん学習者なんで教えてくださいませ〜
2013/10/04(金) 08:42:40.94
>>152
単一化と導出・融合だけの pure Prolog に較べると途方もなく大きいのではないか。
2013/10/04(金) 09:17:10.07
Zの言語仕様には単一化もレゾリューションもNAFもないよ。
どうして実行機構を持たないZのほうが言語仕様がデカいと思うんだい？
2013/10/04(金) 10:09:22.67
言語仕様の大きさは
処理系やツールを実装する人にとっては重要かもしれないけど
ユーザにとっては重要じゃないよね。
何ができるか・何をしないといけないかが重要。
そしてそれは言語仕様の大きさと必ずしも対応しない。

言語仕様の大きさで議論しようというのがそもそも筋が悪い。
言語仕様を全部把握していないと使えない訳じゃあるまい。
2013/10/04(金) 10:19:02.52
結論：>>100は筋悪
2013/10/04(金) 10:20:01.06
その>>100を「センスいい」と言っちゃう>>149も筋悪。
2013/10/04(金) 12:53:16.23
すじわる、って将棋以外で聞かない単語だよね。
まあ筋が悪いとは普通に使うんだから字面を見てわかると思うけど。
159112
垢版 |
2013/10/04(金) 15:11:02.46
>>154
ここでいう言語仕様とは学習しなくてはならない範囲の
意味が強いと思う。そういう意味なら、一人で使う場合は
別だが、他者の形式仕様を読む場合にはひと通りは抑えて
いなくてはならず、Zはその点やはり負担が大きい。
2013/10/04(金) 16:02:12.94
Zは基本的に述語論理と型付集合論がわかってれば
覚えなければならない事はとても少ないだろ。
むしろVDMやAlloyあたりのほうが
述語論理や型付集合論以外の言語要素が多いと思う。

Zで苦労するのは他の言語/手法と比べてツールサポートが少ないことだろ。
2013/10/04(金) 16:30:35.19
>>160
Zについては、全てはこの本の後遺症だと思う。
http://amazon.com/dp/481018563X
2013/10/04(金) 16:33:28.90
http://www.amazon.co.jp/dp/481018563X
かな。
2013/10/04(金) 21:30:59.69
ＺもVDMも基本は70年代の言語だからなぁ

比較的新しい言語だとCafeOBJなんかがあるけど
二木先生の関わっていない利用例を知らない
164デフォルトの名無しさん
垢版 |
2013/10/04(金) 21:49:13.71
>>155
>言語仕様の大きさは
>処理系やツールを実装する人にとっては重要かもしれないけど
>ユーザにとっては重要じゃないよね。
誰にとっても同じだ。
同じことをするんなら小さい方がよいのに決まっとる

>>160
だからZは要らんと言っとる

>>163
CafeOBJが新しいのか
2013/10/04(金) 21:58:38.09
>>164
そんなに言語仕様が小さいのがいいのならBrainf*ckなんか最高だよね
チューリング完全だから「計算可能性の観点においては」
他の言語と同等のことができるよ
166デフォルトの名無しさん
垢版 |
2013/10/04(金) 22:06:34.37
観点は計算可能性だけじゃないだろ
まだチューリング完全なんて言ってるのか
2013/10/04(金) 22:10:26.71
観点は言語仕様の大きさだけじゃないだろ
って話だよ
チューリング完全ならどれも一緒だなんて誰も思っちゃいねーよ
168デフォルトの名無しさん
垢版 |
2013/10/04(金) 22:30:01.22
だれかこの辺の議論のような口喧嘩のようなことを交通整理できる人はいないでしょうか
2013/10/04(金) 23:00:21.87
そういった態度というのは単に自信が無いだけなので、
生暖かく放置すればいいのではないかと思われ
2013/10/04(金) 23:07:34.51
ところで、Prologで仕様記述やその検証ができるなら試してみたいんだが、
その方法を解説した本やWebサイトとかあるのかな？
「理論的にはできるはず」だけだとProlog自体よく知らない俺には無理だが。
171デフォルトの名無しさん
垢版 |
2013/10/04(金) 23:08:43.39
あんたは自信があるのかい
2013/10/04(金) 23:32:01.69
>>170
>ところで、Prologで仕様記述やその検証ができるなら

できないんじゃね？
過去には「できるはず...」という願望もしくは妄想に基づく意見(>>95-)はあったけど、
それに対する反論には何も意見を言えず議論を終えた
個人的には、型の無い純粋Prologを形式言語と呼ぶには無理があると考える

Prologへの願望を語りたいという気持ちは理解できるが、
それはPrologスレで大いに語ればいい、それが妄想であってもいい
2013/10/05(土) 05:30:54.75
Prologで仕様記述しますなんていう例は山ほどある。
知らないんなら論文読まなさすぎ。

どれも結論は
「表現力不足だよね」
「表現上の制限が強すぎて、かえって表現が冗長になってダメだね」
「最低限FOLは必要だよね、やっぱし」
なわけだが。
2013/10/05(土) 05:33:52.83
>>164
>だからZは要らんと言っとる

つまりZの言語仕様はデカくないという意見に反論できないってことね。
理由も言えずに「要らん」としか表現できない人が形式仕様とか、鼻で笑っちゃうねw
■ このスレッドは過去ログ倉庫に格納されています
5ちゃんねるの広告が気に入らない場合は、こちらをクリックしてください。
ニューススポーツなんでも実況