【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/01/05(土) 21:33:15.76

このスレッドは天才チンパンジー「アイちゃん」が
言語訓練のために立てたものです。

アイと研究員とのやり取りに利用するスレッドなので、
関係者以外は書きこまないで下さい。

　　　　　　　　　　　　　　　　　　京都大学霊長類研究所

**デフォルトの名無しさん** · 2013/01/06(日) 01:05:45.32

>>1乙
VDMはともかくAlloyってこの分野で流行ってるの？

**デフォルトの名無しさん** · 2013/01/06(日) 01:16:08.51

ついでだからIPAの報告書
（個人的には形式手法を良とするバイアスがかかっているように思うが）

「形式手法適用調査」報告書
http://sec.ipa.go.jp/reports/20100729.html

「情報系の実稼働システムを対象とした形式手法適用実験報告書」
http://sec.ipa.go.jp/reports/20120420.html

形式手法導入課題を解決する「形式手法活用ガイドならびに参考資料」
http://sec.ipa.go.jp/reports/20120928.html

実務家のための形式手法教材「厳密な仕様記述を志すための形式手法入門」
http://sec.ipa.go.jp/reports/20121113.html

**デフォルトの名無しさん** · 2013/01/06(日) 01:23:51.63

第3回形式手法の産業応用ワークショップ（予稿・スライド）
http://cfv.jp/cvs/event/workshop/2012/09/

第2回・第1回へのリンク有

**デフォルトの名無しさん** · 2013/01/08(火) 01:54:13.02

特許庁の新システム入札やり直すらしいけど
ああいうのこそ形式手法を適用する意義がありそうなものだが

形式手法によってデスマが回避できるというよりは
デスマを回避できる体力があるから形式手法を採用できるってのが
実際なのかもしらん

**デフォルトの名無しさん** · 2013/01/08(火) 06:49:04.96

Alloyの本

抽象によるソフトウェア設計－Alloyではじめる形式手法－
http://www.amazon.co.jp/dp/4274068587

形式手法の本

形式手法入門―ロジックによるソフトウェア設計―
http://www.amazon.co.jp/dp/4274211886/

**デフォルトの名無しさん** · 2013/01/11(金) 06:24:10.24

>Alloy
あー、あの赤いやつね
途中であきらめました

**デフォルトの名無しさん** · 2013/01/11(金) 06:27:52.78

どこで諦めたの? 自分は結構楽しめた。

**デフォルトの名無しさん** · 2013/01/11(金) 22:54:26.79

あきらめたというかフェードアウトした感じかな
たしか半分くらいまでは読んだけど、いつの間にか
読むのをやめてた

形式手法はまったくの素人だったので（今も）
よく分からんかった

**デフォルトの名無しさん** · 2013/01/17(木) 10:49:33.93

>>4 >>5
>IPAの報告書　>第3回形式手法の産業応用ワークショップ
見たけど相変わらずだな。使い物にならんよあんなのじゃ。
人材いないんだなこの方面。

**デフォルトの名無しさん** · 2013/01/18(金) 03:26:26.90

国内だと人材が少ない（しかも学術寄りの人の方が多い）
ってのは実感としてある

形式手法は静的解析のツールとして利用される道の方が明るい気がする
人間が読み書きする形式言語が使い物になる日は来ないと思う

**デフォルトの名無しさん** · 2013/01/18(金) 17:38:42.62

>>12
うん。学術系はだめだ。
実務に近いSRAがやや骨があるようだが。
>人間が読み書きする形式言語
これはどう言う意味かわからんが
>使い物になる日は来ないと思う
そんなことはない。一流人材が参戦すれば変わる。

**デフォルトの名無しさん** · 2013/01/18(金) 19:43:02.15

仕様記述に10日かけて、
プログラムを自動生成して3日で納品できるようになるとすると
ビジネスのありかたとしては
仕様記述で工数を計上して費用請求することになって
今までの設計と大差ないことになるのジャマイカ

**デフォルトの名無しさん** · 2013/01/19(土) 00:19:45.43

>>14
なにが大差ないと言っているのかよくわからん。

**デフォルトの名無しさん** · 2013/01/19(土) 01:08:35.95

費用や納期だけで評価したら大差ないってことでしょ

現状ソフトウェアの品質を正当に評価していない（できない）から
形式手法を導入するインセンティブが働かない

てかageる必要あんのか？

**デフォルトの名無しさん** · 2013/01/19(土) 01:18:12.83

>>15
とある情報システムを開発するのにかかるコスト
とか
予算や開発期間がオーバーするリスク
とか

**デフォルトの名無しさん** · 2013/01/19(土) 12:16:55.38

>>11 >>14 >>17
確かに今までの形式手法ではそうだ。
論文を書きたいだけの奴にはそれでいいんだろ。
>>16
品質は費用納期に反映されるので、それは形式手法側の言い訳だ。

**デフォルトの名無しさん** · 2013/01/19(土) 13:05:09.39

>>18
論文と現場の乖離を示唆しながら
>品質は費用納期に反映される
はねぇだろ

営業や契約担当じゃないから実態は知らないが
発注元は
「フィールドバグ○件以下。超過した場合は違約金！」
とか契約文書に書けるの？

逆に請負側（候補）は
形式手法の適用が要件に入っていない案件で
「我が社は形式手法を導入しているのでちょっといいお値段です！」
で競争に勝てるというの？

「我が社で納期が短縮できるのは形式手法で開発の手戻りを低減するからです！
品質下げる訳じゃありません！」
とか発注元に説明すんの？

**デフォルトの名無しさん** · 2013/01/19(土) 13:53:26.32

>>19

>「フィールドバグ○件以下。超過した場合は違約金！」
>とか契約文書に書けるの？
そりゃ書ける場合もあるよ。
それに、バグが多いと、当然後の注文もなくなってくるだろ。

>「我が社は形式手法を導入しているのでちょっといいお値段です！」
それは、顧客にとってのメリットを言っていないので、その時点でダメだよ。

>「我が社で納期が短縮できるのは形式手法で開発の手戻りを低減するからです>！品質下げる訳じゃありません！」とか発注元に説明すんの？
黙って短い納期でやればいいだけだろ。それは顧客にとってメリットだし、
こっちも短くなった分、他の仕事ができるし。

ほんとに使える形式手法とはこういうものなんだよ。

**デフォルトの名無しさん** · 2013/01/19(土) 14:57:17.31

話が通じていないな

・ソフトウェアの品質を規定する統一的な指標がない
・既存の品質指標は開発手法に依存することが多い
　（形式手法を適用した場合としない場合の公平な比較が困難）
・形式手法を要件に入れると対応できる業者が制限される

このため形式手法を導入するメリットが明確な「発注」がそもそも少ない
（メリットが明確なセーフティクリティカルやミッションクリティカルな案件では
現状でも形式手法が成果を上げている）

潜在的需要があっても表面上需要が無ければ
請負側に働く形式手法導入のインセンティブは弱い

**デフォルトの名無しさん** · 2013/01/19(土) 15:15:19.07

請負側としては

同じ業者から大きな案件を頻繁に受注するケースは少ない
評判に期待して今回頑張っても次回の受注がいつなのかは分からない

いつ効果が表れるか不明確な投資はやりにくい
業界全体で評判になるほどの成果を上げるのは体力に余裕がないとできない

しかも形式手法が扱える業者は多くないが
形式手法だけで需要を独占できるほどの特殊性はない

**デフォルトの名無しさん** · 2013/01/19(土) 15:23:25.33

請負側開発者・マネージャとしては

形式手法によりコストや納期を圧縮できるかもしれないが
勉強やらに費やした分だけ自分の給与が上がる保証はない

訳のわからない仕様書から解放されるといった
現場の幸せを要求しても経営判断には反映されにくい

**デフォルトの名無しさん** · 2013/01/19(土) 15:44:33.85

高階関数とかのようなメタプログラミング機構がなくて言語としては貧弱なのも欠点

**デフォルトの名無しさん** · 2013/01/19(土) 16:08:35.77

まあ今の形式手法の状況認識はそれでいいんじゃないか
>セーフティクリティカルやミッションクリティカルな案件では
現場にとってはそういうニッチなところで使うもので、
平凡な研究者にとっては、やればできると分かっている事をやれば少しは
論文が書けるというそんなものなんじゃないか？
それじゃつまらんけどね

**デフォルトの名無しさん** · 2013/01/19(土) 19:06:51.37

新参で申し訳ないんだけど
形式言語で書いた仕様書は発注側が用意するの？
受注側が用意するの？

**デフォルトの名無しさん** · 2013/01/19(土) 19:55:52.90

形式手法は商習慣まで関知せんよ

発注側「こういうもの作って」→受注側「言われたものを作りました」
という関係がものづくりとしては自然に思えるが
日本のICT業界は往々にしてこうはなっていない

上流で形式仕様を作成する場合
ユーザ企業はまずコンサル会社や大手ベンダに
「形式仕様作成と検証」といった発注を出すんじゃないかな
特に日本の場合は要求分析もセットになるかもしれない

**デフォルトの名無しさん** · 2013/01/19(土) 20:55:25.43

C++の新規格のドラフトにaxiomsっていうのがあったんだけど
結局却下されちゃったんだよな

**デフォルトの名無しさん** · 2013/01/20(日) 18:35:51.46

>>25
そっち方面の学界が腐敗とまでは言わんが競争がなく濁ってるんじゃないか？
だから一流人材が出て来ない。

**デフォルトの名無しさん** · 2013/01/20(日) 23:53:12.74

>>29
ム板でいうのも何だけど
おまえ何様だよ

**デフォルトの名無しさん** · 2013/01/22(火) 23:33:47.71

シンタックスはともかくセマンティクスにおいて
VDM++のまともな仕様って無いの？
曖昧さを持った言語で形式仕様記述とか欺瞞じゃね？

VDM-10のVDM++のが
枠組みはしっかりしてるけど事実上使えないし
Overture界隈はVDM-RTに傾倒してる感じだし
何かみんなおでこ広いし

**デフォルトの名無しさん** · 2013/01/26(土) 00:09:26.58

>>13
> >人間が読み書きする形式言語
> >使い物になる日は来ないと思う
> そんなことはない。一流人材が参戦すれば変わる。

その一流の人材が膨大な人数どうやって確保するの？
形式仕様言語でフルに仕様を書けばプログラムコードと同じオーダーの行数になるという経験則がある。
つまり数人で作れるおもちゃのソフトウェアならともかく、社会の根幹を支えそれが故に信頼性が必須とされる
大きなソフトウェアは現在の大規模開発でプログラミングに関わってる膨大な人数と同じオーダーの
形式仕様記述者が必要になるってことだ。

それだけ莫大な人数のそんな高い質の人材が世界のどこにいるんだい？
寝言は寝てから言った方がいいよ。

それに数人のプロジェクトに限定しても、それを一流の人材で仕様記述しても
それで作られたソフトウェアの寿命がある間は、そいつのメンテナンスのために
ずっと一流の人材を貼りつけておかないと、彼らが書いた形式仕様なんて難しいものは
２流の人材じゃ読み書きできないから保守できないよね。ってことで一流の人材ほど
彼らが書いた仕様のお守をさせられて他の仕事ができなくなる。

これって素晴らしい才能の無駄遣い法だね。

**デフォルトの名無しさん** · 2013/01/26(土) 12:32:30.58

一流の人材を活用するとしたら
二流・三流の人が使える形式手法の技術を確立することだろうね

そういう意味では一流の人材は既に集まっている
ただ二流・三流が何たるかを理解できていない可能性はある

**デフォルトの名無しさん** · 2013/01/26(土) 19:14:58.59

用語定義で「名前： 2chに書き込むときの名前」てなこと書いておきながら
本編に「家で飼っているぬこの名前は～」
とかしれっと書く奴はメタメタにしてやんよ！

軽量形式手法なんて形式手法じゃねぇと思ってたが
名を捨てて実を取ることも必要だと感じた。

**デフォルトの名無しさん** · 2013/01/27(日) 23:46:08.13

>>32
>形式仕様言語でフルに仕様を書けばプログラムコードと同じオーダーの行数に
>なるという経験則がある。
だからあ！そういう今の形式仕様言語が糞なんだよお！まだ分からんのかあ！

**デフォルトの名無しさん** · 2013/01/28(月) 01:17:16.05

>>35
> >>32
> >形式仕様言語でフルに仕様を書けばプログラムコードと同じオーダーの行数に
> >なるという経験則がある。
> だからあ！そういう今の形式仕様言語が糞なんだよお！まだ分からんのかあ！

ならば、形式仕様でフルに仕様記述するのが現実に可能だと主張したいのならば、
今のクソのでない形式仕様言語を現実に作ってからにしろ。

現実に存在しない夢のような形式仕様言語の存在を前提として>>13を主張するのは
単なる精神病患者だよ、誇大妄想と言う名前のな。

形式仕様屋にはこの手の誇大妄想患者が多すぎる。だから信用をなくして来たんだよ。

**デフォルトの名無しさん** · 2013/01/28(月) 01:22:14.84

>>13は今のクソでない形式仕様言語を現実に作るために、一流人材が参加すれば可能だと述べているんだろ。
とはいえ、この論旨を許せば一流人材とやらがいれば世界征服すら可能になるが。

**デフォルトの名無しさん** · 2013/01/28(月) 08:48:24.11

いまはむしろ誇大妄想がいないのが痛い。
だからユーザがプログラムと同じじゃないかと当たり前の苦情を言っても、
夢のような期待をするなと逆切れしてくる。

**デフォルトの名無しさん** · 2013/01/28(月) 08:56:42.23

>>37
クソでない形式言語を作るのは世界征服と並ぶほど難しいことなのでしょうか？

**デフォルトの名無しさん** · 2013/01/28(月) 18:52:03.46

フルフル君さ、ちょっと聞きたいんだけど、どういう意味で「フル」って言ってる？
フルに詳細化された仕様？
そりゃロクに抽象せずに詳細化された仕様をベタに書けばプログラムソースと同様になるわなw

**デフォルトの名無しさん** · 2013/01/28(月) 19:23:10.47

また抽象なんて甘いこと言って逃げるｗ
ベタに書いたらプログラムと同等なるならダメなんよ

**デフォルトの名無しさん** · 2013/01/28(月) 19:29:38.21

逃げるも何も、それが仕様記述言語のポイントだろ…（呆

**デフォルトの名無しさん** · 2013/01/28(月) 19:31:37.37

で、フルってどういう意味で言ってんの？

**デフォルトの名無しさん** · 2013/01/28(月) 19:41:09.93

よし。アンタの言う仕様記述言語のポイントは何か、逃げずに言ってみろ。

**デフォルトの名無しさん** · 2013/01/28(月) 20:14:25.27

