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

1 名前：デフォルトの名無しさん mailto:sage [2013/01/05(土) 21:09:06.67 .net] スレがないので立ててみた 参考ページ en.wikipedia.org/wiki/Formal_methods ja.wikipedia.org/wiki/%E5%BD%A2%E5%BC%8F%E6%89%8B%E6%B3%95 2 名前：デフォルトの名無しさん mailto:sage [2013/01/05(土) 21:33:15.76 .net] このスレッドは天才チンパンジー「アイちゃん」が 言語訓練のために立てたものです。 アイと研究員とのやり取りに利用するスレッドなので、 関係者以外は書きこまないで下さい。 　　　　　　　　　　　　　　　　　　京都大学霊長類研究所 3 名前：デフォルトの名無しさん mailto:sage [2013/01/06(日) 01:05:45.32 .net] >>1乙 VDMはともかくAlloyってこの分野で流行ってるの？ 4 名前：デフォルトの名無しさん mailto:sage [2013/01/06(日) 01:16:08.51 .net] ついでだからIPAの報告書 （個人的には形式手法を良とするバイアスがかかっているように思うが） 「形式手法適用調査」報告書 sec.ipa.go.jp/reports/20100729.html 「情報系の実稼働システムを対象とした形式手法適用実験報告書」 sec.ipa.go.jp/reports/20120420.html 形式手法導入課題を解決する「形式手法活用ガイドならびに参考資料」 sec.ipa.go.jp/reports/20120928.html 実務家のための形式手法 教材「厳密な仕様記述を志すための形式手法入門」 sec.ipa.go.jp/reports/20121113.html 5 名前：デフォルトの名無しさん mailto:sage [2013/01/06(日) 01:23:51.63 .net] 第3回形式手法の産業応用ワークショップ（予稿・スライド） cfv.jp/cvs/event/workshop/2012/09/ 第2回・第1回へのリンク有 6 名前：デフォルトの名無しさん mailto:sage [2013/01/08(火) 01:54:13.02 .net] 特許庁の新システム入札やり直すらしいけど ああいうのこそ形式手法を適用する意義がありそうなものだが 形式手法によってデスマが回避できるというよりは デスマを回避できる体力があるから形式手法を採用できるってのが 実際なのかもしらん 7 名前：デフォルトの名無しさん mailto:sage [2013/01/08(火) 06:49:04.96 .net] Alloyの本 抽象によるソフトウェア設計−Alloyではじめる形式手法− www.amazon.co.jp/dp/4274068587 形式手法の本 形式手法入門―ロジックによるソフトウェア設計― www.amazon.co.jp/dp/4274211886/ 8 名前：デフォルトの名無しさん mailto:sage [2013/01/11(金) 06:24:10.24 .net] >Alloy あー、あの赤いやつね 途中であきらめました 9 名前：デフォルトの名無しさん mailto:sage [2013/01/11(金) 06:27:52.78 .net] どこで諦めたの? 自分は結構楽しめた。 10 名前：デフォルトの名無しさん mailto:sage [2013/01/11(金) 22:54:26.79 .net] あきらめたというかフェードアウトした感じかな たしか半分くらいまでは読んだけど、いつの間にか 読むのをやめてた 形式手法はまったくの素人だったので（今も） よく分からんかった 11 名前：デフォルトの名無しさん [2013/01/17(木) 10:49:33.93 .net] >>4 >>5 >IPAの報告書　>第3回形式手法の産業応用ワークショップ 見たけど相変わらずだな。使い物にならんよあんなのじゃ。 人材いないんだなこの方面。 12 名前：デフォルトの名無しさん mailto:sage [2013/01/18(金) 03:26:26.90 .net] 国内だと人材が少ない（しかも学術寄りの人の方が多い） ってのは実感としてある 形式手法は静的解析のツールとして利用される道の方が明るい気がする 人間が読み書きする形式言語が使い物になる日は来ないと思う 13 名前：デフォルトの名無しさん [2013/01/18(金) 17:38:42.62 .net] >>12 うん。学術系はだめだ。 実務に近いSRAがやや骨があるようだが。 >人間が読み書きする形式言語 これはどう言う意味かわからんが >使い物になる日は来ないと思う そんなことはない。一流人材が参戦すれば変わる。 14 名前：デフォルトの名無しさん mailto:sage [2013/01/18(金) 19:43:02.15 .net] 仕様記述に10日かけて、 プログラムを自動生成して3日で納品できるようになるとすると ビジネスのありかたとしては 仕様記述で工数を計上して費用請求することになって 今までの設計と大差ないことになるのジャマイカ 15 名前：デフォルトの名無しさん [2013/01/19(土) 00:19:45.43 .net] >>14 なにが大差ないと言っているのかよくわからん。 16 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 01:08:35.95 .net] 費用や納期だけで評価したら大差ないってことでしょ 現状ソフトウェアの品質を正当に評価していない（できない）から 形式手法を導入するインセンティブが働かない てかageる必要あんのか？ 17 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 01:18:12.83 .net] >>15 とある情報システムを開発するのにかかるコスト とか 予算や開発期間がオーバーするリスク とか 18 名前：デフォルトの名無しさん [2013/01/19(土) 12:16:55.38 .net] >>11 >>14 >>17 確かに今までの形式手法ではそうだ。 論文を書きたいだけの奴にはそれでいいんだろ。 >>16 品質は費用納期に反映されるので、それは形式手法側の言い訳だ。 19 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 13:05:09.39 .net] >>18 論文と現場の乖離を示唆しながら >品質は費用納期に反映される はねぇだろ 営業や契約担当じゃないから実態は知らないが 発注元は 「フィールドバグ○件以下。超過した場合は違約金！」 とか契約文書に書けるの？ 逆に請負側（候補）は 形式手法の適用が要件に入っていない案件で 「我が社は形式手法を導入しているのでちょっといいお値段です！」 で競争に勝てるというの？ 「我が社で納期が短縮できるのは形式手法で開発の手戻りを低減するからです！ 品質下げる訳じゃありません！」 とか発注元に説明すんの？ 20 名前：デフォルトの名無しさん [2013/01/19(土) 13:53:26.32 .net] >>19 >「フィールドバグ○件以下。超過した場合は違約金！」 >とか契約文書に書けるの？ そりゃ書ける場合もあるよ。 それに、バグが多いと、当然後の注文もなくなってくるだろ。 >「我が社は形式手法を導入しているのでちょっといいお値段です！」 それは、顧客にとってのメリットを言っていないので、その時点でダメだよ。 >「我が社で納期が短縮できるのは形式手法で開発の手戻りを低減するからです>！品質下げる訳じゃありません！」とか発注元に説明すんの？ 黙って短い納期でやればいいだけだろ。それは顧客にとってメリットだし、 こっちも短くなった分、他の仕事ができるし。 ほんとに使える形式手法とはこういうものなんだよ。 21 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 14:57:17.31 .net] 話が通じていないな ・ソフトウェアの品質を規定する統一的な指標がない ・既存の品質指標は開発手法に依存することが多い 　（形式手法を適用した場合としない場合の公平な比較が困難） ・形式手法を要件に入れると対応できる業者が制限される このため形式手法を導入するメリットが明確な「発注」がそもそも少ない （メリットが明確なセーフティクリティカルやミッションクリティカルな案件では 現状でも形式手法が成果を上げている） 潜在的需要があっても表面上需要が無ければ 請負側に働く形式手法導入のインセンティブは弱い 22 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 15:15:19.07 .net] 請負側としては 同じ業者から大きな案件を頻繁に受注するケースは少ない 評判に期待して今回頑張っても次回の受注がいつなのかは分からない いつ効果が表れるか不明確な投資はやりにくい 業界全体で評判になるほどの成果を上げるのは体力に余裕がないとできない しかも形式手法が扱える業者は多くないが 形式手法だけで需要を独占できるほどの特殊性はない 23 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 15:23:25.33 .net] 請負側開発者・マネージャとしては 形式手法によりコストや納期を圧縮できるかもしれないが 勉強やらに費やした分だけ自分の給与が上がる保証はない 訳のわからない仕様書から解放されるといった 現場の幸せを要求しても経営判断には反映されにくい 24 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 15:44:33.85 .net] 高階関数とかのようなメタプログラミング機構がなくて言語としては貧弱なのも欠点 25 名前：デフォルトの名無しさん [2013/01/19(土) 16:08:35.77 .net] まあ今の形式手法の状況認識はそれでいいんじゃないか >セーフティクリティカルやミッションクリティカルな案件では 現場にとってはそういうニッチなところで使うもので、 平凡な研究者にとっては、やればできると分かっている事をやれば少しは 論文が書けるというそんなものなんじゃないか？ それじゃつまらんけどね 26 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 19:06:51.37 .net] 新参で申し訳ないんだけど 形式言語で書いた仕様書は発注側が用意するの？ 受注側が用意するの？ 27 名前：デフォルトの名無しさん mailto:sage [2013/01/19(土) 19:55:52.90 .net] 形式手法は商習慣まで関知せんよ 発注側「こういうもの作って」→受注側「言われたものを作りました」 という関係がものづくりとしては自然に思えるが 日本のICT業界は往々にしてこうはなっていない 上流で形式仕様を作成する場合 ユーザ企業はまずコンサル会社や大手ベンダに 「形式仕様作成と検証」といった発注を出すんじゃないかな 特に日本の場合は要求分析もセットになるかもしれない 28 名前：デフォルトの名無しさん [2013/01/19(土) 20:55:25.43 .net] C++の新規格のドラフトにaxiomsっていうのがあったんだけど 結局却下されちゃったんだよな 29 名前：デフォルトの名無しさん [2013/01/20(日) 18:35:51.46 .net] >>25 そっち方面の学界が腐敗とまでは言わんが競争がなく濁ってるんじゃないか？ だから一流人材が出て来ない。 30 名前：デフォルトの名無しさん mailto:sage [2013/01/20(日) 23:53:12.74 .net] >>29 ム板でいうのも何だけど おまえ何様だよ 31 名前：デフォルトの名無しさん mailto:sage [2013/01/22(火) 23:33:47.71 .net] シンタックスはともかくセマンティクスにおいて VDM++のまともな仕様って無いの？ 曖昧さを持った言語で形式仕様記述とか欺瞞じゃね？ VDM-10のVDM++のが 枠組みはしっかりしてるけど事実上使えないし Overture界隈はVDM-RTに傾倒してる感じだし 何かみんなおでこ広いし 32 名前：デフォルトの名無しさん mailto:sage [2013/01/26(土) 00:09:26.58 .net] >>13 > >人間が読み書きする形式言語 > >使い物になる日は来ないと思う > そんなことはない。一流人材が参戦すれば変わる。 その一流の人材が膨大な人数どうやって確保するの？ 形式仕様言語でフルに仕様を書けばプログラムコードと同じオーダーの行数になるという経験則がある。 つまり数人で作れるおもちゃのソフトウェアならともかく、社会の根幹を支えそれが故に信頼性が必須とされる 大きなソフトウェアは現在の大規模開発でプログラミングに関わってる膨大な人数と同じオーダーの 形式仕様記述者が必要になるってことだ。 それだけ莫大な人数のそんな高い質の人材が世界のどこにいるんだい？ 寝言は寝てから言った方がいいよ。 それに数人のプロジェクトに限定しても、それを一流の人材で仕様記述しても それで作られたソフトウェアの寿命がある間は、そいつのメンテナンスのために ずっと一流の人材を貼りつけておかないと、彼らが書いた形式仕様なんて難しいものは ２流の人材じゃ読み書きできないから保守できないよね。ってことで一流の人材ほど 彼らが書いた仕様のお守をさせられて他の仕事ができなくなる。 これって素晴らしい才能の無駄遣い法だね。 33 名前：デフォルトの名無しさん mailto:sage [2013/01/26(土) 12:32:30.58 .net] 一流の人材を活用するとしたら 二流・三流の人が使える形式手法の技術を確立することだろうね そういう意味では一流の人材は既に集まっている ただ二流・三流が何たるかを理解できていない可能性はある 34 名前：デフォルトの名無しさん mailto:sage [2013/01/26(土) 19:14:58.59 .net] 用語定義で「名前： 2chに書き込むときの名前」てなこと書いておきながら 本編に「家で飼っているぬこの名前は〜」 とかしれっと書く奴はメタメタにしてやんよ！ 軽量形式手法なんて形式手法じゃねぇと思ってたが 名を捨てて実を取ることも必要だと感じた。 35 名前：デフォルトの名無しさん [2013/01/27(日) 23:46:08.13 .net] >>32 >形式仕様言語でフルに仕様を書けばプログラムコードと同じオーダーの行数に >なるという経験則がある。 だからあ！そういう今の形式仕様言語が糞なんだよお！まだ分からんのかあ！ 36 名前：デフォルトの名無しさん mailto:sage [2013/01/28(月) 01:17:16.05 .net] >>35 > >>32 > >形式仕様言語でフルに仕様を書けばプログラムコードと同じオーダーの行数に > >なるという経験則がある。 > だからあ！そういう今の形式仕様言語が糞なんだよお！まだ分からんのかあ！ ならば、形式仕様でフルに仕様記述するのが現実に可能だと主張したいのならば、 今のクソのでない形式仕様言語を現実に作ってからにしろ。 現実に存在しない夢のような形式仕様言語の存在を前提として>>13を主張するのは 単なる精神病患者だよ、誇大妄想と言う名前のな。 形式仕様屋にはこの手の誇大妄想患者が多すぎる。だから信用をなくして来たんだよ。 37 名前：デフォルトの名無しさん mailto:sage [2013/01/28(月) 01:22:14.84 .net] >>13は今のクソでない形式仕様言語を現実に作るために、一流人材が参加すれば可能だと述べているんだろ。 とはいえ、この論旨を許せば一流人材とやらがいれば世界征服すら可能になるが。 38 名前：デフォルトの名無しさん [2013/01/28(月) 08:48:24.11 .net] いまはむしろ誇大妄想がいないのが痛い。 だからユーザがプログラムと同じじゃないかと当たり前の苦情を言っても、 夢のような期待をするなと逆切れしてくる。 39 名前：デフォルトの名無しさん [2013/01/28(月) 08:56:42.23 .net] >>37 クソでない形式言語を作るのは世界征服と並ぶほど難しいことなのでしょうか？ 40 名前：デフォルトの名無しさん mailto:sage [2013/01/28(月) 18:52:03.46 .net] フルフル君さ、ちょっと聞きたいんだけど、どういう意味で「フル」って言ってる？ フルに詳細化された仕様？ そりゃロクに抽象せずに詳細化された仕様をベタに書けばプログラムソースと同様になるわなw 41 名前：デフォルトの名無しさん [2013/01/28(月) 19:23:10.47 .net] また抽象なんて甘いこと言って逃げるｗ ベタに書いたらプログラムと同等なるならダメなんよ 42 名前：デフォルトの名無しさん mailto:sage [2013/01/28(月) 19:29:38.21 .net] 逃げるも何も、それが仕様記述言語のポイントだろ…（呆 43 名前：デフォルトの名無しさん mailto:sage [2013/01/28(月) 19:31:37.37 .net] で、フルってどういう意味で言ってんの？ 44 名前：デフォルトの名無しさん [2013/01/28(月) 19:41:09.93 .net] よし。アンタの言う仕様記述言語のポイントは何か、逃げずに言ってみろ。 45 名前：デフォルトの名無しさん mailto:sage [2013/01/28(月) 20:14:25.27 .net] フルフル君でもそれに噛みついている人でもないが 記述量は確かに実用上の課題ではあるけども プログラムコードと同じオーダーなら駄目で短いならOKって 単純な話ではないと思うんだが 自然言語による仕様書の記述・検証の工数を無視しているのは意図的か？ それに形式的検証まで含むか否かで大きく変わる 証明された信頼性とテストによる確率的な信頼性は比較できない 自動コード生成が可能かどうかでも大きく変わる 46 名前：デフォルトの名無しさん mailto:sage [2013/01/30(水) 07:46:32.50 .net] PGが仕様記述言語でプログラム書いてるから、 プログラムと同じ長さになるんじゃね？ 47 名前：デフォルトの名無しさん [2013/01/30(水) 18:32:23.88 .net] その「仕様記述言語」は、もはや一種のプログラミング言語じゃ？ 48 名前：デフォルトの名無しさん mailto:sage [2013/01/30(水) 20:20:25.03 .net] プログラム言語を含んでいる仕様記述言語は多いね。 プログラム言語部分だけで仕様を書いちゃう人が 仕様がプログラムと同量だとか言い出すんだろうね。 49 名前：デフォルトの名無しさん [2013/01/30(水) 22:00:41.42 .net] >>45 >>46 >>47 >>48 仕様記述言語とプログラミング言語はどこが違うものなの？ 50 名前：デフォルトの名無しさん mailto:sage [2013/01/30(水) 23:21:07.11 .net] >>49 目的が違う 実際のところ言語やターゲットとなる案件によっては プログラミング言語でも仕様記述は不可能ではないし 仕様記述言語で実行可能なコードを書くこともできる 道具として両者を近づける試みも多数なされているが 仕様と実装をごっちゃにしようという話ではない あくまで仕様と実装は別の概念 51 名前：デフォルトの名無しさん mailto:sage [2013/01/31(木) 04:28:00.46 .net] 適切な抽象度を設定すればいいんだろうけど 仕様と設計がごっちゃになってくるから 「俺は今何を書いてるんだろう」ってなってしまう… VDMどうのこうのより、そもそもの設計経験とか抽象化の力が足りないってのが問題 52 名前：デフォルトの名無しさん mailto:sage [2013/01/31(木) 21:59:30.67 .net] 曖昧だったり矛盾を含んだりしている 自然言語の仕様書が幅を利かせすぎという面もある 世の中の仕様書が如何にいい加減か実感できるという点だけでも 形式的仕様記述を「体験」する意義は十分だと思うね 53 名前：デフォルトの名無しさん [2013/01/31(木) 23:37:20.78 .net] >世の中の仕様書が如何にいい加減か実感できるという点だけでも >形式的仕様記述を「体験」する意義は十分だと思うね 形式的仕様ってその程度で満足してもらえるんだ。進まんはずだ。 54 名前：デフォルトの名無しさん mailto:sage [2013/02/01(金) 00:36:31.59 .net] >>53 形式的仕様が誰かor何かに満足してもらえる なんて話はしていないと思うんだが 意図的なのか読解力がないのか分からんが オナニーなら一人でやってくれ 他人を使うな 55 名前：デフォルトの名無しさん mailto:sage [2013/02/01(金) 04:35:25.45 .net] >>53 >形式的仕様ってその程度で満足してもらえるんだ。進まんはずだ。 ほら、この日本語文1つ取っても書いた本人以外には意味不明だろ？ 56 名前：デフォルトの名無しさん mailto:sage [2013/02/01(金) 06:55:33.02 .net] 自然言語で契約交わすからこそ 世の中まわるという事実を無視されてもな… まぁクリティカル系はしらんが 一般には無用だよな 57 名前：デフォルトの名無しさん mailto:sage [2013/02/01(金) 20:30:05.57 .net] 別に契約書を形式言語で書くわけじゃあるまいし 自然言語で契約する＝>世の中まわる が真であろうと偽であろうと 形式的仕様の有用性を否定する理由にはならんよ もちろん肯定する理由にもならないが 58 名前：デフォルトの名無しさん mailto:sage [2013/02/01(金) 20:32:08.41 .net] 契約書に形式仕様が記載された例もあるらしいぞw 59 名前：デフォルトの名無しさん [2013/02/02(土) 21:42:41.80 .net] >>54 >>55 だから >世の中の仕様書が如何にいい加減か実感できるという点だけでも こんなことはたいしたことじゃないと言ってるんだよ つまらんこと言うな 60 名前：デフォルトの名無しさん mailto:sage [2013/02/02(土) 22:44:26.94 .net] たかが「体験する価値」にそんな高い敷居を設定するのか つまらん奴だな 61 名前：デフォルトの名無しさん mailto:sage [2013/02/03(日) 08:34:30.94 .net] 形式言語で仕様を記述したら テストパターンが自動生成されて テストツールに食わせたら自動でテストやってくれる ようになったら勉強しよう 62 名前：デフォルトの名無しさん mailto:sage [2013/02/03(日) 19:55:15.40 .net] >>61 お望みのレベルに達していないだろうけど テスト自動生成なら既に実施例や商品があるよ 産総研でも研究してたはず モデル検査でSATソルバ使うのが流行ってるっぽいんで テストケース生成技術・ツールはもう少し発展しそう 形式手法ではないがテストを仕様に近づけるというアプローチでBDDというのもある ただC++で使いやすいフレームワークは知らない 63 名前：デフォルトの名無しさん mailto:sage [2013/02/12(火) 20:50:42.97 .net] 実装がフレームワークとかで制限されているときって、VDMとかどう使うのがベターなんだろうか？ VDM仕様も制限するのか、VDMと実装との差はしょうがない、ってするのか よくわかんにゃい 64 名前：デフォルトの名無しさん mailto:sage [2013/02/12(火) 23:28:00.22 .net] とりあえずinv, pre, postで十分に制約がかけられているんなら 関数・操作の中身が実装と異なっても問題ないんじゃね あとは使い方次第としか そのフレームワークの特性にも依存するし 65 名前：デフォルトの名無しさん mailto:sage [2013/02/14(木) 19:11:21.64 .net] とりあえず、そのフレームワークに食わせるハンドラやコンポーネントの インターフェースを陰仕様で固めてみたら？ 66 名前：デフォルトの名無しさん mailto:sage [2013/02/14(木) 21:53:35.90 .net] >>64 >>65 ありがとうございます。まずは陰仕様ってことですね とにもかくにも書く目的をしっかりしないとダメですね 67 名前：デフォルトの名無しさん [2013/02/22(金) 11:18:28.53 .net] こういう従順な人はしばらく騙せるかもしれんが、まあ今の仕様記述言語は 使えんことはこのスレを見ていてもすぐにわかるな。 >一般には無用だよな そうだな。 一生懸命擁護弁護しようとしているのがいるがなんでなの？ だからスレも伸びん 68 名前：デフォルトの名無しさん mailto:sage [2013/02/23(土) 00:41:19.99 .net] 具体的な提案もなしに絡んでくるのがいるがなんでなの？ 駄目だと思うのは勝手だし2chに愚痴を書くのも勝手だが 批判できる立場かね？ 擁護弁護したいんじゃない議論がしたいんだよ 69 名前：デフォルトの名無しさん mailto:sage [2013/02/23(土) 00:51:39.71 .net] SIL4クラスの安全にかかわる案件に絡んでいるが 優秀な人間が何人も集まって検討した仕様にすら穴がある これはもう自然言語でやっている限りどうにもならないだろう 現状の形式手法では十分なソリューションたりえないのも事実だが 期待できるのは形式手法くらいしかないのも事実だ 現状が駄目だからといって将来が絶たれてよい技術ではない 70 名前：デフォルトの名無しさん mailto:sage [2013/02/25(月) 04:48:36.69 .net] 仕様の情報伝達力不足は SysML とかで補えばいいんでないの？ 71 名前：デフォルトの名無しさん mailto:sage [2013/02/26(火) 04:49:05.67 .net] 誤解しているようだが そういうのについてのスレなんだが 72 名前：デフォルトの名無しさん [2013/03/01(金) 20:47:27.99 .net] >現状の形式手法では十分なソリューションたりえないのも事実だが >期待できるのは形式手法くらいしかないのも事実だ そうなんだが、あまりに不満足な現状だとはおもわんか？ 73 名前：デフォルトの名無しさん [2013/03/16(土) 23:22:52.05 .net] それみろ。まったくスレがのびんだろ ＶＤＭはもちろんＡｌｌｏｙですらその程度なんだよｗ 74 名前：デフォルトの名無しさん mailto:sage [2013/03/17(日) 00:29:32.18 .net] テストしにくいコードをテストする方法教えて下さい toro.2ch.net/test/read.cgi/tech/1334408391/ でテストケースの自動生成で賑わってるけど同じ人？ 75 名前：デフォルトの名無しさん mailto:sage [2013/03/17(日) 06:38:43.65 .net] 2chなんかでクダ巻いて形式手法を批判した気になってるような低能は そもそもVDMやAlloyを始めることすらしないからじゃないかな 76 名前：デフォルトの名無しさん [2013/03/17(日) 09:55:15.86 .net] >>75 おまえは家来か 77 名前：デフォルトの名無しさん mailto:sage [2013/03/17(日) 10:04:04.95 .net] Alloy本読んで勉強中だが、結局のところ現実の問題をどうモデル化するかって ところがまだよくわからん。 例題でさらっとキャッシュメモリのモデルなんか挙げていたが、あんなの思いつかん。 そのへん、なんかいい参考書ないかねぇ？ 78 名前：デフォルトの名無しさん mailto:sage [2013/03/17(日) 13:16:00.02 .net] Alloyで数独を解くのが昔一部で話題になったけど そういう数理パズルとかで遊んでみるとか 79 名前：デフォルトの名無しさん [2013/03/17(日) 18:09:45.06 .net] >>77 そもそもふつうに思いつかんようなのがよいモデル化かな？ キャッシュメモリってどんな例題だったけ ちょっと見てみるかな 80 名前：デフォルトの名無しさん mailto:sage [2013/06/02(日) 21:23:41.48 .net] 業務ロジックを仕様記述言語で書くことは可能かな？ なんか、例を見てると並列処理の時の云々かんぬんとかかなりアルゴリズム的だったり、詳細よりだったりする例が多いのが気になる。 仕様のバグで一番多いのは論理矛盾だったりするので、 その辺が検出できそうなら導入してみたいんだよね。 81 名前：デフォルトの名無しさん mailto:sage [2013/06/02(日) 22:55:50.61 .net] 業務ロジックがどういうものか知らないけど仕様記述自体はできると思うよ ただ形式仕様記述ができることと 論理矛盾の検出ができることの間には大きな隔たりがあるのが現状 状態の数が限られているならなんとかなるけど 状態変数に実数とか時間を持つとなると途端に検証が困難になる 82 名前：デフォルトの名無しさん mailto:sage [2013/06/04(火) 02:08:31.54 .net] おお、そうなんだ。サンクス。 あんまりたいそうなロジックを扱ってるわけじゃないけど 取引ができる日がn日からm日で、そのうち取引ができるのはステータスがxの人で... とか、まあ、そういったものの組み合わせが多いかな。 最悪、論理矛盾の自動検出が出来なくても、曖昧性の無い記述ができるなら 仕様漏れとかが減ったりしないかなぁ。 83 名前：デフォルトの名無しさん [2013/06/29(土) 13:32:51.16 .net] >>80 >>81 >>82 > 業務ロジックを仕様記述言語で書くことは可能かな？ ていうか、そのためのものなんだがｗ いまの仕様記述を見てたらそんなことも分かりにくいが 84 名前：デフォルトの名無しさん [2013/06/29(土) 13:57:51.79 .net] 組込みっていうか車載開発（ボディ系）でAlloyを個人的に使おうと思ったが、 難しくて挫折しそうになった。。。C言語しか知らないとつらい。。。 85 名前：デフォルトの名無しさん mailto:sage [2013/06/29(土) 19:20:26.45 .net] >>84 組込み系であれば、(Alloy/VDM/Zなどよりも) 「振る舞い」の検証を重視するCSPやCCSのほうが (多くのケースでは)適しているのではないかと思われ もしもこれら形式的記述スタイルに慣れていないのなら、 PROMELA(およびその処理系であるSPIN)はいかが？ C言語とステートマシンの知識があれば、直感で理解できる 最近は、PROMELA/SPINに関する日本語書籍もいくつかあるよ 86 名前：デフォルトの名無しさん mailto:sage [2013/06/29(土) 21:00:02.42 .net] アドバイスありがとうございました。 積読状態ですが、VDMにAlloyにSPINに書籍は購入済みですので、 一度読んでみます。 Alloyに手を出したのは、VDMやSPINの両方のおいしいところを合わせたのと、 手軽にモデリングできると聞いたからです。 ・・・でも私には簡単ではなかったorz 87 名前：デフォルトの名無しさん mailto:sage [2013/06/30(日) 23:16:19.56 .net] 世界的には業務ロジックの構築=DSL(ドメイン記述言語)の流れじゃなかったけ。 88 名前：デフォルトの名無しさん mailto:sage [2013/07/06(土) NY:AN:NY.AN .net] DSLと形式手法は普通に両立すると思うが？ 89 名前：デフォルトの名無しさん [2013/07/16(火) NY:AN:NY.AN .net] Rodinはまともなチュートリアルないんか。 Event Bの理論は本読んでどうにかするとして、ツールとしてのRodinの使い方が公式のチュートリアル見てもよくわからん。 90 名前：デフォルトの名無しさん mailto:sage [2013/08/28(水) NY:AN:NY.AN .net] Code Contractsはこのスレの範疇？ 91 名前：デフォルトの名無しさん mailto:sage [2013/08/29(木) NY:AN:NY.AN .net] いいんじゃね？ 92 名前：デフォルトの名無しさん mailto:sage [2013/08/31(土) NY:AN:NY.AN .net] 形式手法が実用にならないと言われる中で Code Contractsは計算機科学とソフトウェア工学の中庸にあると思うけど あんまり話題にならないね Code Contracts目当てにProfessional買うことはないだろうから Express Editionにも対応してくれればいいのに 93 名前：デフォルトの名無しさん mailto:sage [2013/08/31(土) NY:AN:NY.AN .net] 乞食と思われると残念だから補足するけど 利用するライブラリが契約されてないと利用者側が馬鹿を見るので みんな契約すればいいのに！的な意味で 94 名前：デフォルトの名無しさん mailto:sage [2013/09/09(月) 00:32:04.39 .net] C++1yではConcepts復活すんのかな 95 名前：デフォルトの名無しさん mailto:sage [2013/09/12(木) 18:51:59.14 .net] prologじゃダメなの？（DSLも含めて） 96 名前：デフォルトの名無しさん mailto:sage [2013/09/12(木) 21:25:52.57 .net] >>95 そうね。少なくともDSLを記述して実行させるくらいなら 最初からPrologで書いてしまった方が気が利いていますね。 97 名前：デフォルトの名無しさん mailto:sage [2013/09/12(木) 22:36:29.89 .net] Prologで書かれた仕様を実装に落とし込むのは 自然言語で書かれた仕様を実装に落とし込む時とは 別の危うさがあるように思える バックエンドに使うんなら何でもいいけど 98 名前：デフォルトの名無しさん mailto:sage [2013/09/12(木) 22:38:55.18 .net] 具体化prz 99 名前：デフォルトの名無しさん mailto:sage [2013/09/12(木) 22:49:54.07 .net] ？ 100 名前：デフォルトの名無しさん mailto:sage [2013/09/12(木) 23:22:19.80 .net] スプレッドシードに書かれた自然言語の仕様書よりか、 prologの方が危ういって形式手法の危うさでも指すの？ wikipedia読む限り、形式手法が集合論と述語論理を扱う設計手法みたいだし、 その限りじゃprologで十分だよねとは思ったのだけれども、一体、何が悲しくて alloyやZみたく仕様がデカくて、ノウハウを使い回せない言語が乱立してんだろ 101 名前：デフォルトの名無しさん mailto:sage [2013/09/12(木) 23:47:46.69 .net] 自然言語よりPrologの方が危ういなんて書いてないだろ Prologで十分だというのが仮に事実だとしてそれが何なの？ その事実はPrologが優秀であることの証明にはならないし 他の技術を否定する正当性も与えない 102 名前：デフォルトの名無しさん [2013/09/13(金) 00:20:22.87 .net] 述語論理を書くならprologは有力なツールでしょうね。 でも、そもそも我々は述語論理を扱いたいんじゃないんです。 むしろ触れずに済むなら、その方がきっといいんです。 目的を忘れて手段を論じても無益でしょう。 103 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 07:56:11.25 .net] 集合論や述語論理を徹底的に研究した人はそんなにはいない。 あまりこれに拘った仕様の言語は大半の人には使い難い。 Prologくらい世俗的で下支えとしては述語論理がありますよ くらいの言語の方が万人向きでしょう、という話ですよ。 104 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 11:55:09.39 .net] は？徹底的に研究する必要なくてソフトウェア開発の道具として利用するだけ そもそも、集合論や述語論理のABCすら理解しないでAlloyやZを使う馬鹿いないだろ 105 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 11:59:30.78 .net] >>104 そうだと思いますよ。 106 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 12:20:24.26 .net] >>101 prologの優秀さは、その簡潔かつ可読性の高いコード。 無駄に仕様の大きな言語って、学習コストが高く、バグを誘発するだけ 少し前に途絶えた良い例がperlとcommon lisp 形式手法が集合論と述語論理を取り扱い、 その要件を満たす最小セットの記述がprologで済むのではないかと仮定したとき、 それに対するalloyやZがprologに対して如何なるアドバンテージがあるか って書いたの >他の技術を否定する正当性も与えない 技術を否定しない技術者って技術者に向いてないんじゃないの？ 人権屋とか宗教家にでも転職したら？ >>102 目的が形式手法への適応で、そこに集合論と述語論理が含まれるので述語論理を扱います。 そもそも述語論理のABCを理解してない非技術者がalloyやZを使うのか疑問です 目的を忘れて仕様の膨れあがったツールがalloyやZではないのかといったのが、 >>100のレスにおける核となる主張であり、疑問です。 が、その達観した無益なレスを書いて気持ち良いですか？ 107 名前：デフォルトの名無しさん [2013/09/13(金) 20:09:03.07 .net] つか、Prologで仕様記述なんてどこでやってんの 108 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 20:34:26.75 .net] >>106 >形式手法が集合論と述語論理を取り扱い、 >その要件を満たす最小セットの記述がprologで済むのではないかと仮定したとき、 その仮定「Prologは形式手法の要件を満たす」が間違っているんじゃないかね 述語論理だけを取り扱う、いわゆる純粋Prologの表現力は極めて乏しいものだ Prologプログラミングでは、カットや高階述語(assertなど)の非純粋な操作が必然となる 結果からすると、形式手法の要件である「検証」をPrologは満たさないことになる また、Prologは型付けの弱い言語だ 仕様を記述できたとしても、それに矛盾が無いことを「検査」できない 形式的な立場であれば、ある集合の要素はすべて同じ種類でなければならないが、 この種類、つまり型の一貫性をPrologでは保証できない点は、形式言語としては致命的な欠陥 109 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 20:42:25.00 .net] >>108 「仕様が記述できたとしても、それに矛盾がないことを「検査」できない」 はおかしいだろう。 質問として実行すればいいのではないかな。定理証明の過程なのだから。 110 名前：デフォルトの名無しさん [2013/09/13(金) 20:47:12.33 .net] では来週からPrologで仕様を書いてください。 111 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 21:04:25.47 .net] >>109 やはり形式手法という概念そのものが理解できていないようだね 仕様を実行して振る舞いを確認するのは「シミュレーション(模倣)」と呼ばれる手法であり、 「(形式手法における)検証」ではない 定理証明の過程において、対象となる仕様は「一切実行されない」ことを理解しなければならない これを実現するために、形式手法では厳密な数学を基礎に置き、それを元に証明を進める 112 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 21:16:04.80 .net] >>111 なるほどね。わかった。 動的言語云々ということが書かれていたので検査が実行されるのだと 思ってしまった。 113 名前：112 mailto:sage [2013/09/13(金) 21:22:31.21 .net] まちがえた。 動的云々ではなく、「型付けの弱い言語云々」でした。 114 名前：デフォルトの名無しさん [2013/09/13(金) 22:19:56.75 .net] でも形式手法をそういう言い方にするとAlloyやVDMの微妙さが際立ってしまうのだ 115 名前：デフォルトの名無しさん [2013/09/13(金) 22:56:23.06 .net] >>108 型や集合なら事実を加えるなりの規約程度で、どうにか出来そうなイメージ てか、形式手法って検証なんてステップあるのね。こうなると専用の言語つかった方がはやそう けれど誰かプレーンなprologで時相論理のサブセットとか書いてないのかな 第五世代のprolog hackerたちが、このスレを通ることに期待age 116 名前：デフォルトの名無しさん mailto:sage [2013/09/13(金) 23:21:23.48 .net] >>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 を参考にしたステートマシンをモデルとし、 シミュレーション(=模倣)による振る舞いの確認が可能 最終的にはペトリネットへ変換して検証する予定だったけど、着手できぬまま放置している 117 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 01:22:47.81 .net] VDM ToolsもOvertureも証明の機能が不十分だから 形式手法のレベルで分類すればVDMはもっぱら軽量じゃね？ まあこの際どうでもいいが 118 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 13:12:05.22 .net] >>117 形式言語 VDM と形式言語処理系 VDM Tools をごっちゃにすべきではない 言語 C と 処理系 gcc(あるいは VC++) をごっちゃにするようなもの 言語としての VDM は形式的な証明が可能な体系 (ただし、それを機械的に適用できるか否かは別の話) そして、処理系としての「VDM Tools はもっぱら軽量じゃね？」ならば、同意する 119 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 13:32:16.32 .net] そりゃごっちゃにすべきじゃない文脈もあるだろうが C言語の喩えで言えば gccもVCも対応していない機能はないようなものでしょ C言語の仕様策定は実装ありきだから そのうち対応する見込みはあるけど VDMで証明とかOverture界隈も興味の対象から外れている感じだし先が見えん 120 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 15:56:52.26 .net] >>119 >C言語の喩えで言えば >gccもVCも対応していない機能はないようなものでしょ んなわきゃーない。なんのための言語規格だ。 121 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 16:17:21.73 .net] 言語規格だか何だか知らんが絵に描いた餅でも喰ってろ VDM-SLはISO化されたが VDM++に関しては文法こそ仕様はあるものの 挙動は実装が仕様みたいな状況だぞ 122 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 20:04:31.44 .net] 挙動なんて言ってる時点で 静的解析をガン無視してるのはVDM界隈じゃなくて>>121だということがわかる。 123 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 22:53:25.27 .net] だったらVDMの静的解析に期待を持てるような 実績や活用法の情報をくれよ 124 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 23:08:58.11 .net] >>123 「だったら」が何を指すのか意味不明だし、また静的解析みたいな曖昧な言葉を持ち出す まだ >>123 は(言語としての) VDM における検証や証明を扱うレベルに達していないので、 無理に背伸びはせず(処理系としての) VDM Tools を触ることから始めたほうがいいと思われ ただし、今のままでは軽量と言われる VDM Tools ですら理解するのは難しいと思うがね 125 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 23:15:08.44 .net] >>122に言えよ 126 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 23:23:18.69 .net] >>125を翻訳すると、 「>>122くんの言葉を真似しただけだから、僕ちゃん悪くないもん！！」 127 名前：デフォルトの名無しさん mailto:sage [2013/09/14(土) 23:42:17.97 .net] >>124 選民意識も結構だが 「馬鹿には無理」みたいなこというから形式手法が馬鹿にされる ユーザに技術の存在を意識させないというのは 道具のあるべき姿の一つだが stealth formal methodsなんてフレーズが生まれるのは何かおかしい 128 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 00:48:45.39 .net] >>127 形式手法が何であって何ではないか、また形式手法では何ができて何ができないのか、 こんな基本的なことも>>123は分かっていないようだから、理屈よりも実践を、 つまり VDM Tools を触ることから/触れるレベルの学習から始めたほうがいいと アドバイスしてるだけだがね また>>127は「(形式手法の習得は)馬鹿には無理」と考えているようだけど、自分はそうは思わない 最低限必要なのは普通高校卒業程度の数学と教養であり、IT業界人やそれを目指す学生の大半が該当する ただし、本人にヤル気が無ければ無理だし、たとえあっても素直さと謙虚さは必要だがね 129 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 07:45:12.05 .net] >>123 つ 「型検査」 130 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 14:17:26.84 .net] 型検査なんかプログラミング言語で一般的過ぎて 期待も何もスタートラインだろ 整数（int, nat, nat1）とトークンだけで記述できる場合はまだしも レコードやクラスを使い始めると モダンなプログラミング言語に比べ使い勝手の悪さが目立つ さらに証明までやろうとすると証明責務が無理ゲーになる 結果としてユーザが気軽に型を作れない 131 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 14:34:04.62 .net] VDM++に関して言えば演算子オーバーロードはつけるべきだった メソッド名に全角の≦とかを使うなんてバッドノウハウは見るに耐えない インターフェイスやMix-inも言語レベルで対応してない テンプレートやジェネリクスもない これらはプログラマが楽するための道具に留まらず データ表現を抽象化してロジックに意識を集中させるために 仕様記述に有効な機能じゃなかろうか 132 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 16:58:56.24 .net] 証明しにくくするだけ 133 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 18:02:44.28 .net] 仕様を書く人が 証明のこと気にしないといけないのが未成熟な証 ASTなり中間言語にさえ落とし込めさえすれば あとは数学者やコンピュータサイエンティストの仕事だ 134 名前：デフォルトの名無しさん [2013/09/15(日) 18:22:03.16 .net] そりゃないわ。 135 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 18:35:46.84 .net] >>133 >あとは数学者やコンピュータサイエンティストの仕事だ いや、それはAI(人工知能)の仕事だよ 自然語で書かれた曖昧な仕様を、コンピュータが理解できる機械語へ変換するという もちろん、これが理想の姿であるのは理解するが、現時点では夢物語でしかない だから、自然言語で書く曖昧な(非形式的な)仕様の代わりに、 (数学を元にした)形式的な仕様記述を試みよう、という思想が形式手法の出発点にある >>133には、C.A.R. ホーアの言葉を送ろう： 　職業としてプログラミング業務を行うためには、基礎となる数学理論に基づき、 　すでに確立された他の工学分野の先例にならわなければならない。 　これは教育を改善することによって実現することができる。 　　　　　　　　　　　　　　　「プログラミング -- 魔術か科学か？」から引用 136 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 19:10:48.05 .net] 形式的な検証を目的に形式仕様を書くのなら 証明のことを気にするのは当然だろw 137 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 19:26:34.98 .net] >>135 だからそのAIを作るのは数学者やコンピュータサイエンティストで 言語のユーザでも言語屋さんでもないだろ >>136 気にした方が良い結果になることが多いだろうが 気にしないと使えないなら未熟だってこと 形式仕様を書くのは形式的な検証が主目的とは限らない 138 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 19:52:25.00 .net] 形式手法に限らず、大抵のものは「気にしないと使えない」だろ。 オブジェクト指向だって関数型だってCoqやAgdaだって、 記述目的を意識して書かないとクソな記述になるのと同じだろ。 139 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 20:06:00.03 .net] 程度問題だよ 少なくとも俺にとってはVDMとりわけVDM++は 仕様を記述するには気が利かないし面倒くさ過ぎる そのくせ証明による検証も大して期待できない 勿論そう思わない人もいるだろう そういう人は是非とも形式仕様記述を活用して普及に努めてもらいたい 140 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 21:08:48.08 .net] >>137 >だからそのAIを作るのは数学者やコンピュータサイエンティストで >言語のユーザでも言語屋さんでもないだろ もちろん、そのとおりだよ そして、AIの話題はスレ違いってことさ 141 名前：デフォルトの名無しさん mailto:sage [2013/09/15(日) 21:25:23.64 .net] スレチってほどでもないと思うけど SATソルバの話題とかしてもいいんじゃね？ どうせ過疎ってるか 愚痴や揚げ足取りの応酬しかしてないんだし 142 名前：デフォルトの名無しさん mailto:sage [2013/09/16(月) 00:03:43.85 .net] そんなことより、皆さん、どうやってデッドロック回避してるの？ 143 名前：デフォルトの名無しさん mailto:sage [2013/09/16(月) 00:42:33.03 .net] >>139 そういう態度を、評論家とかコメンテータという まあ、自分で理解できないのを言語やツールのせいにするのが許されるのは、お子ちゃま迄だよ 144 名前：デフォルトの名無しさん mailto:sage [2013/09/16(月) 19:32:39.59 .net] どっちが先に根負けするか賭けようぜ 俺は最初の奴とみた 145 名前：デフォルトの名無しさん mailto:sage [2013/09/16(月) 20:44:16.20 .net] どっちって誰と誰だよ 146 名前：デフォルトの名無しさん mailto:sage [2013/09/16(月) 20:50:19.99 .net] ざーっと追ってあなたの思う両者でよかろう 傍観者的には、すでに1on1じゃなく途中から同意見者が混ざって混乱してる可能性もありそうに感じた 147 名前：デフォルトの名無しさん mailto:sage [2013/09/16(月) 21:05:43.76 .net] ４，５人が入り混じった乱戦だろｗ 148 名前：デフォルトの名無しさん mailto:sage [2013/09/16(月) 21:14:01.04 .net] このスレで興味もってざっとぐぐってるんですが、なかなか面白そうな分野ですね。 書籍やサイトのお勧めあったらご教示願えると幸いです 149 名前：デフォルトの名無しさん [2013/10/02(水) 09:58:39.78 .net] >>100 >>133 >>137 この人センスいいねえ >>111 >>136 この人は単なる学習者 150 名前：デフォルトの名無しさん mailto:sage [2013/10/03(木) 20:35:05.95 .net] へー（ニヤニヤ Zの言語仕様がデカいと思っている人のセンスがいいとか言うのって 本人以外考えられないけどw 151 名前：デフォルトの名無しさん [2013/10/03(木) 23:29:48.73 .net] ニヤニヤすんな 要らん言うてんやろ 152 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 07:56:58.26 .net] で、Zの言語仕様のどこがデカいわけ？ ぼくちゃん学習者なんで教えてくださいませ〜 153 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 08:42:40.94 .net] >>152 単一化と導出・融合だけの pure Prolog に較べると途方もなく大きいのではないか。 154 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 09:17:10.07 .net] Zの言語仕様には単一化もレゾリューションもNAFもないよ。 どうして実行機構を持たないZのほうが言語仕様がデカいと思うんだい？ 155 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 10:09:22.67 .net] 言語仕様の大きさは 処理系やツールを実装する人にとっては重要かもしれないけど ユーザにとっては重要じゃないよね。 何ができるか・何をしないといけないかが重要。 そしてそれは言語仕様の大きさと必ずしも対応しない。 言語仕様の大きさで議論しようというのがそもそも筋が悪い。 言語仕様を全部把握していないと使えない訳じゃあるまい。 156 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 10:19:02.52 .net] 結論：>>100は筋悪 157 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 10:20:01.06 .net] その>>100を「センスいい」と言っちゃう>>149も筋悪。 158 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 12:53:16.23 .net] すじわる、って将棋以外で聞かない単語だよね。 まあ筋が悪いとは普通に使うんだから字面を見てわかると思うけど。 159 名前：112 mailto:sage [2013/10/04(金) 15:11:02.46 .net] >>154 ここでいう言語仕様とは学習しなくてはならない範囲の 意味が強いと思う。そういう意味なら、一人で使う場合は 別だが、他者の形式仕様を読む場合にはひと通りは抑えて いなくてはならず、Zはその点やはり負担が大きい。 160 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 16:02:12.94 .net] Zは基本的に述語論理と型付集合論がわかってれば 覚えなければならない事はとても少ないだろ。 むしろVDMやAlloyあたりのほうが 述語論理や型付集合論以外の言語要素が多いと思う。 Zで苦労するのは他の言語/手法と比べてツールサポートが少ないことだろ。 161 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 16:30:35.19 .net] >>160 Zについては、全てはこの本の後遺症だと思う。 amazon.com/dp/481018563X 162 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 16:33:28.90 .net] www.amazon.co.jp/dp/481018563X かな。 163 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 21:30:59.69 .net] ＺもVDMも基本は70年代の言語だからなぁ 比較的新しい言語だとCafeOBJなんかがあるけど 二木先生の関わっていない利用例を知らない 164 名前：デフォルトの名無しさん [2013/10/04(金) 21:49:13.71 .net] >>155 >言語仕様の大きさは >処理系やツールを実装する人にとっては重要かもしれないけど >ユーザにとっては重要じゃないよね。 誰にとっても同じだ。 同じことをするんなら小さい方がよいのに決まっとる >>160 だからZは要らんと言っとる >>163 CafeOBJが新しいのか 165 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 21:58:38.09 .net] >>164 そんなに言語仕様が小さいのがいいのならBrainf*ckなんか最高だよね チューリング完全だから「計算可能性の観点においては」 他の言語と同等のことができるよ 166 名前：デフォルトの名無しさん [2013/10/04(金) 22:06:34.37 .net] 観点は計算可能性だけじゃないだろ まだチューリング完全なんて言ってるのか 167 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 22:10:26.71 .net] 観点は言語仕様の大きさだけじゃないだろ って話だよ チューリング完全ならどれも一緒だなんて誰も思っちゃいねーよ 168 名前：デフォルトの名無しさん [2013/10/04(金) 22:30:01.22 .net] だれかこの辺の議論のような口喧嘩のようなことを交通整理できる人はいないでしょうか 169 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 23:00:21.87 .net] そういった態度というのは単に自信が無いだけなので、 生暖かく放置すればいいのではないかと思われ 170 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 23:07:34.51 .net] ところで、Prologで仕様記述やその検証ができるなら試してみたいんだが、 その方法を解説した本やWebサイトとかあるのかな？ 「理論的にはできるはず」だけだとProlog自体よく知らない俺には無理だが。 171 名前：デフォルトの名無しさん [2013/10/04(金) 23:08:43.39 .net] あんたは自信があるのかい 172 名前：デフォルトの名無しさん mailto:sage [2013/10/04(金) 23:32:01.69 .net] >>170 >ところで、Prologで仕様記述やその検証ができるなら できないんじゃね？ 過去には「できるはず...」という願望もしくは妄想に基づく意見(>>95-)はあったけど、 それに対する反論には何も意見を言えず議論を終えた 個人的には、型の無い純粋Prologを形式言語と呼ぶには無理があると考える Prologへの願望を語りたいという気持ちは理解できるが、 それはPrologスレで大いに語ればいい、それが妄想であってもいい 173 名前：デフォルトの名無しさん mailto:sage [2013/10/05(土) 05:30:54.75 .net] Prologで仕様記述しますなんていう例は山ほどある。 知らないんなら論文読まなさすぎ。 どれも結論は 「表現力不足だよね」 「表現上の制限が強すぎて、かえって表現が冗長になってダメだね」 「最低限FOLは必要だよね、やっぱし」 なわけだが。 174 名前：デフォルトの名無しさん mailto:sage [2013/10/05(土) 05:33:52.83 .net] >>164 >だからZは要らんと言っとる つまりZの言語仕様はデカくないという意見に反論できないってことね。 理由も言えずに「要らん」としか表現できない人が形式仕様とか、鼻で笑っちゃうねw 175 名前：デフォルトの名無しさん mailto:sage [2013/10/05(土) 08:56:49.36 .net] Alloyの本を読んでもちっとも頭に入っていきません。 この本を読むうえで必要な前提知識って何でしょうか？ また、その知識を得るのに最適な書籍があれば教えてください。 今は組込み関係の仕事（主に車関係）をしていて、知ってる言語はC言語のみです。 176 名前：デフォルトの名無しさん mailto:sage [2013/10/05(土) 10:07:18.70 .net] 知識はともかく 詳細仕様や実装仕様じゃなく 純粋なシステム仕様の読み書きをした経験がいるんじゃないかな 組込み関係だとシステム仕様と実装仕様がごっちゃになってる印象がある 実装仕様レベルの形式記述もできるけど そういうのは実装言語（C言語）のツールを使った方がいいと思う 177 名前：デフォルトの名無しさん [2013/10/05(土) 18:08:45.67 .net] >>174 その存在自体が無駄だと言っとるんだから、さらに何を言う必要がある？ Zや言語仕様の大きさなんていうくだらんことにどんだけ時間を浪費するんだ 178 名前：デフォルトの名無しさん mailto:sage [2013/10/05(土) 18:25:17.75 .net] Zを否定した根拠が「言語仕様のデカさ」だったのに 今更なにを喚いているんだい、負け犬くんw 179 名前：デフォルトの名無しさん mailto:sage [2013/10/05(土) 18:35:37.68 .net] 「C言語以外は全部無駄」とたいして変わらん主張 180 名前：デフォルトの名無しさん mailto:sage [2013/10/05(土) 22:31:33.47 .net] >>164は自分の主張が矛盾しているのに気付かない可哀想な子 >>160が言うように、Zは「述語論理と型付集合論」を知っていれば学習の壁は低い つまり、もしも>>164の言葉「同じことをするんなら小さい方がよいのに決まっとる」が正しければ、 仕様の小さなZは優れていていることになるが、その一方でツールサポートの少ない「Zは要らん」と言う では、ナゼそんな矛盾が生まれたのか？これは形式手法へ拒絶反応を起こす人によくあるパターンで、 形式手法を扱うのに前提となる素養(論理と集合)が欠けているからだろう だから>>164にはZの仕様が(とほうもなく)巨大に見えて尻込みしてしまう 逆にAlloyはツールで実際に動かしながら試行錯誤できるから容易い存在に見える 実際にはAlloyの全容は巨大で難解なものだけど、>>164には表層の一部しか見えていない おそらく、>>164はERM/OMT/UMLのような「仕様の視覚化手法(visualize method)」には 十分な経験と自信があるのだろう ところが残念なことに、その延長で「仕様の形式化手法(formal method)」を 理解しようとして、その狭間(ギャップ)で「もがいている」のだと思われる 181 名前：デフォルトの名無しさん [2013/10/05(土) 22:44:35.57 .net] >>175 述語論理ですかねー。あの変なシンタクスがオブジェクト指向と関係なくて、回りくどく表現された述語論理だと思うとたぶんわかってくる気がする。 あとAlloyだとたぶんその仕事にはあまり直接的に活かせないような。>>84-86に同じような話があるけど。 182 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 06:14:26.21 .net] >>180 そうだね、>>164みたいな人は10年か20年ぐらい前にもいたねえ。 「オブジェクト指向」でギャップに嵌ってる人達がね…（遠い目 UMLは図を「コトバ」として読む力が必要とされるんだけど、 形式手法では式を「コトバ」として読んじゃいけない。 式はあくまで記号列として読まないと「形式」の意味がわからない。 それができない人にはZは地獄のような言語かもしれない。 そういう人ほどZで徹底した形式主義を身につけたほうがいいと思うけど、 大抵は実行系中心の軽量形式手法で「これが形式手法かー」と思っちゃうんだよな… 183 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 10:50:33.15 .net] >>180 確かに、 Zは「述語論理と型付集合論」を知っていれば学習の壁は低いのだろうが、 そういう人材を一般企業では集められなかったからZは顧みられなかった のではないか。 184 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 11:30:50.49 .net] 述語論理も型付集合論も大学の教養レベルの数学で十分なのだから 「人材を集められなかった」のではないと思う。 単に、Zに限らず形式手法なしでもシステムを作れると思ってたんだろ。 だから、Zに限らずモデル規範型の形式手法は顧みられなかった。 185 名前：デフォルトの名無しさん [2013/10/06(日) 18:43:42.19 .net] >>182 >形式手法では式を「コトバ」として読んじゃいけない。 >式はあくまで記号列として読まないと「形式」の意味がわからない。 ここは何を言ってるの？記号列として読んでいるのでは意味が分かっていない と言われそうだけど。 186 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 22:31:52.02 .net] >>185 横レスだけど、形式手法の証明においては式に含まれる記号の意味は「無価値」だということ 記号の意味を分かる必要は無いし、 証明の過程で記号の意味は完全に無視され「形式(公理や定理)」だけが価値を持つ ソフトウェア仕様記述は現実世界のモヤモヤした実体(=モノ)をある体系でモデル化することから始まる たとえばUML等のOOA/OODでは現実世界をオブジェクトの集まりと捉え、オブジェクトの持つ属性や オブジェクト間の(継承や部分といった)関係を定義することによって(非形式的な)モデル化を進める ここでは実体をコトバとして抽象化する事を、具体的には定義するオブジェクト/属性/関係などの 命名(naming)を、つまり(人にとっての)直感的な意味を重要視する これによって(人にとって)分かりやすく、特に共同作業下における仕様イメージの統一的な共有化を図る これに対して、形式手法では現実世界をモデル化することは(視覚化手法と)同じだけれど、 数学という形式的な体系を用いる点が異なる つまり、ある式(=モデル)が直感的には(=人にとっては)いかに分かりやすくて正しく見えようとも、 いいかえるといかにOO的視点では優れた設計であっても、形式に矛盾があれば誤りであると見なす 187 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 22:55:41.08 .net] >>186 こっちも横レスだけど 証明は形式意味論のレイヤーで行われるけれど 形式仕様自体は現実世界の概念（「コトバ」）とリンクしている 「コトバ」であり「記号列」であることを理解できないと 形式仕様を理解したことにはならんだろう 188 名前：デフォルトの名無しさん [2013/10/06(日) 22:57:20.47 .net] >>186 >形式手法の証明においては式に含まれる記号の意味は「無価値」だということ それは証明器にとって、ということでしょう。人間にとってではない。 >これに対して、形式手法では現実世界をモデル化することは(視覚化手法と)同じだけれど、 そのモデル化の時点で、「意味」が介在するよね。 >形式に矛盾があれば誤りであると見なす それは当たり前。矛盾というのは形式的なものだからね。 だからといって「意味」が不要ということにはならない。 189 名前：デフォルトの名無しさん [2013/10/06(日) 23:01:03.54 .net] 「形式」手法 "form"-al method という言葉の意味からはじめないといけないようだな！ 190 名前：デフォルトの名無しさん [2013/10/06(日) 23:11:16.30 .net] >>189 およその意味はみんな分かってると思うが その厳密な定義もない（あるいは厳密に定義する意味もない）ことも含めて だがもし必要なら、そこからはじめてくれてもよいが 191 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 23:15:39.39 .net] みんな数学ガール／ゲーデルの不完全性定理 でも読んで和みたまえ（ステマ） 192 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 23:30:11.15 .net] >>187,188 現実世界を抽象化する過程に意味が伴うのはその通りで、視覚化手法も形式手法も同じ 形式手法にとっても抽象化の過程ではコトバの意味が大切なのに変わりはない 違うのは、抽象化の成果物である「仕様(設計書)の検証」において、視覚化手法では (人間が介在する)直感を頼りとしており、そこではコトバの意味が重要な位置を占める それに対して形式手法では仕様の検証に人の直感は介在せず、コトバの意味は無視する ここで、証明(=形式を元にした検証)を人力でやろうが証明器で自動化しようが同じ そして、もし証明が失敗すれば(仕様に矛盾を発見すれば)、現実世界の抽象化という前工程に立ち返る その時には、(数学としての)形式化の単純ミスもあるだろうけど、コトバの意味(の定義)の過ち、 つまり(抽象化の過程で)現実世界の解釈に何か誤りや漏れがあったことが発見できるだろう 193 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 23:45:46.18 .net] >>188 >>形式に矛盾があれば誤りであると見なす >それは当たり前。矛盾というのは形式的なものだからね。 いや、「非形式的な矛盾(=直感に基づく矛盾)」というのは存在する たとえばOOの仕様で、ある箇所では「XはYのサブクラスである」と記述され、 別の箇所では「YはXのサブクラスである」と記述されていれば、それは矛盾だろう ただし、サブクラスというオブジェクト間の関係は(人の)直感として定義されたものだから、 それは「形式的な矛盾」ではない 194 名前：デフォルトの名無しさん mailto:sage [2013/10/06(日) 23:49:56.14 .net] この会話が成立していないのに 話が流れていく感じはすごいな 形式手法に言及しているのに 詭弁（誤謬）ばかりってのが皮肉 195 名前：デフォルトの名無しさん [2013/10/07(月) 06:12:47.77 .net] >>193 >「非形式的な矛盾(=直感に基づく矛盾)」というのは存在する 形式的に意味不明な言明だ。 論理的訓練が不十分のようだから指摘しておく。 >別の箇所では「YはXのサブクラスである」と記述されていれば、それは矛盾だろう 矛盾とはAかつ¬Aが帰結することだ。「XはYのサブクラスである」と 「YはXのサブクラスである」はまだ矛盾ではない。 >ただし、サブクラスというオブジェクト間の関係は(人の)直感として定義されたものだから、 そういう関係もまた形式的に記述するんだよ。 >>194 >形式手法に言及しているのに >詭弁（誤謬）ばかりってのが皮肉 意味不明。間違いがあれば指摘すればよい。 形式手法＝無謬ということではない。形式手法を偶像崇拝してる？ 196 名前：デフォルトの名無しさん [2013/10/07(月) 08:17:29.48 .net] >>192 概ね妥当なコメントと思うが 「視覚化手法」なんてものを形式手法と対比させるのはいかがなものか それから、ここでは皆矛盾矛盾と言うが、矛盾がないというのは最低限の条件に過ぎない 197 名前：デフォルトの名無しさん mailto:sage [2013/10/07(月) 08:39:38.60 .net] >>184 20年近く前に、私の周辺でZの研究会が次々と撃沈していったのを 知っている私としては、隔世の感ありだな。 198 名前：197 mailto:sage [2013/10/07(月) 08:43:06.72 .net] 研究会 -> 勉強会 199 名前：デフォルトの名無しさん [2013/10/07(月) 09:12:11.96 .net] >>197 撃沈の主な原因は何だったのですか？ そのころなら述語論理や集合論ではないと思うのですが 200 名前：デフォルトの名無しさん mailto:sage [2013/10/07(月) 09:27:05.81 .net] 計算機の性能だな 20年前のCPUの性能ではSAT SMTソルバーをぶん回すとかありえんだろう 201 名前：デフォルトの名無しさん mailto:sage [2013/10/07(月) 09:27:11.00 .net] >>199 隔世とは、大学の教養レベルの水準が上がっているのだなぁという 漠然とした印象です。 直接の原因はテキスト(>>162)にあったと思います。これに限らず、 勉強会がうまくいくかどうかには、早い段階で良い要約を誰かが 準備してくれるかどうかが大事ですが、それをしてくれる人が いなかった。それでほとんどの人に全貌が見えなかった。 202 名前：デフォルトの名無しさん mailto:sage [2013/10/07(月) 10:13:24.23 .net] >>195 スマン、言葉が足りなかったようだ >>193での「非形式的な矛盾」とは「(UMLのような)非形式手法における矛盾」のこと そして非形式手法においても矛盾(という概念)は(人間的な)直感として存在していることを言いたかった たとえそれが形式主義の視点では「意味不明な言明」であったとしても.... >>ただし、サブクラスというオブジェクト間の関係は(人の)直感として定義されたものだから、 >そういう関係もまた形式的に記述するんだよ。 形式手法であれば、構築しようとする体系(システム)におけるサブクラスという関係を (形式的に)定義するのは当然のことだね ここで、もしもサブクラスの(形式的な)定義に交換律を含めれば、 「XはYのサブクラスである」かつ「YはXのサブクラスである」(という仕様記述)は矛盾ではなくなる つまり、(形式手法の)証明ではサブクラス(というコトバ)から人が連想する直感的な意味は無視される たとえば、仮にサブクラス(というコトバ)の代わりに机や椅子(というコトバ)で仕様が記述されていても (無矛盾であることを)証明できるのが形式手法であり、それが非形式手法との違いになる 203 名前：デフォルトの名無しさん [2013/10/07(月) 12:14:52.74 .net] >>202 >交換律を含めれば 細かいのだが、ここは、反対称律を含めなければ、だな >つまり、(形式手法の)証明ではサブクラス(というコトバ)から人が連想する直感的な意味は無視される >たとえば、仮にサブクラス(というコトバ)の代わりに机や椅子(というコトバ)で仕様が記述されていても >(無矛盾であることを)証明できるのが形式手法であり、それが非形式手法との違いになる この辺り、ヒルベルト流の「形式主義」の説明なら妥当だが、ソフトウェア工学の「形式手法」の 説明としては相当ズレてると思う 204 名前：デフォルトの名無しさん mailto:sage [2013/10/07(月) 17:30:11.68 .net] >>203 識別子の字面に引きずられるようなら、その時点で形式手法を使う意味は半減するよ。 形式仕様を読み書きする時には、字面が持つ自然言語的意味を無視して あくまで記号操作の対象として扱う。 識別子の字面が大事になるのは、形式手法を知らない人に説明する時。 「形式的に」扱う訓練を受けていない人のために非形式的意味を使う。 非形式的な意味を持たせた時点で、その記述は形式仕様ではなくなる。 205 名前：デフォルトの名無しさん mailto:sage [2013/10/07(月) 20:32:26.92 .net] pi = 3.14159 e = 2.71828 と e = 3.14159 pi = 2.71828 で「後者に違和感を持つのは間違い」という奴の 形式仕様は読みたくないな 形式仕様からプログラムコードを自動生成してメンテナンスフリーというならともかく それがソフトウェアなり何なりの「仕様」を定めている以上 非形式的な意味は持たせてもいいし それによって非形式的仕様になる訳じゃない 非形式的な意味は形式的検証の結果に影響を与えないのだから 206 名前：デフォルトの名無しさん [2013/10/07(月) 20:40:11.24 .net] >>205 >形式仕様を読み書きする時には、字面が持つ自然言語的意味を無視して >あくまで記号操作の対象として扱う。 そんなことをは君（人間）は気にする必要はないのだ。 放っておいても証明器は完璧にそうしてくれる。 同じことを君（人間）がやってもそれこそ効果は半減する。 書くことは人間にしかできないのだが，そのとき「記号」で書いていては， そもそもどういう対象を書いているかが分からないだろう？ｗ >「形式的に」扱う訓練を受けていない人のために非形式的意味を使う。 訓練を受けているとかいないとかでなく、どんな相手だろうと、何を書いて いるかを伝えるためには、単なる記号では伝わらないんだよ。 >非形式的な意味を持たせた時点で、その記述は形式仕様ではなくなる。 これも違う。人間がどういう読み方をしようと、machine readableであれば 形式仕様なんだよ。 あと、君が「形式手法を知らない人」「訓練を受けていない人」とよく 言ってるらしいのが気になるな。 207 名前：206 [2013/10/07(月) 20:42:57.52 .net] 誤　>>205 すまん 正　>>204 208 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 02:10:26.26 .net] ここで思いのたけを質問したらどうですか？ topse.or.jp/2013/10/2023 209 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 17:34:58.34 .net] >>206 >これも違う。人間がどういう読み方をしようと、machine readableであれば >形式仕様なんだよ。 じゃあポインタをキャストしまくってるCのソースも形式仕様だねw 210 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 17:39:04.75 .net] >>206 >同じことを君（人間）がやってもそれこそ効果は半減する。 残念ながら、その形式言語の表現力がFOL以上であれば、 (非定理を含む)あらゆる式を自動的に証明可能なアルゴリズムは存在しない。 211 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 17:41:09.34 .net] >>205 >e = 3.14159 >pi = 2.71828 まさに、こういうまやかしに惑わされないために 先入観を排して記号を記号として扱う訓練が必要なんだよ。 212 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 18:46:34.06 .net] エラーや例外が発生しないプログラムが必ずしも「正しい」訳じゃないように 形式的に無矛盾な仕様が必ずしも「正しい」訳じゃない 無矛盾な証券決済システムの仕様は 鉄道運行管理システムの仕様としては全くもって正しくない 記号を記号として扱うのは機械でもできるし機械の方が得意だ しかし形式意味論では扱わない記号に込められた「意味」を読み取るのは 現状では人間にしかできない 機械が得意なことは機械に任せて 人間は人間にしかできないことに力を入れる方が得策だろう 213 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 19:41:41.07 .net] >>212 なら自然言語とか図形言語で仕様書いてれば？ 214 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 19:51:16.96 .net] 機械が形式仕様を書いてくれるようになったら やってもいいかもね 215 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 20:22:13.24 .net] >>214 それが可能ならそれこそ形式仕様なぞ不要だな そもそも何でも証明器で検証するのが前提になってる>>206は 形式手法にどんな夢を見ているんだ？ >>206 > 放っておいても証明器は完璧にそうしてくれる。 > 同じことを君（人間）がやってもそれこそ効果は半減する。 残念ながら証明器は放っておいても何もしてくれない。 証明器を有効に使うために必要なエフォートを知った上での 主張とは思えない。 > どんな相手だろうと、何を書いて > いるかを伝えるためには、単なる記号では伝わらないんだよ。 piを「円周率」として読むレベルの厳密さで良いのであれば、 拘束文法による半形式仕様で十分だ。 216 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 20:40:26.34 .net] >>215 とりあえず俺は>>206じゃないが 複数の人間の発言を一緒くたにされても困る >>そもそも何でも証明器で検証するのが前提になってる 証明器での検証を前提としない軽量形式手法においては 人間に意味が伝わらない仕様は使い物にならない 形式仕様は自然言語の曖昧さの排除が目的であって意味の排除じゃない > 残念ながら証明器は放っておいても何もしてくれない。 人間が記号を記号として扱ってメタな意味を排除すると証明器は何かしてくれるの？ 217 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:11:58.28 .net] >>216 > 証明器での検証を前提としない軽量形式手法においては 全てを証明器でやるわけではないからといって、 必ずしも証明器での検証を前提としないわけではないだろう。 形式仕様スレでこんな論理の基礎を指摘しなきゃいかんのか？ > 人間が記号を記号として扱ってメタな意味を排除すると証明器は何かしてくれるの？ はあ？ まだ証明器が何もかもやってくれるとでも思ってるのか。 証明器はドラえもんのポケットじゃないぞ。 218 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:17:28.76 .net] 言葉が通じないというか 相手の発言の意図を汲もうという気が感じられないな 219 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:19:40.69 .net] 発言の意図を汲み取ってクレクレ言う人が形式手法とは恐れ入った！ 220 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:27:43.77 .net] 現行の証明器の能力が限られてることと 人間が非形式的な意味を排して形式仕様を読まなければいけないことの間に 随分と論理の飛躍があると思うんだけど 非形式的な意味を排して形式仕様を読める能力が必要だとして 形式仕様から非形式的な意味を読み取るor 形式仕様に非形式的な意味を書き記す能力が 同時に成立しない・成立させてはいけない理由は何？ 両方の能力が必要なんじゃないの？ 221 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:28:51.63 .net] >>212 >無矛盾な証券決済システムの仕様は >鉄道運行管理システムの仕様としては全くもって正しくない ミスリードが2つある。 1つ目は、無矛盾な証券決済システムの仕様があったとしても その仕様が証券決済システムの仕様としてvalidとは限らない。 なのにあたかも証券決済システムとしてvalidであるかのように、 鉄道運行管理システムの仕様としてinvalidだと主張している。 2つ目は、条件なしに「全くもって正しくない」と書いていることから、 「全ての」無矛盾な証券決済システムの仕様が 鉄道運行管理システムの仕様として「完全にinvalid」だという主張になる。 これは正しくない。 無矛盾な証券決済システムの仕様のうちいくつかは 鉄道運行管理システムの仕様としてinvalidな部分がある、 というならば、それはそうだろう。 もっとも、 無矛盾な証券決済システムの仕様のうちいくつかは 証券決済システムの仕様としてinvalidな部分がある、 も正しいがな。 222 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:34:10.43 .net] >>220 「同時に成立しない・成立させてはいけない」なんて主張はしていない。 それは>>204を読んでくれ。 その>>204に対して 「いや、証明器があるから、人間は形式仕様を自然言語的な意味で解釈すればいいんだ。人間が自然言語的な意味を排除する必要なんてないんだ。」 という主張をしている人がいるんだ。 223 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:38:17.58 .net] >>221 言ってる内容については理解するけどね そういう揚げ足取りをするなら 「全くもって」を全体と部分の議論にすり替えてるのはミスリードじゃないの？ >1つ目は、無矛盾な証券決済システムの仕様があったとしても >その仕様が証券決済システムの仕様としてvalidとは限らない。 それを理解している人なら >e = 3.14159 >pi = 2.71828 を「まやかし」だなんて思わないだろう 224 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:47:32.85 .net] >>222 > 形式手法を使う意味は半減するよ。 これが文字通り意味が50%になるって主張なら「同時に成立させてはいけない」とは言ってない。 しかし明らかにこの発言には「識別子の字面に引きずられてはいけない」という 否定的な主張が含まれている。 違うかね？ 225 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:50:53.87 .net] >>223 いや、実際その例はまやかしだよ。 じゃあ pi = 3.1415926532 だったらどうする？ piを円周率だと思って読み進めて地雷作る？ eだろうがpiだろうが3.14159だろうが3.1415926532だろうが 「記号として書いてある通り」 に理解して 「記号として定義されている通り」の振る舞いについて validityを評価するしかあるまい？ 226 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:51:58.92 .net] >>224 字面に引きずられて、それで「形式手法やってます」と言えるの？ 227 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:54:39.89 .net] >>225 お前は自然言語が使えるんだろ？ 「ここの記述はミスじゃないですか？」 「書き換えても検証結果は変わらないしミスということで直しましょう」 こんなやりとりもできないの？ 228 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:59:09.82 .net] >>226 形式的な意味しかない記号の列を作って「仕様書いてます」と言えるの？ 229 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 21:59:21.79 .net] >>227 つまり>>204に賛成なわけだね？ 形式仕様として読む上では記号列をして操作し、 非形式的な説明においては自然言語的意味を使う。 そういうことだろ？ ところで、 >>225 > じゃあ > pi = 3.1415926532 > だったらどうする？ このpiは円周率ではないことには気付いたよな？ 230 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 22:01:28.11 .net] >>228 それで正しいシステムが出来れば、堂々と「仕様書いてます」と言っていいだろ。 もちろん、形式手法やっていない人とは非形式的意味を使って説明した上で。 231 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 22:38:00.15 .net] 「形式仕様として扱う時には記号列として操作する」 ここから「全ての状況において非形式的扱いをしない」を導き出しちゃうとはね。 どんな論理体系なんだろうな。 232 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 22:47:35.90 .net] >>228 まさか形式仕様スレでこんな幼稚な主張が出てくるとはね… 「自然言語的な意味に引きずられずに、記号を記号として操作する訓練が必要」 ここからどうして 「形式的な意味しかない記号の列を作って」 となるかが不明。 この人にとって形式仕様とは一体何なんだろう。 例えば注釈なしのペトリネットやオートマトンで記述したものは 仕様を構成するドキュメントとは認めないのだろうか？ ぜひ拝聴したくなった。 233 名前：デフォルトの名無しさん mailto:sage [2013/10/08(火) 22:54:15.62 .net] 批判するなら>>182-の文脈を加味してもらいたいものだね 234 名前：デフォルトの名無しさん mailto:sage [2013/10/09(水) 06:20:38.89 .net] >>180と>>182の2人は理論と経験が伴ってるね 235 名前：デフォルトの名無しさん mailto:sage [2013/10/09(水) 14:42:56.90 .net] >>234 君を含めて、三人は理論と経験が伴ってることになるね。 236 名前：デフォルトの名無しさん mailto:sage [2013/10/09(水) 15:53:49.68 .net] 4人目が現れた 237 名前：デフォルトの名無しさん mailto:sage [2013/10/11(金) 08:11:23.53 .net] 導入事例はよ はよ 238 名前：デフォルトの名無しさん [2013/10/11(金) 22:31:20.64 .net] 【会社の即戦力の定義とは】 「社会の一員として人々の役に立つ価値を提供すること」 会社にとって喉から手が出る程欲しい人材とは、 この求められる価値を提供するために、解決すべき 課題を正しく共有し、一緒になって価値を生み出す ことが出来る人材なのです。 ところがＪＡＬグランドサービスの即戦力って言っている奴らは自分の気の合う人には仲良くするけど 気に入らない人間には粘着してとことんまで罵倒したりパワハラしたり自分にはとことん甘いくせに人の揚げ足ばかり探して 仕事中も喋ってばかりで口元緩んでばかりじゃないか 先に暴言を吐けば自分が強いと思わせることができるなんて考えているみたいだけどそれは違う　 それは弱い動物がキャンキャン吼えているのと同じことだよ ＪＡＬグランドサービスは仲良しクラブ会社　仕事中　趣味の話で盛り上がって手が止まってんだよｗ たまには仕事まじめにやったらどうだね？ 239 名前：デフォルトの名無しさん [2013/10/11(金) 22:32:05.51 .net] ＪＡＬグランドサービスは貧乏性でテーブル拭いて汚れたタオルを次の清掃場所 さらに次の清掃場所にもっていって汚れたタオルを使えっていってきた タオルからはなんともいえない臭いが漂い色もケチャップやなんやらがこびりついていて汚かった お客さまのためにを毎日言っている会社なのになにこれ？　矛盾してるよね？ 青タオルはウンコがこびりついていて汚い　それをキレイなタオルといいラバーのほかギャレー 床のゲロ掃除などさまざまなところで活用している バケツにそのタオルを濡らすとき気持ちが悪い　バケツもすごく汚いよね バケツ洗っているところみたことがないし ＪＡＬはこんな会社です 白タオルは生乾きで蒸れた悪臭がしている　それでお客様がつかうテーブルを拭いているんだから あのテーブルは菌をひろげているようなもんだ 240 名前：デフォルトの名無しさん [2013/10/11(金) 22:32:50.46 .net] ＪＡＬグランドサービスはパートやアルバイト、契約社員に対し若い正社員ですら横柄かつ高圧的な言動（恫喝行為など）を取ることが常態化されていて それを正せる上司が一人もいないというのが特徴の会社 241 名前：デフォルトの名無しさん [2013/10/11(金) 22:33:27.02 .net] 人が見えにくい場所で係長がとある気弱な社員のわき腹を殴ったり 蹴っ飛ばしたり頭を殴ったりしていた あれをパワハラといわずになんていうのか？ こんな屑なことばかりやっている悪質な会社ＪＡＬの傘のなかでふんぞり返っているのだから ＪＡＬそのものがたいしたことがないといえるだろう 班長　係長　課長とも人間としての品格を疑うことがおおい 常軌を逸した行動を認知していながらそれを容認しているＪＡＬグランドサービス フィロソフィなどただ毎日口にだして読んでればそれで満たされる ただそれだけのもの　どんなりっぱな言葉を並べたとこでそれを毎日読んでる人間が バカじゃ意味がない　陵辱　ひとの足をひっぱったり人を不幸にしている ＪＡＬグランドサービスが物心両面の幸せだと？　笑わせるなｗ　クズ会社がｗ 242 名前：デフォルトの名無しさん [2013/10/11(金) 22:34:12.22 .net] ロッカーの一番奥の壁を誰かが蹴っ飛ばしたのかなんだかわからないけど 大きな穴があいて破損させた馬鹿がいたよね？ 犯人つかまったの？ あれだけの穴があいていて音が聞こえなかったなんておかしいよね？ こんな不祥事はこの会社しかないだろうしあれだけ人が多いロッカーで誰も気がつかないのもこの会社だけｗ アホＪＡＬグランドサービスｗ 243 名前：デフォルトの名無しさん mailto:sage [2013/10/14(月) 19:13:20.13 .net] スレタイを二度見した 244 名前：206 [2013/10/15(火) 23:09:23.21 .net] >>219 >>225 >>226 >>230 >>232 年齢は20代、アスペと見た 245 名前：デフォルトの名無しさん mailto:sage [2013/10/16(水) 01:29:13.48 .net] >>188=>>206が暴れているだけで 他の人は多少の立場の違いはあっても 根っこの部分は妥当なことを言ってるな 246 名前：デフォルトの名無しさん mailto:sage [2013/10/16(水) 01:44:38.47 .net] 素朴に疑問に思ったのだが このスレは時折 「形式主義を否定した形式手法」 とおぼしきものが主張されているようだが これは軽量形式手法の一派か何かなのか？ 通常のソフトウエア工学では 形式手法とはシステム記述に形式主義を導入して 形式主義的な検証や開発をおこなうこと を指すと思うのだが... 247 名前：デフォルトの名無しさん mailto:sage [2013/10/16(水) 01:58:15.28 .net] 技術として否定的（悲観的というべきか）であっても 形式主義の否定はしてないんじゃ？ 表現が拙いだけで 「通常のソフトウェア工学」とかしれっと言っちゃうあたり >>246も大して変わらんレベルなような印象を受けるが 248 名前：デフォルトの名無しさん mailto:sage [2013/10/16(水) 01:59:18.39 .net] >>205 >e = 3.14159 >pi = 2.71828 >で「後者に違和感を持つのは間違い」という奴の >形式仕様は読みたくないな そういう話なのか？ hoge = 2.0 * pi * r という形式的定義があった時に 円周率や半径の類推から piやrの形式的定義を辿らずに hogeを円周の長さだと思い込んではいけない という話なんじゃないのか？ 249 名前：デフォルトの名無しさん mailto:sage [2013/10/16(水) 02:03:25.11 .net] >>247 例えば>>188は 形式主義を真っ向から否定しているようだが？ 250 名前：デフォルトの名無しさん mailto:sage [2013/10/16(水) 02:16:17.00 .net] >>248 そういう話も包含されているだろうね 仕様を書く人は誤解を生まないように気を付けた方が良いし 仕様を読む人は思い込みをしないように気を付けた方が良い そんな凡庸な結論では刺激が足りない人が 極論で言葉遊びしているのがこのスレ >>249 もっと具体的に言ってくれないと同意も否定もできん 251 名前：デフォルトの名無しさん mailto:sage [2013/10/16(水) 03:00:35.01 .net] 式に含まれる記号の意味は証明（記号の操作）に無関係である しかし人間は様々な形式化されていない知識を持っている それは当該の公理系においては誤ったあるいは誤っているかどうか判断出来ない 推論規則をもたらす知れないが無価値とは言えない どのくらいの価値があるかは適用場面や人の価値観によるだろう 252 名前：デフォルトの名無しさん [2013/10/16(水) 09:03:40.50 .net] >>209 >じゃあポインタをキャストしまくってるCのソースも形式仕様だねw ということになるね。なぜダメ？ あなたの定義は？ 253 名前：デフォルトの名無しさん mailto:sage [2013/10/16(水) 09:18:21.22 .net] Cは未定義動作や実装依存があるから 形式的意味論が定義されているとは 言えないんじゃないかなー 254 名前：デフォルトの名無しさん mailto:sage [2013/10/16(水) 09:19:58.66 .net] 機械可読なら形式仕様って それじゃエクセル方眼紙も形式仕様かよw 255 名前：デフォルトの名無しさん [2013/10/16(水) 09:21:06.47 .net] >>246 >形式手法とはシステム記述に形式主義を導入して >形式主義的な検証や開発をおこなうこと >を指すと思うのだが... ちょっと違う。「主義」をはずせばよい。 >>248 >そういう話なのか？ >hoge = 2.0 * pi * r >という形式的定義があった時に >円周率や半径の類推から >piやrの形式的定義を辿らずに >hogeを円周の長さだと思い込んではいけない >という話なんじゃないのか？ いや、そもそもhogeやrを円周や半径と思ってはいけないと言ってるんだろ？ それに、いくら形式的定義を辿ってもhogeが円周だとはわからないよ >>249 >形式主義を真っ向から否定しているようだが？ 形式主義を否定してるんじゃなくて、形式手法＝形式主義ではないと言ってる >>250 >仕様を書く人は誤解を生まないように気を付けた方が良いし >仕様を読む人は思い込みをしないように気を付けた方が良い 随分ぬるいがｗまあそういうことだ。記号病達にはこれも伝わらないのじゃないかな 256 名前：デフォルトの名無しさん mailto:sage [2013/10/16(水) 09:28:13.23 .net] >>255 > 「主義」をはずせばよい。 formal methodsからformalismを取ったら何が残るの？ばかなの？ > それに、いくら形式的定義を辿ってもhogeが円周だとはわからないよ hogeを円周と読むなって話だということが理解できない？ばかなの？ 257 名前：デフォルトの名無しさん mailto:sage [2013/10/16(水) 09:35:15.08 .net] >>255 既に誰かが指摘しているようだが あなたが形式手法と呼んでいるものは 制限文法による仕様記述なのでは？ 258 名前：デフォルトの名無しさん [2013/10/16(水) 09:47:51.55 .net] >>256 >formal methodsからformalismを取ったら何が残るの？ アスペを相手にしたくないので、短く言うが、数学と記号表記の関係と同じ。 >hogeを円周と読むなって話 だから、>>255で、君達はそう言ってるんだろ、と言っただろ。よく読め 259 名前：デフォルトの名無しさん [2013/10/16(水) 09:55:30.15 .net] >>253 >Cは未定義動作や実装依存があるから それは細かいことではないか。それに、未定義の所は使わければよいし、実装依存ならその実装に従えばよいし >>254 >それじゃエクセル方眼紙も形式仕様かよw 方眼紙だけだと何もない形式仕様ということになるね 260 名前：デフォルトの名無しさん [2013/10/16(水) 10:01:36.85 .net] >>257 なんの限定もついていない形式手法について話してるつもりだが？ しかも言ってることは、「記号操作が本質なのじゃないよ」ということだけ 261 名前：デフォルトの名無しさん [2013/10/16(水) 10:07:55.75 .net] >>256 >hogeを円周と読むなって話 そんならそもそもお前は何を書いているんだという話 262 名前：デフォルトの名無しさん mailto:sage [2013/10/16(水) 11:28:01.88 .net] >>260 "制限文法" "仕様記述" でggrks 263 名前：デフォルトの名無しさん mailto:sage [2013/10/16(水) 11:28:49.24 .net] >>259 それを「細かいこと」なんて言う人が 形式手法に何の用があるんだい？あほ？ 264 名前：デフォルトの名無しさん [2013/10/16(水) 19:10:23.13 .net] >>263 アスペの上に、言葉づかいの癖から見てクズのようだからもう相手しないが >それを「細かいこと」なんて言う人が それが細かくない（本質的である）と思っているということは、君は未定義動作や実装依存をなくせばＣのソースも形式仕様だと言うんだな それから、形式的ということと細かいということは同じことではないんだよ 265 名前：デフォルトの名無しさん mailto:sage [2013/10/16(水) 20:28:23.99 .net] >>264のロジックが崩壊している件ww 266 名前：デフォルトの名無しさん mailto:sage [2013/10/16(水) 21:27:26.11 .net] まずJavascriptで書きます。 次に実行します。 ここでエラーが出たら間違いがあるということです。 正しく実行できたら正しく実行できるということです。 267 名前：デフォルトの名無しさん mailto:sage [2013/10/16(水) 23:00:58.62 .net] なんというトートロジー エラーが出なくても正しいとは限らないのは>>212で言われているとおり 268 名前：デフォルトの名無しさん mailto:sage [2013/10/17(木) 13:29:16.40 .net] >>264 >それが細かくない（本質的である）と思っているということは、 この前提から > 君は未定義動作や実装依存をなくせばＣのソースも形式仕様だと言うんだな こんな帰結を導出する人には、形式手法は無理です。（きっぱり 269 名前：デフォルトの名無しさん mailto:sage [2013/12/19(木) 10:09:23.66 .net] Alloyの本を読んで容易に理解できるには、前提知識として何が必要ですか？ このブログ d.hatena.ne.jp/rabbit2go/20110802/1312252092 でも初心者だが容易に理解できたとあるが、私は読んでもさっぱりわかりません。。。 270 名前：デフォルトの名無しさん mailto:sage [2014/04/04(金) 18:04:17.82 ID:cQ9GUWm/.net] 佐原伸 @donkeyshin: ちゅうか、機関銃買ってレイシスト撃ち こrしたくなるので米国ボイコット^_^ RT @tomooda: まあそうなんだけど、USAもユートピアとはほど遠い。全体主義も吹き荒れるし，雇用だって安定しないくせに階層間の流動性は日本以上に低い。レガシーとしか言いようがない古く非合理的な。 271 名前：デフォルトの名無しさん mailto:sage [2015/04/28(火) 23:15:25.31 ID:8LxH1Yrp.net] 久しぶりに来たが、超過疎ってるなｗ 形式仕様なんてどれもクソだって分かったかｗ 272 名前：デフォルトの名無しさん mailto:sage [2015/04/29(水) 02:03:55.33 ID:kKwn8j7I.net] クソではないよ 適用分野がとっくに収束してて適用分野も枯れてる 誰も語る事がなくなっただけだ 273 名前：デフォルトの名無しさん mailto:sage [2015/04/29(水) 06:15:54.81 ID:f54jgqM7.net] 質問もないから新しく始める人もいないってことだろうな。 274 名前：デフォルトの名無しさん mailto:sage [2015/04/29(水) 08:30:09.47 ID:JCD1NrNA.net] >>272　>>273 歯切れが悪くて何を言ってるか分からんが、 もうオワタ、でオーケー？何も残さんで 275 名前：デフォルトの名無しさん mailto:sage [2015/04/29(水) 11:04:46.37 ID:mWtY0FPp.net] 形式仕様なんてどれもクソだが クソ未満の非形式仕様が溢れかえっている喜劇 >>271 ミューテックスとセマフォの違いって排他制御の「実装」レベルの話なんじゃ 例えばデッドロックを回避する機構を入れたいなら そういうコードを書かなきゃいけない ミューテックスの一般的と言えるような実装がない以上 promelaでの一般的な記述もないような 余計なお世話かも知れんが モデル検査は排他制御のあるシステムの検証には適しているといえるけど それは排他制御を抽象化しての話 排他制御自体の検証には向いていないと思う 276 名前：デフォルトの名無しさん [2015/04/29(水) 12:43:37.44 ID:JCD1NrNA.net] >>275 結局ソフトウェアエンジニアリングがクソだと言ったか？ｗ > それは排他制御を抽象化しての話 > 排他制御自体の検証には向いていないと思う これは何言ってる？ 277 名前：デフォルトの名無しさん mailto:sage [2015/04/29(水) 13:07:57.19 ID:f54jgqM7.net] >>271の問題はまさにそこのところ、モデルと実際のプログラムをどう対応付けるかなんだろう。 VDMが実際の開発に導入されている話は聞くがAlloyについてはあまり聞かないのは やはり抽象度のギャップの要因が大きいように思う。 278 名前：デフォルトの名無しさん mailto:sage [2015/04/29(水) 21:37:39.89 ID:JCD1NrNA.net] >>277 抽象度のギャップは大きいほどいいじゃないか 279 名前：デフォルトの名無しさん mailto:sage [2015/04/30(木) 06:12:35.13 ID:B1QV8IC2.net] なんで大きいほどいいの？ ギャップ=0で、動くプログラムがそのまま検査できるのが理想じゃないのか。 280 名前：デフォルトの名無しさん mailto:sage [2015/04/30(木) 07:36:41.80 ID:YRFCj/Kr.net] >>279 ん？言葉の違いか？ ギャップってモデルと実際のプログラムの間の抽象度の違いのことじゃないのか？ 281 名前：デフォルトの名無しさん mailto:sage [2015/04/30(木) 07:58:46.50 ID:B1QV8IC2.net] うん、その違いだよ。 抽象度の高いモデルで正しさを証明できたとして、それをもって現実のプログラムの 正しさの証明とするにはギャップは小さいほうがいいと思うが。 書き換えの段階で間違いが入ったらそもそも意味がないし。 ギャップが大きいほどいいとする理由は？ 282 名前：デフォルトの名無しさん mailto:sage [2015/04/30(木) 08:47:12.46 ID:YRFCj/Kr.net] えー！　 極端な場合で考えてみなよ ギャップ＝０ということはモデルの意味がないということだ 283 名前：デフォルトの名無しさん [2015/04/30(木) 09:07:52.87 ID:B1QV8IC2.net] モデルの意味って何ぞ？ >>277の言う現実のプロジェクトではモデルを構築することそれ自体が目的じゃなくて 実際のシステムに誤りがないことを保証したいわけだろう。 モデルはそのための道具でしかない。 284 名前：デフォルトの名無しさん mailto:sage [2015/04/30(木) 10:01:13.28 ID:YRFCj/Kr.net] モデルがなぜそのための道具になりえるとしたら、それはモデルが何だからか考えてみな 285 名前：デフォルトの名無しさん mailto:sage [2015/04/30(木) 10:02:47.56 ID:YRFCj/Kr.net] モデルがそのための道具になりえるとしたら、それはモデルが何だからかを考えてみな 286 名前：デフォルトの名無しさん mailto:sage [2015/04/30(木) 21:17:47.07 ID:B1QV8IC2.net] ここでそういう質問が出るとは思わなかったが、形式手法におけるモデルの意義は 機械的に検証可能であることに尽きるだろう。現実のプログラムではそれが難しいから モデルで代用していると言ってもいい。 たぶんあんたが考える「モデルの意味」は違うんだろうけど、じゃあそれ説明して。 287 名前：デフォルトの名無しさん mailto:sage [2015/05/01(金) 20:46:23.78 ID:mxjbyy1D.net] まぁ色々な側面があると思うけどね 形式手法によって手戻りを低減するには できるだけ早期に検証することが有効で 建前としては仕様が実装に先行するのだから 検証の対象は実装より抽象度が高くなる とはいえギャップが大きすぎるのも実際的ではない だからBやZで言われる段階的詳細化が意味を成す 288 名前：デフォルトの名無しさん mailto:sage [2015/05/01(金) 21:06:27.82 ID:mxjbyy1D.net] 別の大きな側面としては 抽象化しないと現在の計算機・理論ではまともに検証できない というのがある 簡単に言えば状態変数として二値変数が64個あるだけで 状態空間を表現するのにアドレス空間を食いつぶしてしまう 自然数や実数を扱うプログラムをまともに自動検証できるようにするには ハードにせよ計算理論にせよ技術革新が必要 289 名前：デフォルトの名無しさん mailto:sage [2015/05/01(金) 21:07:15.76 ID:mxjbyy1D.net] 勿論「矛盾がない」という検証結果が 実際的な時間・コストで得られないとしても 「矛盾がある」という結果が早期に得られる場合もあるので 計算機ぶん回すのも無意味ではないが それはいわゆる形式手法というより「テスト」の範疇だと思う 290 名前：デフォルトの名無しさん mailto:sage [2015/05/01(金) 23:33:52.21 ID:QsO/fHrg.net] >建前としては仕様が実装に先行するのだから >検証の対象は実装より抽象度が高くなる >抽象化しないと現在の計算機・理論ではまともに検証できない 積極的に抽象化すべき理由じゃなくて単なる結果だな。 291 名前：デフォルトの名無しさん mailto:sage [2015/05/02(土) 00:16:55.31 ID:XhAWgoUD.net] 自然言語の曖昧さの排除という使命がある以上 闇雲に抽象化すればいいってもんでもないだろ さらに言うなら「単なる結果」でない 形式手法を使う積極的理由なんてあるのか？ 292 名前：デフォルトの名無しさん [2015/05/02(土) 09:28:39.94 ID:GIpzT+Qy.net] 皆独り言を言っている。 293 名前：デフォルトの名無しさん [2015/05/02(土) 20:56:44.49 ID:0dQA+dZy.net] どいつもこいつもｗこの分野のやつらはｗ そんなのを抽象化なんて言うから世間から笑われるんだ 単なるアバウトって言うんだよ 294 名前：デフォルトの名無しさん mailto:sage [2015/05/09(土) 05:15:44.76 ID:gLXIswIQ.net] >>293 アバウトなのは、抽象に関するあんたの理解。 295 名前：デフォルトの名無しさん mailto:sage [2015/08/10(月) 08:36:36.39 ID:R/t8P2/U.net] 質問に罵倒なんぞは自然言語でいいが、主張は形式手法言語で書いてくれ。 Event-Bしか読めないけど。 296 名前：デフォルトの名無しさん mailto:sage [2015/08/10(月) 23:38:42.28 ID:8/xPnylN.net] 形式言語で表現できるのは形式的意味でしかなく 主張するところの、いわゆる意味を示すことはできない そして論理的に矛盾の無い主張だからといって有意義とは限らない ここで「偶数+奇数は奇数だ！」と主張したところで スレチとなるだけ ま、自然言語から意味を見出しているのも幻想かもしらんが 297 名前：デフォルトの名無しさん [2015/12/30(水) 12:08:29.72 ID:z2Nurwun.net] Alloyって楽しいな。 コンピュータと対話しながら、記述対象に対する自分の理解を深められるのがとても楽しい。 298 名前：デフォルトの名無しさん mailto:sage [2016/03/03(木) 22:41:34.71 ID:tH72Ij/h.net] test 299 名前：デフォルトの名無しさん [2018/05/23(水) 23:09:57.69 ID:Au5e7VGg.net] 僕の知り合いの知り合いができたパソコン一台でお金持ちになれるやり方 役に立つかもしれません グーグルで検索するといいかも『ネットで稼ぐ方法　モニアレフヌノ』 ZLPAL 300 名前：デフォルトの名無しさん [2018/07/04(水) 22:59:43.98 ID:gFgZc5FG.net] LGL 301 名前：デフォルトの名無しさん mailto:sage [2018/07/06(金) 12:34:31.11 ID:uTPDH9XV.net] ZLPAL

---

---

[ 新着レスの取得/表示 (agate) ] / [ 携帯版 ]

read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef