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

1デフォルトの名無しさん2013/01/05(土) 21:09:06.67

250デフォルトの名無しさん2013/10/16(水) 02:16:17.00
>>248
そういう話も包含されているだろうね

仕様を書く人は誤解を生まないように気を付けた方が良いし
仕様を読む人は思い込みをしないように気を付けた方が良い

そんな凡庸な結論では刺激が足りない人が
極論で言葉遊びしているのがこのスレ

>>249
もっと具体的に言ってくれないと同意も否定もできん

251デフォルトの名無しさん2013/10/16(水) 03:00:35.01
式に含まれる記号の意味は証明(記号の操作)に無関係である

しかし人間は様々な形式化されていない知識を持っている
それは当該の公理系においては誤ったあるいは誤っているかどうか判断出来ない
推論規則をもたらす知れないが無価値とは言えない

どのくらいの価値があるかは適用場面や人の価値観によるだろう

252デフォルトの名無しさん2013/10/16(水) 09:03:40.50
>>209
>じゃあポインタをキャストしまくってるCのソースも形式仕様だねw
ということになるね。なぜダメ? あなたの定義は?

253デフォルトの名無しさん2013/10/16(水) 09:18:21.22
Cは未定義動作や実装依存があるから
形式的意味論が定義されているとは
言えないんじゃないかなー

254デフォルトの名無しさん2013/10/16(水) 09:19:58.66
機械可読なら形式仕様って
それじゃエクセル方眼紙も形式仕様かよw

255デフォルトの名無しさん2013/10/16(水) 09:21:06.47
>>246
>形式手法とはシステム記述に形式主義を導入して
>形式主義的な検証や開発をおこなうこと
>を指すと思うのだが...
ちょっと違う。「主義」をはずせばよい。

>>248
>そういう話なのか?
>hoge = 2.0 * pi * r
>という形式的定義があった時に
>円周率や半径の類推から
>piやrの形式的定義を辿らずに
>hogeを円周の長さだと思い込んではいけない
>という話なんじゃないのか?
いや、そもそもhogeやrを円周や半径と思ってはいけないと言ってるんだろ?
それに、いくら形式的定義を辿ってもhogeが円周だとはわからないよ

>>249
>形式主義を真っ向から否定しているようだが?
形式主義を否定してるんじゃなくて、形式手法=形式主義ではないと言ってる

>>250
>仕様を書く人は誤解を生まないように気を付けた方が良いし
>仕様を読む人は思い込みをしないように気を付けた方が良い
随分ぬるいがwまあそういうことだ。記号病達にはこれも伝わらないのじゃないかな

256デフォルトの名無しさん2013/10/16(水) 09:28:13.23
>>255
> 「主義」をはずせばよい。
formal methodsからformalismを取ったら何が残るの?ばかなの?

> それに、いくら形式的定義を辿ってもhogeが円周だとはわからないよ
hogeを円周と読むなって話だということが理解できない?ばかなの?

257デフォルトの名無しさん2013/10/16(水) 09:35:15.08
>>255
既に誰かが指摘しているようだが
あなたが形式手法と呼んでいるものは
制限文法による仕様記述なのでは?

258デフォルトの名無しさん2013/10/16(水) 09:47:51.55
>>256
>formal methodsからformalismを取ったら何が残るの?
アスペを相手にしたくないので、短く言うが、数学と記号表記の関係と同じ。
>hogeを円周と読むなって話
だから、>>255で、君達はそう言ってるんだろ、と言っただろ。よく読め

259デフォルトの名無しさん2013/10/16(水) 09:55:30.15
>>253
>Cは未定義動作や実装依存があるから
それは細かいことではないか。それに、未定義の所は使わければよいし、実装依存ならその実装に従えばよいし

>>254
>それじゃエクセル方眼紙も形式仕様かよw
方眼紙だけだと何もない形式仕様ということになるね

260デフォルトの名無しさん2013/10/16(水) 10:01:36.85
>>257
なんの限定もついていない形式手法について話してるつもりだが?
しかも言ってることは、「記号操作が本質なのじゃないよ」ということだけ

261デフォルトの名無しさん2013/10/16(水) 10:07:55.75
>>256

>hogeを円周と読むなって話

そんならそもそもお前は何を書いているんだという話

262デフォルトの名無しさん2013/10/16(水) 11:28:01.88
>>260
"制限文法" "仕様記述"
でggrks

263デフォルトの名無しさん2013/10/16(水) 11:28:49.24
>>259
それを「細かいこと」なんて言う人が
形式手法に何の用があるんだい?あほ?

