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