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

1 ：2013/01/05 〜 最終レス ：2013/09/16

スレがないので立ててみた
参考ページ
http://en.wikipedia.org/wiki/Formal_methods
http://ja.wikipedia.org/wiki/%E5%BD%A2%E5%BC%8F%E6%89%8B%E6%B3%95

2 ：

このスレッドは天才チンパンジー「アイちゃん」が
言語訓練のために立てたものです。
アイと研究員とのやり取りに利用するスレッドなので、
関係者以外は書きこまないで下さい。
　　　　　　　　　　　　　　　　　　京都大学霊長類研究所

3 ：

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

4 ：

ついでだから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

5 ：

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

6 ：

特許庁の新システム入札やり直すらしいけど
ああいうのこそ形式手法を適用する意義がありそうなものだが
形式手法によってデスマが回避できるというよりは
デスマを回避できる体力があるから形式手法を採用できるってのが
実際なのかもしらん

7 ：

Alloyの本
抽象によるソフトウェア設計−Alloyではじめる形式手法−
http://www.amazon.co.jp/dp/4274068587
形式手法の本
形式手法入門―ロジックによるソフトウェア設計―
http://www.amazon.co.jp/dp/4274211886/

8 ：

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

9 ：

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

10 ：

あきらめたというかフェードアウトした感じかな
たしか半分くらいまでは読んだけど、いつの間にか
読むのをやめてた
形式手法はまったくの素人だったので（今も）
よく分からんかった

11 ：

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

12 ：

国内だと人材が少ない（しかも学術寄りの人の方が多い）
ってのは実感としてある
形式手法は静的解析のツールとして利用される道の方が明るい気がする
人間が読み書きする形式言語が使い物になる日は来ないと思う

13 ：

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

14 ：

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

15 ：

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

16 ：

費用や納期だけで評価したら大差ないってことでしょ
現状ソフトウェアの品質を正当に評価していない（できない）から
形式手法を導入するインセンティブが働かない
てかageる必要あんのか？

17 ：

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

18 ：

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

19 ：

>>18
論文と現場の乖離を示唆しながら
>品質は費用納期に反映される
はねぇだろ
営業や契約担当じゃないから実態は知らないが
発注元は
「フィールドバグ○件以下。超過した場合は違約金！」
とか契約文書に書けるの？
逆に請負側（候補）は
形式手法の適用が要件に入っていない案件で
「我が社は形式手法を導入しているのでちょっといいお値段です！」
で競争に勝てるというの？
「我が社で納期が短縮できるのは形式手法で開発の手戻りを低減するからです！
品質下げる訳じゃありません！」
とか発注元に説明すんの？

20 ：

>>19
>「フィールドバグ○件以下。超過した場合は違約金！」
>とか契約文書に書けるの？
そりゃ書ける場合もあるよ。
それに、バグが多いと、当然後の注文もなくなってくるだろ。
>「我が社は形式手法を導入しているのでちょっといいお値段です！」
それは、顧客にとってのメリットを言っていないので、その時点でダメだよ。
>「我が社で納期が短縮できるのは形式手法で開発の手戻りを低減するからです>！品質下げる訳じゃありません！」とか発注元に説明すんの？
黙って短い納期でやればいいだけだろ。それは顧客にとってメリットだし、
こっちも短くなった分、他の仕事ができるし。
ほんとに使える形式手法とはこういうものなんだよ。

21 ：

話が通じていないな
・ソフトウェアの品質を規定する統一的な指標がない
・既存の品質指標は開発手法に依存することが多い
　（形式手法を適用した場合としない場合の公平な比較が困難）
・形式手法を要件に入れると対応できる業者が制限される
このため形式手法を導入するメリットが明確な「発注」がそもそも少ない
（メリットが明確なセーフティクリティカルやミッションクリティカルな案件では
現状でも形式手法が成果を上げている）
潜在的需要があっても表面上需要が無ければ
請負側に働く形式手法導入のインセンティブは弱い

22 ：

請負側としては
同じ業者から大きな案件を頻繁に受注するケースは少ない
評判に期待して今回頑張っても次回の受注がいつなのかは分からない
いつ効果が表れるか不明確な投資はやりにくい
業界全体で評判になるほどの成果を上げるのは体力に余裕がないとできない
しかも形式手法が扱える業者は多くないが
形式手法だけで需要を独占できるほどの特殊性はない

