【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

**デフォルトの名無しさん** · 2013/01/05(土) 21:33:15.76

このスレッドは天才チンパンジー「アイちゃん」が
言語訓練のために立てたものです。

アイと研究員とのやり取りに利用するスレッドなので、
関係者以外は書きこまないで下さい。

　　　　　　　　　　　　　　　　　　京都大学霊長類研究所

**デフォルトの名無しさん** · 2013/01/06(日) 01:05:45.32

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

**デフォルトの名無しさん** · 2013/01/06(日) 01:16:08.51

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

**デフォルトの名無しさん** · 2013/01/06(日) 01:23:51.63

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

第2回・第1回へのリンク有

**デフォルトの名無しさん** · 2013/01/08(火) 01:54:13.02

特許庁の新システム入札やり直すらしいけど
ああいうのこそ形式手法を適用する意義がありそうなものだが

形式手法によってデスマが回避できるというよりは
デスマを回避できる体力があるから形式手法を採用できるってのが
実際なのかもしらん

**デフォルトの名無しさん** · 2013/01/08(火) 06:49:04.96

Alloyの本

抽象によるソフトウェア設計－Alloyではじめる形式手法－
http://www.amazon.co.jp/dp/4274068587

形式手法の本

形式手法入門―ロジックによるソフトウェア設計―
http://www.amazon.co.jp/dp/4274211886/

**デフォルトの名無しさん** · 2013/01/11(金) 06:24:10.24

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

**デフォルトの名無しさん** · 2013/01/11(金) 06:27:52.78

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

**デフォルトの名無しさん** · 2013/01/11(金) 22:54:26.79

あきらめたというかフェードアウトした感じかな
たしか半分くらいまでは読んだけど、いつの間にか
読むのをやめてた

形式手法はまったくの素人だったので（今も）
よく分からんかった

**デフォルトの名無しさん** · 2013/01/17(木) 10:49:33.93

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

**デフォルトの名無しさん** · 2013/01/18(金) 03:26:26.90

国内だと人材が少ない（しかも学術寄りの人の方が多い）
ってのは実感としてある

形式手法は静的解析のツールとして利用される道の方が明るい気がする
人間が読み書きする形式言語が使い物になる日は来ないと思う

**デフォルトの名無しさん** · 2013/01/18(金) 17:38:42.62

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

**デフォルトの名無しさん** · 2013/01/18(金) 19:43:02.15

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

**デフォルトの名無しさん** · 2013/01/19(土) 00:19:45.43

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

**デフォルトの名無しさん** · 2013/01/19(土) 01:08:35.95

費用や納期だけで評価したら大差ないってことでしょ

現状ソフトウェアの品質を正当に評価していない（できない）から
形式手法を導入するインセンティブが働かない

てかageる必要あんのか？

**デフォルトの名無しさん** · 2013/01/19(土) 01:18:12.83

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

**デフォルトの名無しさん** · 2013/01/19(土) 12:16:55.38

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

**デフォルトの名無しさん** · 2013/01/19(土) 13:05:09.39

>>18
論文と現場の乖離を示唆しながら
>品質は費用納期に反映される
はねぇだろ

営業や契約担当じゃないから実態は知らないが
発注元は
「フィールドバグ○件以下。超過した場合は違約金！」
とか契約文書に書けるの？

逆に請負側（候補）は
形式手法の適用が要件に入っていない案件で
「我が社は形式手法を導入しているのでちょっといいお値段です！」
で競争に勝てるというの？

「我が社で納期が短縮できるのは形式手法で開発の手戻りを低減するからです！
品質下げる訳じゃありません！」
とか発注元に説明すんの？

**デフォルトの名無しさん** · 2013/01/19(土) 13:53:26.32

>>19

>「フィールドバグ○件以下。超過した場合は違約金！」
>とか契約文書に書けるの？
そりゃ書ける場合もあるよ。
それに、バグが多いと、当然後の注文もなくなってくるだろ。

>「我が社は形式手法を導入しているのでちょっといいお値段です！」
それは、顧客にとってのメリットを言っていないので、その時点でダメだよ。

>「我が社で納期が短縮できるのは形式手法で開発の手戻りを低減するからです>！品質下げる訳じゃありません！」とか発注元に説明すんの？
黙って短い納期でやればいいだけだろ。それは顧客にとってメリットだし、
こっちも短くなった分、他の仕事ができるし。

ほんとに使える形式手法とはこういうものなんだよ。

**デフォルトの名無しさん** · 2013/01/19(土) 14:57:17.31

話が通じていないな

・ソフトウェアの品質を規定する統一的な指標がない
・既存の品質指標は開発手法に依存することが多い
　（形式手法を適用した場合としない場合の公平な比較が困難）
・形式手法を要件に入れると対応できる業者が制限される

このため形式手法を導入するメリットが明確な「発注」がそもそも少ない
（メリットが明確なセーフティクリティカルやミッションクリティカルな案件では
現状でも形式手法が成果を上げている）

潜在的需要があっても表面上需要が無ければ
請負側に働く形式手法導入のインセンティブは弱い