フルフル君でもそれに噛みついている人でもないが

記述量は確かに実用上の課題ではあるけども
プログラムコードと同じオーダーなら駄目で短いならOKって
単純な話ではないと思うんだが

自然言語による仕様書の記述・検証の工数を無視しているのは意図的か？

それに形式的検証まで含むか否かで大きく変わる
証明された信頼性とテストによる確率的な信頼性は比較できない

自動コード生成が可能かどうかでも大きく変わる

**デフォルトの名無しさん** · 2013/01/30(水) 07:46:32.50

PGが仕様記述言語でプログラム書いてるから、
プログラムと同じ長さになるんじゃね？

**デフォルトの名無しさん** · 2013/01/30(水) 18:32:23.88

その「仕様記述言語」は、もはや一種のプログラミング言語じゃ？

**デフォルトの名無しさん** · 2013/01/30(水) 20:20:25.03

プログラム言語を含んでいる仕様記述言語は多いね。
プログラム言語部分だけで仕様を書いちゃう人が
仕様がプログラムと同量だとか言い出すんだろうね。

**デフォルトの名無しさん** · 2013/01/30(水) 22:00:41.42

>>45 >>46 >>47 >>48
仕様記述言語とプログラミング言語はどこが違うものなの？

**デフォルトの名無しさん** · 2013/01/30(水) 23:21:07.11

>>49
目的が違う

実際のところ言語やターゲットとなる案件によっては
プログラミング言語でも仕様記述は不可能ではないし
仕様記述言語で実行可能なコードを書くこともできる

道具として両者を近づける試みも多数なされているが
仕様と実装をごっちゃにしようという話ではない
あくまで仕様と実装は別の概念

**デフォルトの名無しさん** · 2013/01/31(木) 04:28:00.46

適切な抽象度を設定すればいいんだろうけど
仕様と設計がごっちゃになってくるから
「俺は今何を書いてるんだろう」ってなってしまう…
VDMどうのこうのより、そもそもの設計経験とか抽象化の力が足りないってのが問題

**デフォルトの名無しさん** · 2013/01/31(木) 21:59:30.67

曖昧だったり矛盾を含んだりしている
自然言語の仕様書が幅を利かせすぎという面もある

世の中の仕様書が如何にいい加減か実感できるという点だけでも
形式的仕様記述を「体験」する意義は十分だと思うね

**デフォルトの名無しさん** · 2013/01/31(木) 23:37:20.78

>世の中の仕様書が如何にいい加減か実感できるという点だけでも
>形式的仕様記述を「体験」する意義は十分だと思うね
形式的仕様ってその程度で満足してもらえるんだ。進まんはずだ。

**デフォルトの名無しさん** · 2013/02/01(金) 00:36:31.59

>>53
形式的仕様が誰かor何かに満足してもらえる
なんて話はしていないと思うんだが

意図的なのか読解力がないのか分からんが
オナニーなら一人でやってくれ
他人を使うな

**デフォルトの名無しさん** · 2013/02/01(金) 04:35:25.45

>>53
>形式的仕様ってその程度で満足してもらえるんだ。進まんはずだ。

ほら、この日本語文1つ取っても書いた本人以外には意味不明だろ？

**デフォルトの名無しさん** · 2013/02/01(金) 06:55:33.02

自然言語で契約交わすからこそ
世の中まわるという事実を無視されてもな…
まぁクリティカル系はしらんが
一般には無用だよな

**デフォルトの名無しさん** · 2013/02/01(金) 20:30:05.57

別に契約書を形式言語で書くわけじゃあるまいし
自然言語で契約する＝>世の中まわる
が真であろうと偽であろうと
形式的仕様の有用性を否定する理由にはならんよ
もちろん肯定する理由にもならないが

**デフォルトの名無しさん** · 2013/02/01(金) 20:32:08.41

契約書に形式仕様が記載された例もあるらしいぞw

**デフォルトの名無しさん** · 2013/02/02(土) 21:42:41.80

>>54 >>55
だから
>世の中の仕様書が如何にいい加減か実感できるという点だけでも
こんなことはたいしたことじゃないと言ってるんだよ
つまらんこと言うな

**デフォルトの名無しさん** · 2013/02/02(土) 22:44:26.94

たかが「体験する価値」にそんな高い敷居を設定するのか
つまらん奴だな

**デフォルトの名無しさん** · 2013/02/03(日) 08:34:30.94

形式言語で仕様を記述したら
テストパターンが自動生成されて
テストツールに食わせたら自動でテストやってくれる
ようになったら勉強しよう

**デフォルトの名無しさん** · 2013/02/03(日) 19:55:15.40

>>61
お望みのレベルに達していないだろうけど
テスト自動生成なら既に実施例や商品があるよ
産総研でも研究してたはず

モデル検査でSATソルバ使うのが流行ってるっぽいんで
テストケース生成技術・ツールはもう少し発展しそう

形式手法ではないがテストを仕様に近づけるというアプローチでBDDというのもある
ただC++で使いやすいフレームワークは知らない