23 ：

請負側開発者・マネージャとしては
形式手法によりコストや納期を圧縮できるかもしれないが
勉強やらに費やした分だけ自分の給与が上がる保証はない
訳のわからない仕様書から解放されるといった
現場の幸せを要求しても経営判断には反映されにくい

24 ：

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

25 ：

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

26 ：

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

27 ：

形式手法は商習慣まで関知せんよ
発注側「こういうもの作って」→受注側「言われたものを作りました」
という関係がものづくりとしては自然に思えるが
日本のICT業界は往々にしてこうはなっていない
上流で形式仕様を作成する場合
ユーザ企業はまずコンサル会社や大手ベンダに
「形式仕様作成と検証」といった発注を出すんじゃないかな
特に日本の場合は要求分析もセットになるかもしれない

28 ：

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

29 ：

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

30 ：

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

31 ：

シンタックスはともかくセマンティクスにおいて
VDM++のまともな仕様って無いの？
曖昧さを持った言語で形式仕様記述とか欺瞞じゃね？
VDM-10のVDM++のが
枠組みはしっかりしてるけど事実上使えないし
Overture界隈はVDM-RTに傾倒してる感じだし
何かみんなおでこ広いし

32 ：

>>13
> >人間が読み書きする形式言語
> >使い物になる日は来ないと思う
> そんなことはない。一流人材が参戦すれば変わる。
その一流の人材が膨大な人数どうやって確保するの？
形式仕様言語でフルに仕様を書けばプログラムコードと同じオーダーの行数になるという経験則がある。
つまり数人で作れるおもちゃのソフトウェアならともかく、社会の根幹を支えそれが故に信頼性が必須とされる
大きなソフトウェアは現在の大規模開発でプログラミングに関わってる膨大な人数と同じオーダーの
形式仕様記述者が必要になるってことだ。
それだけ莫大な人数のそんな高い質の人材が世界のどこにいるんだい？
寝言は寝てから言った方がいいよ。
それに数人のプロジェクトに限定しても、それを一流の人材で仕様記述しても
それで作られたソフトウェアの寿命がある間は、そいつのメンテナンスのために
ずっと一流の人材を貼りつけておかないと、彼らが書いた形式仕様なんて難しいものは
２流の人材じゃ読み書きできないから保守できないよね。ってことで一流の人材ほど
彼らが書いた仕様のお守をさせられて他の仕事ができなくなる。
これって素晴らしい才能の無駄遣い法だね。

33 ：

一流の人材を活用するとしたら
二流・三流の人が使える形式手法の技術を確立することだろうね
そういう意味では一流の人材は既に集まっている
ただ二流・三流が何たるかを理解できていない可能性はある

34 ：

用語定義で「名前： 2chに書き込むときの名前」てなこと書いておきながら
本編に「家で飼っているぬこの名前は〜」
とかしれっと書く奴はメタメタにしてやんよ！
軽量形式手法なんて形式手法じゃねぇと思ってたが
名を捨てて実を取ることも必要だと感じた。

35 ：

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

36 ：

>>35
> >>32
> >形式仕様言語でフルに仕様を書けばプログラムコードと同じオーダーの行数に
> >なるという経験則がある。
> だからあ！そういう今の形式仕様言語が糞なんだよお！まだ分からんのかあ！
ならば、形式仕様でフルに仕様記述するのが現実に可能だと主張したいのならば、
今のクソのでない形式仕様言語を現実に作ってからにしろ。
現実に存在しない夢のような形式仕様言語の存在を前提として>>13を主張するのは
単なる精神病患者だよ、誇大妄想と言う名前のな。
形式仕様屋にはこの手の誇大妄想患者が多すぎる。だから信用をなくして来たんだよ。

37 ：

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

38 ：

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

39 ：

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

40 ：

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

41 ：

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

42 ：

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

43 ：

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

44 ：

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

45 ：

フルフル君でもそれに噛みついている人でもないが
記述量は確かに実用上の課題ではあるけども
プログラムコードと同じオーダーなら駄目で短いならOKって
単純な話ではないと思うんだが
自然言語による仕様書の記述・検証の工数を無視しているのは意図的か？
それに形式的検証まで含むか否かで大きく変わる
証明された信頼性とテストによる確率的な信頼性は比較できない
自動コード生成が可能かどうかでも大きく変わる

46 ：

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

47 ：

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

48 ：

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

49 ：

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

50 ：

>>49
目的が違う
実際のところ言語やターゲットとなる案件によっては
プログラミング言語でも仕様記述は不可能ではないし
仕様記述言語で実行可能なコードを書くこともできる
道具として両者を近づける試みも多数なされているが
仕様と実装をごっちゃにしようという話ではない
あくまで仕様と実装は別の概念

51 ：

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

52 ：

曖昧だったり矛盾を含んだりしている
自然言語の仕様書が幅を利かせすぎという面もある
世の中の仕様書が如何にいい加減か実感できるという点だけでも
形式的仕様記述を「体験」する意義は十分だと思うね

53 ：

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

54 ：

>>53
形式的仕様が誰かor何かに満足してもらえる
なんて話はしていないと思うんだが
意図的なのか読解力がないのか分からんが
Rーなら一人でやってくれ
他人を使うな

55 ：

>>53
>形式的仕様ってその程度で満足してもらえるんだ。進まんはずだ。
ほら、この日本語文1つ取っても書いた本人以外には意味不明だろ？

56 ：

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

57 ：

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

58 ：

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

59 ：

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

60 ：

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

61 ：

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

62 ：

>>61
お望みのレベルに達していないだろうけど
テスト自動生成なら既に実施例や商品があるよ
産総研でも研究してたはず
モデル検査でSATソルバ使うのが流行ってるっぽいんで
テストケース生成技術・ツールはもう少し発展しそう
形式手法ではないがテストを仕様に近づけるというアプローチでBDDというのもある
ただC++で使いやすいフレームワークは知らない

63 ：

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

64 ：

とりあえずinv, pre, postで十分に制約がかけられているんなら
関数・操作の中身が実装と異なっても問題ないんじゃね
あとは使い方次第としか
そのフレームワークの特性にも依存するし

65 ：

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

66 ：

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

67 ：

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

68 ：

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

69 ：

SIL4クラスの安全にかかわる案件に絡んでいるが
優秀な人間が何人も集まって検討した仕様にすら穴がある
これはもう自然言語でやっている限りどうにもならないだろう
現状の形式手法では十分なソリューションたりえないのも事実だが
期待できるのは形式手法くらいしかないのも事実だ
現状が駄目だからといって将来が絶たれてよい技術ではない

70 ：

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

71 ：

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

72 ：

>現状の形式手法では十分なソリューションたりえないのも事実だが
>期待できるのは形式手法くらいしかないのも事実だ
そうなんだが、あまりに不満足な現状だとはおもわんか？

73 ：

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

74 ：

テストしにくいコードをテストする方法教えて下さい
http://toro.2ch.net/test/read.cgi/tech/1334408391/
でテストケースの自動生成で賑わってるけど同じ人？

75 ：

2chなんかでクダ巻いて形式手法を批判した気になってるような低能は
そもそもVDMやAlloyを始めることすらしないからじゃないかな

76 ：

>>75
おまえは家来か

77 ：

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

78 ：

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

79 ：

>>77
そもそもふつうに思いつかんようなのがよいモデル化かな？
キャッシュメモリってどんな例題だったけ
ちょっと見てみるかな

80 ：

業務ロジックを仕様記述言語で書くことは可能かな？
なんか、例を見てると並列処理の時の云々かんぬんとかかなりアルゴリズム的だったり、詳細よりだったりする例が多いのが気になる。
仕様のバグで一番多いのは論理矛盾だったりするので、
その辺が検出できそうなら導入してみたいんだよね。

81 ：

業務ロジックがどういうものか知らないけど仕様記述自体はできると思うよ
ただ形式仕様記述ができることと
論理矛盾の検出ができることの間には大きな隔たりがあるのが現状
状態の数が限られているならなんとかなるけど
状態変数に実数とか時間を持つとなると途端に検証が困難になる

82 ：

おお、そうなんだ。サンクス。
あんまりたいそうなロジックを扱ってるわけじゃないけど
取引ができる日がn日からm日で、そのうち取引ができるのはステータスがxの人で...
とか、まあ、そういったものの組み合わせが多いかな。
最悪、論理矛盾の自動検出が出来なくても、曖昧性の無い記述ができるなら
仕様漏れとかが減ったりしないかなぁ。

83 ：

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