**デフォルトの名無しさん** · 2013/01/19(土) 15:15:19.07

請負側としては

同じ業者から大きな案件を頻繁に受注するケースは少ない
評判に期待して今回頑張っても次回の受注がいつなのかは分からない

いつ効果が表れるか不明確な投資はやりにくい
業界全体で評判になるほどの成果を上げるのは体力に余裕がないとできない

しかも形式手法が扱える業者は多くないが
形式手法だけで需要を独占できるほどの特殊性はない

**デフォルトの名無しさん** · 2013/01/19(土) 15:23:25.33

請負側開発者・マネージャとしては

形式手法によりコストや納期を圧縮できるかもしれないが
勉強やらに費やした分だけ自分の給与が上がる保証はない

訳のわからない仕様書から解放されるといった
現場の幸せを要求しても経営判断には反映されにくい

**デフォルトの名無しさん** · 2013/01/19(土) 15:44:33.85

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

**デフォルトの名無しさん** · 2013/01/19(土) 16:08:35.77

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

**デフォルトの名無しさん** · 2013/01/19(土) 19:06:51.37

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

**デフォルトの名無しさん** · 2013/01/19(土) 19:55:52.90

形式手法は商習慣まで関知せんよ

発注側「こういうもの作って」→受注側「言われたものを作りました」
という関係がものづくりとしては自然に思えるが
日本のICT業界は往々にしてこうはなっていない

上流で形式仕様を作成する場合
ユーザ企業はまずコンサル会社や大手ベンダに
「形式仕様作成と検証」といった発注を出すんじゃないかな
特に日本の場合は要求分析もセットになるかもしれない

**デフォルトの名無しさん** · 2013/01/19(土) 20:55:25.43

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

**デフォルトの名無しさん** · 2013/01/20(日) 18:35:51.46

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

**デフォルトの名無しさん** · 2013/01/20(日) 23:53:12.74

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

**デフォルトの名無しさん** · 2013/01/22(火) 23:33:47.71

シンタックスはともかくセマンティクスにおいて
VDM++のまともな仕様って無いの？
曖昧さを持った言語で形式仕様記述とか欺瞞じゃね？

VDM-10のVDM++のが
枠組みはしっかりしてるけど事実上使えないし
Overture界隈はVDM-RTに傾倒してる感じだし
何かみんなおでこ広いし

**デフォルトの名無しさん** · 2013/01/26(土) 00:09:26.58

>>13
> >人間が読み書きする形式言語
> >使い物になる日は来ないと思う
> そんなことはない。一流人材が参戦すれば変わる。

その一流の人材が膨大な人数どうやって確保するの？
形式仕様言語でフルに仕様を書けばプログラムコードと同じオーダーの行数になるという経験則がある。
つまり数人で作れるおもちゃのソフトウェアならともかく、社会の根幹を支えそれが故に信頼性が必須とされる
大きなソフトウェアは現在の大規模開発でプログラミングに関わってる膨大な人数と同じオーダーの
形式仕様記述者が必要になるってことだ。

それだけ莫大な人数のそんな高い質の人材が世界のどこにいるんだい？
寝言は寝てから言った方がいいよ。

それに数人のプロジェクトに限定しても、それを一流の人材で仕様記述しても
それで作られたソフトウェアの寿命がある間は、そいつのメンテナンスのために
ずっと一流の人材を貼りつけておかないと、彼らが書いた形式仕様なんて難しいものは
２流の人材じゃ読み書きできないから保守できないよね。ってことで一流の人材ほど
彼らが書いた仕様のお守をさせられて他の仕事ができなくなる。

これって素晴らしい才能の無駄遣い法だね。

**デフォルトの名無しさん** · 2013/01/26(土) 12:32:30.58

一流の人材を活用するとしたら
二流・三流の人が使える形式手法の技術を確立することだろうね

そういう意味では一流の人材は既に集まっている
ただ二流・三流が何たるかを理解できていない可能性はある

**デフォルトの名無しさん** · 2013/01/26(土) 19:14:58.59

用語定義で「名前： 2chに書き込むときの名前」てなこと書いておきながら
本編に「家で飼っているぬこの名前は～」
とかしれっと書く奴はメタメタにしてやんよ！

軽量形式手法なんて形式手法じゃねぇと思ってたが
名を捨てて実を取ることも必要だと感じた。

**デフォルトの名無しさん** · 2013/01/27(日) 23:46:08.13

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

**デフォルトの名無しさん** · 2013/01/28(月) 01:17:16.05

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

ならば、形式仕様でフルに仕様記述するのが現実に可能だと主張したいのならば、
今のクソのでない形式仕様言語を現実に作ってからにしろ。

現実に存在しない夢のような形式仕様言語の存在を前提として>>13を主張するのは
単なる精神病患者だよ、誇大妄想と言う名前のな。

形式仕様屋にはこの手の誇大妄想患者が多すぎる。だから信用をなくして来たんだよ。

**デフォルトの名無しさん** · 2013/01/28(月) 01:22:14.84

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