**デフォルトの名無しさん** · 2013/02/12(火) 20:50:42.97

実装がフレームワークとかで制限されているときって、VDMとかどう使うのがベターなんだろうか？
VDM仕様も制限するのか、VDMと実装との差はしょうがない、ってするのか
よくわかんにゃい

**デフォルトの名無しさん** · 2013/02/12(火) 23:28:00.22

とりあえずinv, pre, postで十分に制約がかけられているんなら
関数・操作の中身が実装と異なっても問題ないんじゃね

あとは使い方次第としか
そのフレームワークの特性にも依存するし

**デフォルトの名無しさん** · 2013/02/14(木) 19:11:21.64

とりあえず、そのフレームワークに食わせるハンドラやコンポーネントの
インターフェースを陰仕様で固めてみたら？

**デフォルトの名無しさん** · 2013/02/14(木) 21:53:35.90

>>64 >>65
ありがとうございます。まずは陰仕様ってことですね
とにもかくにも書く目的をしっかりしないとダメですね

**デフォルトの名無しさん** · 2013/02/22(金) 11:18:28.53

こういう従順な人はしばらく騙せるかもしれんが、まあ今の仕様記述言語は
使えんことはこのスレを見ていてもすぐにわかるな。
>一般には無用だよな
そうだな。
一生懸命擁護弁護しようとしているのがいるがなんでなの？
だからスレも伸びん

**デフォルトの名無しさん** · 2013/02/23(土) 00:41:19.99

具体的な提案もなしに絡んでくるのがいるがなんでなの？
駄目だと思うのは勝手だし2chに愚痴を書くのも勝手だが
批判できる立場かね？

擁護弁護したいんじゃない議論がしたいんだよ

**デフォルトの名無しさん** · 2013/02/23(土) 00:51:39.71

SIL4クラスの安全にかかわる案件に絡んでいるが
優秀な人間が何人も集まって検討した仕様にすら穴がある
これはもう自然言語でやっている限りどうにもならないだろう

現状の形式手法では十分なソリューションたりえないのも事実だが
期待できるのは形式手法くらいしかないのも事実だ

現状が駄目だからといって将来が絶たれてよい技術ではない

**デフォルトの名無しさん** · 2013/02/25(月) 04:48:36.69

仕様の情報伝達力不足は SysML とかで補えばいいんでないの？

**デフォルトの名無しさん** · 2013/02/26(火) 04:49:05.67

誤解しているようだが
そういうのについてのスレなんだが

**デフォルトの名無しさん** · 2013/03/01(金) 20:47:27.99

>現状の形式手法では十分なソリューションたりえないのも事実だが
>期待できるのは形式手法くらいしかないのも事実だ

そうなんだが、あまりに不満足な現状だとはおもわんか？

**デフォルトの名無しさん** · 2013/03/16(土) 23:22:52.05

それみろ。まったくスレがのびんだろ
ＶＤＭはもちろんＡｌｌｏｙですらその程度なんだよｗ

**デフォルトの名無しさん** · 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を始めることすらしないからじゃないかな

**デフォルトの名無しさん** · 2013/03/17(日) 09:55:15.86

>>75
おまえは家来か

**デフォルトの名無しさん** · 2013/03/17(日) 10:04:04.95

Alloy本読んで勉強中だが、結局のところ現実の問題をどうモデル化するかって
ところがまだよくわからん。
例題でさらっとキャッシュメモリのモデルなんか挙げていたが、あんなの思いつかん。
そのへん、なんかいい参考書ないかねぇ？

**デフォルトの名無しさん** · 2013/03/17(日) 13:16:00.02

Alloyで数独を解くのが昔一部で話題になったけど
そういう数理パズルとかで遊んでみるとか

**デフォルトの名無しさん** · 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の人で...

とか、まあ、そういったものの組み合わせが多いかな。
最悪、論理矛盾の自動検出が出来なくても、曖昧性の無い記述ができるなら
仕様漏れとかが減ったりしないかなぁ。

**デフォルトの名無しさん** · 2013/06/29(土) 13:32:51.16

>>80 >>81 >>82
> 業務ロジックを仕様記述言語で書くことは可能かな？
ていうか、そのためのものなんだがｗ
いまの仕様記述を見てたらそんなことも分かりにくいが

**デフォルトの名無しさん** · 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と形式手法は普通に両立すると思うが？

**デフォルトの名無しさん** · 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が優秀であることの証明にはならないし
他の技術を否定する正当性も与えない

**デフォルトの名無しさん** · 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のレスにおける核となる主張であり、疑問です。
が、その達観した無益なレスを書いて気持ち良いですか？

**デフォルトの名無しさん** · 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
「仕様が記述できたとしても、それに矛盾がないことを「検査」できない」
はおかしいだろう。

質問として実行すればいいのではないかな。定理証明の過程なのだから。

**デフォルトの名無しさん** · 2013/09/13(金) 20:47:12.33

では来週からPrologで仕様を書いてください。

**デフォルトの名無しさん** · 2013/09/13(金) 21:04:25.47

>>109
やはり形式手法という概念そのものが理解できていないようだね
仕様を実行して振る舞いを確認するのは「シミュレーション(模倣)」と呼ばれる手法であり、
「(形式手法における)検証」ではない

定理証明の過程において、対象となる仕様は「一切実行されない」ことを理解しなければならない
これを実現するために、形式手法では厳密な数学を基礎に置き、それを元に証明を進める

**デフォルトの名無しさん** · 2013/09/13(金) 21:16:04.80

>>111
なるほどね。わかった。
動的言語云々ということが書かれていたので検査が実行されるのだと
思ってしまった。

**112** · 2013/09/13(金) 21:22:31.21

まちがえた。
動的云々ではなく、「型付けの弱い言語云々」でした。

**デフォルトの名無しさん** · 2013/09/13(金) 22:19:56.75

でも形式手法をそういう言い方にするとAlloyやVDMの微妙さが際立ってしまうのだ

**デフォルトの名無しさん** · 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なり中間言語にさえ落とし込めさえすれば
あとは数学者やコンピュータサイエンティストの仕事だ

**デフォルトの名無しさん** · 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

このスレで興味もってざっとぐぐってるんですが、なかなか面白そうな分野ですね。
書籍やサイトのお勧めあったらご教示願えると幸いです

**デフォルトの名無しさん** · 2013/10/02(水) 09:58:39.78

>>100 >>133 >>137
この人センスいいねえ

>>111 >>136
この人は単なる学習者

**デフォルトの名無しさん** · 2013/10/03(木) 20:35:05.95

へー（ニヤニヤ
Zの言語仕様がデカいと思っている人のセンスがいいとか言うのって
本人以外考えられないけどw

**デフォルトの名無しさん** · 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

すじわる、って将棋以外で聞かない単語だよね。
まあ筋が悪いとは普通に使うんだから字面を見てわかると思うけど。

**112** · 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なんかがあるけど
二木先生の関わっていない利用例を知らない

**デフォルトの名無しさん** · 2013/10/04(金) 21:49:13.71

>>155
>言語仕様の大きさは
>処理系やツールを実装する人にとっては重要かもしれないけど
>ユーザにとっては重要じゃないよね。
誰にとっても同じだ。
同じことをするんなら小さい方がよいのに決まっとる

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

>>163
CafeOBJが新しいのか

**デフォルトの名無しさん** · 2013/10/04(金) 21:58:38.09

>>164
そんなに言語仕様が小さいのがいいのならBrainf*ckなんか最高だよね
チューリング完全だから「計算可能性の観点においては」
他の言語と同等のことができるよ

**デフォルトの名無しさん** · 2013/10/04(金) 22:06:34.37

観点は計算可能性だけじゃないだろ
まだチューリング完全なんて言ってるのか

**デフォルトの名無しさん** · 2013/10/04(金) 22:10:26.71

観点は言語仕様の大きさだけじゃないだろ
って話だよ
チューリング完全ならどれも一緒だなんて誰も思っちゃいねーよ

**デフォルトの名無しさん** · 2013/10/04(金) 22:30:01.22

だれかこの辺の議論のような口喧嘩のようなことを交通整理できる人はいないでしょうか

**デフォルトの名無しさん** · 2013/10/04(金) 23:00:21.87

そういった態度というのは単に自信が無いだけなので、
生暖かく放置すればいいのではないかと思われ

**デフォルトの名無しさん** · 2013/10/04(金) 23:07:34.51

ところで、Prologで仕様記述やその検証ができるなら試してみたいんだが、
その方法を解説した本やWebサイトとかあるのかな？
「理論的にはできるはず」だけだとProlog自体よく知らない俺には無理だが。

**デフォルトの名無しさん** · 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

**デフォルトの名無しさん** · 2013/10/05(土) 08:56:49.36

Alloyの本を読んでもちっとも頭に入っていきません。
この本を読むうえで必要な前提知識って何でしょうか？
また、その知識を得るのに最適な書籍があれば教えてください。

今は組込み関係の仕事（主に車関係）をしていて、知ってる言語はC言語のみです。

**デフォルトの名無しさん** · 2013/10/05(土) 10:07:18.70

知識はともかく
詳細仕様や実装仕様じゃなく
純粋なシステム仕様の読み書きをした経験がいるんじゃないかな

組込み関係だとシステム仕様と実装仕様がごっちゃになってる印象がある

実装仕様レベルの形式記述もできるけど
そういうのは実装言語（C言語）のツールを使った方がいいと思う

**デフォルトの名無しさん** · 2013/10/05(土) 18:08:45.67

>>174
その存在自体が無駄だと言っとるんだから、さらに何を言う必要がある？
Zや言語仕様の大きさなんていうくだらんことにどんだけ時間を浪費するんだ

**デフォルトの名無しさん** · 2013/10/05(土) 18:25:17.75

Zを否定した根拠が「言語仕様のデカさ」だったのに
今更なにを喚いているんだい、負け犬くんw

