【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

**デフォルトの名無しさん** · 2015/04/28(火) 23:15:25.31

久しぶりに来たが、超過疎ってるなｗ
形式仕様なんてどれもクソだって分かったかｗ

**デフォルトの名無しさん** · 2015/04/29(水) 02:03:55.33

クソではないよ
適用分野がとっくに収束してて適用分野も枯れてる
誰も語る事がなくなっただけだ

**デフォルトの名無しさん** · 2015/04/29(水) 06:15:54.81

質問もないから新しく始める人もいないってことだろうな。

**デフォルトの名無しさん** · 2015/04/29(水) 08:30:09.47

>>273　>>274
歯切れが悪くて何を言ってるか分からんが、
もうオワタ、でオーケー？何も残さんで

**デフォルトの名無しさん** · 2015/04/29(水) 11:04:46.37

形式仕様なんてどれもクソだが
クソ未満の非形式仕様が溢れかえっている喜劇

>>271
ミューテックスとセマフォの違いって排他制御の「実装」レベルの話なんじゃ
例えばデッドロックを回避する機構を入れたいなら
そういうコードを書かなきゃいけない
ミューテックスの一般的と言えるような実装がない以上
promelaでの一般的な記述もないような

余計なお世話かも知れんが
モデル検査は排他制御のあるシステムの検証には適しているといえるけど
それは排他制御を抽象化しての話
排他制御自体の検証には向いていないと思う

**デフォルトの名無しさん** · 2015/04/29(水) 12:43:37.44

>>276
結局ソフトウェアエンジニアリングがクソだと言ったか？ｗ
> それは排他制御を抽象化しての話
> 排他制御自体の検証には向いていないと思う
これは何言ってる？

**デフォルトの名無しさん** · 2015/04/29(水) 13:07:57.19

>>271の問題はまさにそこのところ、モデルと実際のプログラムをどう対応付けるかなんだろう。
VDMが実際の開発に導入されている話は聞くがAlloyについてはあまり聞かないのは
やはり抽象度のギャップの要因が大きいように思う。

**デフォルトの名無しさん** · 2015/04/29(水) 21:37:39.89

>>278
抽象度のギャップは大きいほどいいじゃないか

**デフォルトの名無しさん** · 2015/04/30(木) 06:12:35.13

なんで大きいほどいいの？
ギャップ=0で、動くプログラムがそのまま検査できるのが理想じゃないのか。

**デフォルトの名無しさん** · 2015/04/30(木) 07:36:41.80

>>280
ん？言葉の違いか？
ギャップってモデルと実際のプログラムの間の抽象度の違いのことじゃないのか？

**デフォルトの名無しさん** · 2015/04/30(木) 07:58:46.50

うん、その違いだよ。
抽象度の高いモデルで正しさを証明できたとして、それをもって現実のプログラムの
正しさの証明とするにはギャップは小さいほうがいいと思うが。
書き換えの段階で間違いが入ったらそもそも意味がないし。
ギャップが大きいほどいいとする理由は？

**デフォルトの名無しさん** · 2015/04/30(木) 08:47:12.46

えー！　
極端な場合で考えてみなよ
ギャップ＝０ということはモデルの意味がないということだ

**デフォルトの名無しさん** · 2015/04/30(木) 09:07:52.87

モデルの意味って何ぞ？
>>278の言う現実のプロジェクトではモデルを構築することそれ自体が目的じゃなくて
実際のシステムに誤りがないことを保証したいわけだろう。
モデルはそのための道具でしかない。

**デフォルトの名無しさん** · 2015/04/30(木) 10:01:13.28

モデルがなぜそのための道具になりえるとしたら、それはモデルが何だからか考えてみな

**デフォルトの名無しさん** · 2015/04/30(木) 10:02:47.56

モデルがそのための道具になりえるとしたら、それはモデルが何だからかを考えてみな

**デフォルトの名無しさん** · 2015/04/30(木) 21:17:47.07

ここでそういう質問が出るとは思わなかったが、形式手法におけるモデルの意義は
機械的に検証可能であることに尽きるだろう。現実のプログラムではそれが難しいから
モデルで代用していると言ってもいい。

たぶんあんたが考える「モデルの意味」は違うんだろうけど、じゃあそれ説明して。

**デフォルトの名無しさん** · 2015/05/01(金) 20:46:23.78

まぁ色々な側面があると思うけどね

形式手法によって手戻りを低減するには
できるだけ早期に検証することが有効で
建前としては仕様が実装に先行するのだから
検証の対象は実装より抽象度が高くなる

とはいえギャップが大きすぎるのも実際的ではない
だからBやZで言われる段階的詳細化が意味を成す

**デフォルトの名無しさん** · 2015/05/01(金) 21:06:27.82

別の大きな側面としては
抽象化しないと現在の計算機・理論ではまともに検証できない
というのがある

簡単に言えば状態変数として二値変数が64個あるだけで
状態空間を表現するのにアドレス空間を食いつぶしてしまう

自然数や実数を扱うプログラムをまともに自動検証できるようにするには
ハードにせよ計算理論にせよ技術革新が必要

**デフォルトの名無しさん** · 2015/05/01(金) 21:07:15.76

勿論「矛盾がない」という検証結果が
実際的な時間・コストで得られないとしても
「矛盾がある」という結果が早期に得られる場合もあるので
計算機ぶん回すのも無意味ではないが
それはいわゆる形式手法というより「テスト」の範疇だと思う

**デフォルトの名無しさん** · 2015/05/01(金) 23:33:52.21

>建前としては仕様が実装に先行するのだから
>検証の対象は実装より抽象度が高くなる

>抽象化しないと現在の計算機・理論ではまともに検証できない

積極的に抽象化すべき理由じゃなくて単なる結果だな。

**デフォルトの名無しさん** · 2015/05/02(土) 00:16:55.31

自然言語の曖昧さの排除という使命がある以上
闇雲に抽象化すればいいってもんでもないだろ

さらに言うなら「単なる結果」でない
形式手法を使う積極的理由なんてあるのか？

**デフォルトの名無しさん** · 2015/05/02(土) 09:28:39.94

皆独り言を言っている。

**デフォルトの名無しさん** · 2015/05/02(土) 20:56:44.49

どいつもこいつもｗこの分野のやつらはｗ
そんなのを抽象化なんて言うから世間から笑われるんだ
単なるアバウトって言うんだよ

**デフォルトの名無しさん** · 2015/05/09(土) 05:15:44.76

>>294
アバウトなのは、抽象に関するあんたの理解。

**デフォルトの名無しさん** · 2015/08/10(月) 08:36:36.39

質問に罵倒なんぞは自然言語でいいが、主張は形式手法言語で書いてくれ。
Event-Bしか読めないけど。

**デフォルトの名無しさん** · 2015/08/10(月) 23:38:42.28

形式言語で表現できるのは形式的意味でしかなく
主張するところの、いわゆる意味を示すことはできない

そして論理的に矛盾の無い主張だからといって有意義とは限らない
ここで「偶数+奇数は奇数だ！」と主張したところで
スレチとなるだけ

ま、自然言語から意味を見出しているのも幻想かもしらんが

**デフォルトの名無しさん** · 2015/12/30(水) 12:08:29.72

Alloyって楽しいな。
コンピュータと対話しながら、記述対象に対する自分の理解を深められるのがとても楽しい。

**デフォルトの名無しさん** · 2016/03/03(木) 22:41:34.71

test

**デフォルトの名無しさん** · 2018/05/23(水) 23:09:57.69

僕の知り合いの知り合いができたパソコン一台でお金持ちになれるやり方
役に立つかもしれません
グーグルで検索するといいかも『ネットで稼ぐ方法　モニアレフヌノ』

ZLPAL

**デフォルトの名無しさん** · 2018/07/04(水) 22:59:43.98

LGL

**デフォルトの名無しさん** · 2018/07/06(金) 12:34:31.11

ZLPAL