84 ：

組込みっていうか車載開発（ボディ系）でAlloyを個人的に使おうと思ったが、
難しくて挫折しそうになった。。。C言語しか知らないとつらい。。。

85 ：

>>84
組込み系であれば、(Alloy/VDM/Zなどよりも)
「振る舞い」の検証を重視するCSPやCCSのほうが
(多くのケースでは)適しているのではないかと思われ
もしもこれら形式的記述スタイルに慣れていないのなら、
PROMELA(およびその処理系であるSPIN)はいかが？
C言語とステートマシンの知識があれば、直感で理解できる
最近は、PROMELA/SPINに関する日本語書籍もいくつかあるよ

86 ：

アドバイスありがとうございました。
積読状態ですが、VDMにAlloyにSPINに書籍は購入済みですので、
一度読んでみます。
Alloyに手を出したのは、VDMやSPINの両方のおいしいところを合わせたのと、
手軽にモデリングできると聞いたからです。
・・・でも私には簡単ではなかったorz

87 ：

世界的には業務ロジックの構築=DSL(ドメイン記述言語)の流れじゃなかったけ。

88 ：

DSLと形式手法は普通に両立すると思うが？

89 ：

Rodinはまともなチュートリアルないんか。
Event Bの理論は本読んでどうにかするとして、ツールとしてのRodinの使い方が公式のチュートリアル見てもよくわからん。

90 ：

Code Contractsはこのスレの範疇？

91 ：

いいんじゃね？

92 ：

形式手法が実用にならないと言われる中で
Code Contractsは計算機科学とソフトウェア工学の中庸にあると思うけど
あんまり話題にならないね
Code Contracts目当てにProfessional買うことはないだろうから
Express Editionにも対応してくれればいいのに

93 ：

乞食と思われると残念だから補足するけど
利用するライブラリが契約されてないと利用者側が馬鹿を見るので
みんな契約すればいいのに！的な意味で

94 ：

C++1yではConcepts復活すんのかな

95 ：

prologじゃダメなの？（DSLも含めて）

96 ：

>>95
そうね。少なくともDSLを記述して実行させるくらいなら
最初からPrologで書いてしまった方が気が利いていますね。

97 ：

Prologで書かれた仕様を実装に落とし込むのは
自然言語で書かれた仕様を実装に落とし込む時とは
別の危うさがあるように思える
バックエンドに使うんなら何でもいいけど

98 ：

具体化prz

99 ：

？

100read 1read

1read 100read
TOP カテ一覧 スレ一覧 2ch元 削除依頼 ▲

COM (386)
C++によるDICOMファイル解析 (184)
関数型言語ML (SML, OCaml, etc.), Part 6 (713)
ニートの俺が何か開発して食いつなぐスレ (979)
Regular Expression(正規表現) Part11 (523)
GCCについて part10 (354)
--log9.info------------------
【福岡から】九州・沖縄のＱＭＡ事情20【沖縄まで】 (279)
滋賀のゲーセン事情 (793)
三重県のゲーセン事情36 (322)
宮城のQMA事情 その6 (512)
名古屋(東海地方)スレpart36 (866)
香川の音ゲー事情8 (940)
【新潟市内】万代シティ・古町近辺のゲームセンター (960)
ふぁんとむ湾岸最凶自演伝説 (219)
ROUND1枚方店 2ゲーム目 (211)
札幌ゲーセン事情　PART19 (285)
石川ゲーセン事情 Part22 (686)
｛まったり｝大分ゲーセン情事 7｛ゆったり｝ (124)
姫路・加古川のゲーセン事情Part9 (161)
立川のゲーセン事情17 (492)
五反田★アムネット (326)
【埼玉】大宮のゲームセンター事情 (114)
--log55.com------------------
【ちかなん】高海千歌×松浦果南スレPart.1【お姉さんと妹】
桜坂しずく演劇教室 3.5舞台目
「果南×善子」って中々良いな…
穂乃果「GOHANYA新装開店の巻」
エマ・ヴェルデちゃんはBuono！かわいい！パンの耳4本目だよ〜！
【逢田梨香子】桜内梨子ちゃん大好きスレ【りきゃこ】Part12.9
/cV^_V^Vトッリ冷えてますか〜!!????(・8・)？こたつ出したちゅんよ？
スクスタのUR排出5%って絶対嘘だろ