**デフォルトの名無しさん** · 2013/10/05(土) 18:35:37.68

「C言語以外は全部無駄」とたいして変わらん主張

**デフォルトの名無しさん** · 2013/10/05(土) 22:31:33.47

>>164は自分の主張が矛盾しているのに気付かない可哀想な子

>>160が言うように、Zは「述語論理と型付集合論」を知っていれば学習の壁は低い
つまり、もしも>>164の言葉「同じことをするんなら小さい方がよいのに決まっとる」が正しければ、
仕様の小さなZは優れていていることになるが、その一方でツールサポートの少ない「Zは要らん」と言う

では、ナゼそんな矛盾が生まれたのか？これは形式手法へ拒絶反応を起こす人によくあるパターンで、
形式手法を扱うのに前提となる素養(論理と集合)が欠けているからだろう
だから>>164にはZの仕様が(とほうもなく)巨大に見えて尻込みしてしまう
逆にAlloyはツールで実際に動かしながら試行錯誤できるから容易い存在に見える
実際にはAlloyの全容は巨大で難解なものだけど、>>164には表層の一部しか見えていない

おそらく、>>164はERM/OMT/UMLのような「仕様の視覚化手法(visualize method)」には
十分な経験と自信があるのだろう
ところが残念なことに、その延長で「仕様の形式化手法(formal method)」を
理解しようとして、その狭間(ギャップ)で「もがいている」のだと思われる

**デフォルトの名無しさん** · 2013/10/05(土) 22:44:35.57

>>175
述語論理ですかねー。あの変なシンタクスがオブジェクト指向と関係なくて、回りくどく表現された述語論理だと思うとたぶんわかってくる気がする。
あとAlloyだとたぶんその仕事にはあまり直接的に活かせないような。>>84-86に同じような話があるけど。

**デフォルトの名無しさん** · 2013/10/06(日) 06:14:26.21

>>180
そうだね、>>164みたいな人は10年か20年ぐらい前にもいたねえ。
「オブジェクト指向」でギャップに嵌ってる人達がね…（遠い目

UMLは図を「コトバ」として読む力が必要とされるんだけど、
形式手法では式を「コトバ」として読んじゃいけない。
式はあくまで記号列として読まないと「形式」の意味がわからない。
それができない人にはZは地獄のような言語かもしれない。

そういう人ほどZで徹底した形式主義を身につけたほうがいいと思うけど、
大抵は実行系中心の軽量形式手法で「これが形式手法かー」と思っちゃうんだよな…

**デフォルトの名無しさん** · 2013/10/06(日) 10:50:33.15

>>180 確かに、
Zは「述語論理と型付集合論」を知っていれば学習の壁は低いのだろうが、
そういう人材を一般企業では集められなかったからZは顧みられなかった
のではないか。

**デフォルトの名無しさん** · 2013/10/06(日) 11:30:50.49

述語論理も型付集合論も大学の教養レベルの数学で十分なのだから
「人材を集められなかった」のではないと思う。
単に、Zに限らず形式手法なしでもシステムを作れると思ってたんだろ。

だから、Zに限らずモデル規範型の形式手法は顧みられなかった。

**デフォルトの名無しさん** · 2013/10/06(日) 18:43:42.19

>>182
>形式手法では式を「コトバ」として読んじゃいけない。
>式はあくまで記号列として読まないと「形式」の意味がわからない。

ここは何を言ってるの？記号列として読んでいるのでは意味が分かっていない
と言われそうだけど。

**デフォルトの名無しさん** · 2013/10/06(日) 22:31:52.02

>>185
横レスだけど、形式手法の証明においては式に含まれる記号の意味は「無価値」だということ
記号の意味を分かる必要は無いし、
証明の過程で記号の意味は完全に無視され「形式(公理や定理)」だけが価値を持つ

ソフトウェア仕様記述は現実世界のモヤモヤした実体(=モノ)をある体系でモデル化することから始まる
たとえばUML等のOOA/OODでは現実世界をオブジェクトの集まりと捉え、オブジェクトの持つ属性や
オブジェクト間の(継承や部分といった)関係を定義することによって(非形式的な)モデル化を進める
ここでは実体をコトバとして抽象化する事を、具体的には定義するオブジェクト/属性/関係などの
命名(naming)を、つまり(人にとっての)直感的な意味を重要視する
これによって(人にとって)分かりやすく、特に共同作業下における仕様イメージの統一的な共有化を図る

これに対して、形式手法では現実世界をモデル化することは(視覚化手法と)同じだけれど、
数学という形式的な体系を用いる点が異なる
つまり、ある式(=モデル)が直感的には(=人にとっては)いかに分かりやすくて正しく見えようとも、
いいかえるといかにOO的視点では優れた設計であっても、形式に矛盾があれば誤りであると見なす

**デフォルトの名無しさん** · 2013/10/06(日) 22:55:41.08

>>186
こっちも横レスだけど
証明は形式意味論のレイヤーで行われるけれど
形式仕様自体は現実世界の概念（「コトバ」）とリンクしている

