15/04/30 07:58:46.50 B1QV8IC2.net
うん、その違いだよ。
抽象度の高いモデルで正しさを証明できたとして、それをもって現実のプログラムの
正しさの証明とするにはギャップは小さいほうがいいと思うが。
書き換えの段階で間違いが入ったらそもそも意味がないし。
ギャップが大きいほどいいとする理由は？
282:デフォルトの名無しさん
15/04/30 08:47:12.46 YRFCj/Kr.net
えー！
極端な場合で考えてみなよ
ギャップ＝０ということはモデルの意味がないということだ
283:デフォルトの名無しさん
15/04/30 09:07:52.87 B1QV8IC2.net
モデルの意味って何ぞ？
>>277の言う現実のプロジェクトではモデルを構築することそれ自体が目的じゃなくて
実際のシステムに誤りがないことを保証したいわけだろう。
モデルはそのための道具でしかない。
284:デフォルトの名無しさん
15/04/30 10:01:13.28 YRFCj/Kr.net
モデルがなぜそのための道具になりえるとしたら、それはモデルが何だからか考えてみな
285:デフォルトの名無しさん
15/04/30 10:02:47.56 YRFCj/Kr.net
モデルがそのための道具になりえるとしたら、それはモデルが何だからかを考えてみな
286:デフォルトの名無しさん
15/04/30 21:17:47.07 B1QV8IC2.net
ここでそういう質問が出るとは思わなかったが、形式手法におけるモデルの意義は
機械的に検証可能であることに尽きるだろう。現実のプログラムではそれが難しいから
モデルで代用していると言ってもいい。
たぶんあんたが考える「モデルの意味」は違うんだろうけど、じゃあそれ説明して。
287:デフォルトの名無しさん
15/05/01 20:46:23.78 mxjbyy1D.net
まぁ色々な側面があると思うけどね
形式手法によって手戻りを低減するには
できるだけ早期に検証することが有効で
建前としては仕様が実装に先行するのだから
検証の対象は実装より抽象度が高くなる
とはいえギャップが大きすぎるのも実際的ではない
だからBやZで言われる段階的詳細化が意味を成す
288:デフォルトの名無しさん
15/05/01 21:06:27.82 mxjbyy1D.net
別の大きな側面としては
抽象化しないと現在の計算機・理論ではまともに検証できない
というのがある
簡単に言えば状態変数として二値変数が64個あるだけで
状態空間を表現するのにアドレス空間を食いつぶしてしまう
自然数や実数を扱うプログラムをまともに自動検証できるようにするには
ハードにせよ計算理論にせよ技術革新が必要
289:デフォルトの名無しさん
15/05/01 21:07:15.76 mxjbyy1D.net
勿論「矛盾がない」という検証結果が
実際的な時間・コストで得られないとしても
「矛盾がある」という結果が早期に得られる場合もあるので
計算機ぶん回すのも無意味ではないが
それはいわゆる形式手法というより「テスト」の範疇だと思う
290:デフォルトの名無しさん
15/05/01 23:33:52.21 QsO/fHrg.net
>建前としては仕様が実装に先行するのだから
>検証の対象は実装より抽象度が高くなる
>抽象化しないと現在の計算機・理論ではまともに検証できない
積極的に抽象化すべき理由じゃなくて単なる結果だな。
291:デフォルトの名無しさん
15/05/02 00:16:55.31 XhAWgoUD.net
自然言語の曖昧さの排除という使命がある以上
闇雲に抽象化すればいいってもんでもないだろ
さらに言うなら「単なる結果」でない
形式手法を使う積極的理由なんてあるのか？
292:デフォルトの名無しさん
15/05/02 09:28:39.94 GIpzT+Qy.net
皆独り言を言っている。
293:デフォルトの名無しさん
15/05/02 20:56:44.49 0dQA+dZy.net
どいつもこいつもｗこの分野のやつらはｗ
そんなのを抽象化なんて言うから世間から笑われるんだ
単なるアバウトって言うんだよ
294:デフォルトの名無しさん
15/05/09 05:15:44.76 gLXIswIQ.net
>>293
アバウトなのは、抽象に関するあんたの理解。
295:デフォルトの名無しさん
15/08/10 08:36:36.39 R/t8P2/U.net
質問に罵倒なんぞは自然言語でいいが、主張は形式手法言語で書いてくれ。
Event-Bしか読めないけど。
296:デフォルトの名無しさん
15/08/10 23:38:42.28 8/xPnylN.net
形式言語で表現できるのは形式的意味でしかなく
主張するところの、いわゆる意味を示すことはできない
そして論理的に矛盾の無い主張だからといって有意義とは限らない
ここで「偶数+奇数は奇数だ！」と主張したところで
スレチとなるだけ
ま、自然言語から意味を見出しているのも幻想かもしらんが
297:デフォルトの名無しさん
15/12/30 12:08:29.72 z2Nurwun.net
Alloyって楽しいな。
コンピュータと対話しながら、記述対象に対する自分の理解を深められるのがとても楽しい。
298:デフォルトの名無しさん
16/03/03 22:41:34.71 tH72Ij/h.net
test
299:デフォルトの名無しさん
18/05/23 23:09:57.69 Au5e7VGg.net
僕の知り合いの知り合いができたパソコン一台でお金持ちになれるやり方
役に立つかもしれません
グーグルで検索するといいかも『ネットで稼ぐ方法 モニアレフヌノ』
ZLPAL
300:デフォルトの名無しさん
18/07/04 22:59:43.98 gFgZc5FG.net
LGL
301:デフォルトの名無しさん
18/07/06 12:34:31.11 uTPDH9XV.net
ZLPAL