264デフォルトの名無しさん2013/10/16(水) 19:10:23.13
>>263
アスペの上に、言葉づかいの癖から見てクズのようだからもう相手しないが
>それを「細かいこと」なんて言う人が
それが細かくない(本質的である)と思っているということは、君は未定義動作や実装依存をなくせばCのソースも形式仕様だと言うんだな
それから、形式的ということと細かいということは同じことではないんだよ

265デフォルトの名無しさん2013/10/16(水) 20:28:23.99
>>264のロジックが崩壊している件ww

266デフォルトの名無しさん2013/10/16(水) 21:27:26.11
まずJavascriptで書きます。
次に実行します。
ここでエラーが出たら間違いがあるということです。
正しく実行できたら正しく実行できるということです。

267デフォルトの名無しさん2013/10/16(水) 23:00:58.62
なんというトートロジー

エラーが出なくても正しいとは限らないのは>>212で言われているとおり

268デフォルトの名無しさん2013/10/17(木) 13:29:16.40
>>264
>それが細かくない(本質的である)と思っているということは、

この前提から

> 君は未定義動作や実装依存をなくせばCのソースも形式仕様だと言うんだな

こんな帰結を導出する人には、形式手法は無理です。(きっぱり

269デフォルトの名無しさん2013/12/19(木) 10:09:23.66
Alloyの本を読んで容易に理解できるには、前提知識として何が必要ですか?
このブログ
http://d.hatena.ne.jp/rabbit2go/20110802/1312252092
でも初心者だが容易に理解できたとあるが、私は読んでもさっぱりわかりません。。。

270デフォルトの名無しさん2014/04/04(金) 18:04:17.82ID:cQ9GUWm/
佐原伸 @donkeyshin: ちゅうか、機関銃買ってレイシスト撃ち こrしたくなるので米国ボイコット^_^
RT @tomooda: まあそうなんだけど、USAもユートピアとはほど遠い。全体主義も吹き荒れるし,雇用だって安定しないくせに階層間の流動性は日本以上に低い。レガシーとしか言いようがない古く非合理的な。

271デフォルトの名無しさん2015/04/24(金) 23:38:42.03ID:belF3Fjq
SPINを勉強し始めたところなんだけど、ミューテックス/セマフォ/モニタって
promelaでどう記述するのが一般的なんだろう?
セマフォはBasic Spin Manualにあったけど、どこかにまとまった情報がないかな。

272デフォルトの名無しさん2015/04/28(火) 23:15:25.31ID:8LxH1Yrp
久しぶりに来たが、超過疎ってるなw
形式仕様なんてどれもクソだって分かったかw

273デフォルトの名無しさん2015/04/29(水) 02:03:55.33ID:kKwn8j7I
クソではないよ
適用分野がとっくに収束してて適用分野も枯れてる
誰も語る事がなくなっただけだ

274デフォルトの名無しさん2015/04/29(水) 06:15:54.81ID:f54jgqM7
質問もないから新しく始める人もいないってことだろうな。

275デフォルトの名無しさん2015/04/29(水) 08:30:09.47ID:JCD1NrNA
>>273 >>274
歯切れが悪くて何を言ってるか分からんが、
もうオワタ、でオーケー?何も残さんで

276デフォルトの名無しさん2015/04/29(水) 11:04:46.37ID:mWtY0FPp
形式仕様なんてどれもクソだが
クソ未満の非形式仕様が溢れかえっている喜劇

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

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

277デフォルトの名無しさん2015/04/29(水) 12:43:37.44ID:JCD1NrNA
>>276
結局ソフトウェアエンジニアリングがクソだと言ったか?w
> それは排他制御を抽象化しての話
> 排他制御自体の検証には向いていないと思う
これは何言ってる?

278デフォルトの名無しさん2015/04/29(水) 13:07:57.19ID:f54jgqM7
>>271の問題はまさにそこのところ、モデルと実際のプログラムをどう対応付けるかなんだろう。
VDMが実際の開発に導入されている話は聞くがAlloyについてはあまり聞かないのは
やはり抽象度のギャップの要因が大きいように思う。

279デフォルトの名無しさん2015/04/29(水) 21:37:39.89ID:JCD1NrNA
>>278
抽象度のギャップは大きいほどいいじゃないか

280デフォルトの名無しさん2015/04/30(木) 06:12:35.13ID:B1QV8IC2
なんで大きいほどいいの?
ギャップ=0で、動くプログラムがそのまま検査できるのが理想じゃないのか。

281デフォルトの名無しさん2015/04/30(木) 07:36:41.80ID:YRFCj/Kr
>>280
ん?言葉の違いか?
ギャップってモデルと実際のプログラムの間の抽象度の違いのことじゃないのか?

282デフォルトの名無しさん2015/04/30(木) 07:58:46.50ID:B1QV8IC2
うん、その違いだよ。
抽象度の高いモデルで正しさを証明できたとして、それをもって現実のプログラムの
正しさの証明とするにはギャップは小さいほうがいいと思うが。
書き換えの段階で間違いが入ったらそもそも意味がないし。
ギャップが大きいほどいいとする理由は?

283デフォルトの名無しさん2015/04/30(木) 08:47:12.46ID:YRFCj/Kr
えー! 
極端な場合で考えてみなよ
ギャップ=0ということはモデルの意味がないということだ

284デフォルトの名無しさん2015/04/30(木) 09:07:52.87ID:B1QV8IC2
モデルの意味って何ぞ?
>>278の言う現実のプロジェクトではモデルを構築することそれ自体が目的じゃなくて
実際のシステムに誤りがないことを保証したいわけだろう。
モデルはそのための道具でしかない。

285デフォルトの名無しさん2015/04/30(木) 10:01:13.28ID:YRFCj/Kr
モデルがなぜそのための道具になりえるとしたら、それはモデルが何だからか考えてみな

286デフォルトの名無しさん2015/04/30(木) 10:02:47.56ID:YRFCj/Kr
モデルがそのための道具になりえるとしたら、それはモデルが何だからかを考えてみな

287デフォルトの名無しさん2015/04/30(木) 21:17:47.07ID:B1QV8IC2
ここでそういう質問が出るとは思わなかったが、形式手法におけるモデルの意義は
機械的に検証可能であることに尽きるだろう。現実のプログラムではそれが難しいから
モデルで代用していると言ってもいい。

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

288デフォルトの名無しさん2015/05/01(金) 20:46:23.78ID:mxjbyy1D
まぁ色々な側面があると思うけどね

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

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

289デフォルトの名無しさん2015/05/01(金) 21:06:27.82ID:mxjbyy1D
別の大きな側面としては
抽象化しないと現在の計算機・理論ではまともに検証できない
というのがある

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

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

290デフォルトの名無しさん2015/05/01(金) 21:07:15.76ID:mxjbyy1D
勿論「矛盾がない」という検証結果が
実際的な時間・コストで得られないとしても
「矛盾がある」という結果が早期に得られる場合もあるので
計算機ぶん回すのも無意味ではないが
それはいわゆる形式手法というより「テスト」の範疇だと思う

291デフォルトの名無しさん2015/05/01(金) 23:33:52.21ID:QsO/fHrg
>建前としては仕様が実装に先行するのだから
>検証の対象は実装より抽象度が高くなる

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

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

292デフォルトの名無しさん2015/05/02(土) 00:16:55.31ID:XhAWgoUD
自然言語の曖昧さの排除という使命がある以上
闇雲に抽象化すればいいってもんでもないだろ

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

293デフォルトの名無しさん2015/05/02(土) 09:28:39.94ID:GIpzT+Qy
皆独り言を言っている。

294デフォルトの名無しさん2015/05/02(土) 20:56:44.49ID:0dQA+dZy
どいつもこいつもwこの分野のやつらはw
そんなのを抽象化なんて言うから世間から笑われるんだ
単なるアバウトって言うんだよ

295デフォルトの名無しさん2015/05/09(土) 05:15:44.76ID:gLXIswIQ
>>294
アバウトなのは、抽象に関するあんたの理解。

296デフォルトの名無しさん2015/08/10(月) 08:36:36.39ID:R/t8P2/U
質問に罵倒なんぞは自然言語でいいが、主張は形式手法言語で書いてくれ。
Event-Bしか読めないけど。

297デフォルトの名無しさん2015/08/10(月) 23:38:42.28ID:8/xPnylN
形式言語で表現できるのは形式的意味でしかなく
主張するところの、いわゆる意味を示すことはできない

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

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

298デフォルトの名無しさん2015/12/30(水) 12:08:29.72ID:z2Nurwun
Alloyって楽しいな。
コンピュータと対話しながら、記述対象に対する自分の理解を深められるのがとても楽しい。

299デフォルトの名無しさん2016/03/03(木) 22:41:34.71ID:tH72Ij/h
test

300デフォルトの名無しさん2018/05/23(水) 23:09:57.69ID:Au5e7VGg
僕の知り合いの知り合いができたパソコン一台でお金持ちになれるやり方
役に立つかもしれません
グーグルで検索するといいかも『ネットで稼ぐ方法 モニアレフヌノ』

ZLPAL

新着レスの表示
レスを投稿する