「コトバ」であり「記号列」であることを理解できないと
形式仕様を理解したことにはならんだろう

**デフォルトの名無しさん** · 2013/10/06(日) 22:57:20.47

>>186
>形式手法の証明においては式に含まれる記号の意味は「無価値」だということ
それは証明器にとって、ということでしょう。人間にとってではない。

>これに対して、形式手法では現実世界をモデル化することは(視覚化手法と)同じだけれど、
そのモデル化の時点で、「意味」が介在するよね。

>形式に矛盾があれば誤りであると見なす
それは当たり前。矛盾というのは形式的なものだからね。
だからといって「意味」が不要ということにはならない。

**デフォルトの名無しさん** · 2013/10/06(日) 23:01:03.54

「形式」手法 "form"-al method という言葉の意味からはじめないといけないようだな！

**デフォルトの名無しさん** · 2013/10/06(日) 23:11:16.30

>>189
およその意味はみんな分かってると思うが
その厳密な定義もない（あるいは厳密に定義する意味もない）ことも含めて
だがもし必要なら、そこからはじめてくれてもよいが

**デフォルトの名無しさん** · 2013/10/06(日) 23:15:39.39

みんな数学ガール／ゲーデルの不完全性定理
でも読んで和みたまえ（ステマ）

**デフォルトの名無しさん** · 2013/10/06(日) 23:30:11.15

>>187,188
現実世界を抽象化する過程に意味が伴うのはその通りで、視覚化手法も形式手法も同じ
形式手法にとっても抽象化の過程ではコトバの意味が大切なのに変わりはない

違うのは、抽象化の成果物である「仕様(設計書)の検証」において、視覚化手法では
(人間が介在する)直感を頼りとしており、そこではコトバの意味が重要な位置を占める
それに対して形式手法では仕様の検証に人の直感は介在せず、コトバの意味は無視する
ここで、証明(=形式を元にした検証)を人力でやろうが証明器で自動化しようが同じ

そして、もし証明が失敗すれば(仕様に矛盾を発見すれば)、現実世界の抽象化という前工程に立ち返る
その時には、(数学としての)形式化の単純ミスもあるだろうけど、コトバの意味(の定義)の過ち、
つまり(抽象化の過程で)現実世界の解釈に何か誤りや漏れがあったことが発見できるだろう

**デフォルトの名無しさん** · 2013/10/06(日) 23:45:46.18

>>188
>>形式に矛盾があれば誤りであると見なす
>それは当たり前。矛盾というのは形式的なものだからね。

いや、「非形式的な矛盾(=直感に基づく矛盾)」というのは存在する
たとえばOOの仕様で、ある箇所では「XはYのサブクラスである」と記述され、
別の箇所では「YはXのサブクラスである」と記述されていれば、それは矛盾だろう
ただし、サブクラスというオブジェクト間の関係は(人の)直感として定義されたものだから、
それは「形式的な矛盾」ではない

**デフォルトの名無しさん** · 2013/10/06(日) 23:49:56.14

この会話が成立していないのに
話が流れていく感じはすごいな

形式手法に言及しているのに
詭弁（誤謬）ばかりってのが皮肉

**デフォルトの名無しさん** · 2013/10/07(月) 06:12:47.77

>>193
>「非形式的な矛盾(=直感に基づく矛盾)」というのは存在する
形式的に意味不明な言明だ。
論理的訓練が不十分のようだから指摘しておく。
>別の箇所では「YはXのサブクラスである」と記述されていれば、それは矛盾だろう
矛盾とはAかつ￢Aが帰結することだ。「XはYのサブクラスである」と
「YはXのサブクラスである」はまだ矛盾ではない。
>ただし、サブクラスというオブジェクト間の関係は(人の)直感として定義されたものだから、
そういう関係もまた形式的に記述するんだよ。

>>194
>形式手法に言及しているのに
>詭弁（誤謬）ばかりってのが皮肉
意味不明。間違いがあれば指摘すればよい。
形式手法＝無謬ということではない。形式手法を偶像崇拝してる？

**デフォルトの名無しさん** · 2013/10/07(月) 08:17:29.48

>>192
概ね妥当なコメントと思うが
「視覚化手法」なんてものを形式手法と対比させるのはいかがなものか
それから、ここでは皆矛盾矛盾と言うが、矛盾がないというのは最低限の条件に過ぎない

**デフォルトの名無しさん** · 2013/10/07(月) 08:39:38.60

>>184
20年近く前に、私の周辺でZの研究会が次々と撃沈していったのを
知っている私としては、隔世の感ありだな。

**197** · 2013/10/07(月) 08:43:06.72

研究会 -> 勉強会

**デフォルトの名無しさん** · 2013/10/07(月) 09:12:11.96

>>197
撃沈の主な原因は何だったのですか？
そのころなら述語論理や集合論ではないと思うのですが

**デフォルトの名無しさん** · 2013/10/07(月) 09:27:05.81

計算機の性能だな
20年前のCPUの性能ではSAT SMTソルバーをぶん回すとかありえんだろう