- 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
- 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]
- 【会社の即戦力の定義とは】
「社会の一員として人々の役に立つ価値を提供すること」 会社にとって喉から手が出る程欲しい人材とは、 この求められる価値を提供するために、解決すべき 課題を正しく共有し、一緒になって価値を生み出す ことが出来る人材なのです。 ところがJALグランドサービスの即戦力って言っている奴らは自分の気の合う人には仲良くするけど 気に入らない人間には粘着してとことんまで罵倒したりパワハラしたり自分にはとことん甘いくせに人の揚げ足ばかり探して 仕事中も喋ってばかりで口元緩んでばかりじゃないか 先に暴言を吐けば自分が強いと思わせることができるなんて考えているみたいだけどそれは違う それは弱い動物がキャンキャン吼えているのと同じことだよ JALグランドサービスは仲良しクラブ会社 仕事中 趣味の話で盛り上がって手が止まってんだよw たまには仕事まじめにやったらどうだね?
- 239 名前:デフォルトの名無しさん [2013/10/11(金) 22:32:05.51 .net]
- JALグランドサービスは貧乏性でテーブル拭いて汚れたタオルを次の清掃場所
さらに次の清掃場所にもっていって汚れたタオルを使えっていってきた タオルからはなんともいえない臭いが漂い色もケチャップやなんやらがこびりついていて汚かった お客さまのためにを毎日言っている会社なのになにこれ? 矛盾してるよね? 青タオルはウンコがこびりついていて汚い それをキレイなタオルといいラバーのほかギャレー 床のゲロ掃除などさまざまなところで活用している バケツにそのタオルを濡らすとき気持ちが悪い バケツもすごく汚いよね バケツ洗っているところみたことがないし JALはこんな会社です 白タオルは生乾きで蒸れた悪臭がしている それでお客様がつかうテーブルを拭いているんだから あのテーブルは菌をひろげているようなもんだ
- 240 名前:デフォルトの名無しさん [2013/10/11(金) 22:32:50.46 .net]
- JALグランドサービスはパートやアルバイト、契約社員に対し若い正社員ですら横柄かつ高圧的な言動(恫喝行為など)を取ることが常態化されていて
それを正せる上司が一人もいないというのが特徴の会社
- 241 名前:デフォルトの名無しさん [2013/10/11(金) 22:33:27.02 .net]
- 人が見えにくい場所で係長がとある気弱な社員のわき腹を殴ったり
蹴っ飛ばしたり頭を殴ったりしていた あれをパワハラといわずになんていうのか? こんな屑なことばかりやっている悪質な会社JALの傘のなかでふんぞり返っているのだから JALそのものがたいしたことがないといえるだろう 班長 係長 課長とも人間としての品格を疑うことがおおい 常軌を逸した行動を認知していながらそれを容認しているJALグランドサービス フィロソフィなどただ毎日口にだして読んでればそれで満たされる ただそれだけのもの どんなりっぱな言葉を並べたとこでそれを毎日読んでる人間が バカじゃ意味がない 陵辱 ひとの足をひっぱったり人を不幸にしている JALグランドサービスが物心両面の幸せだと? 笑わせるなw クズ会社がw
- 242 名前:デフォルトの名無しさん [2013/10/11(金) 22:34:12.22 .net]
- ロッカーの一番奥の壁を誰かが蹴っ飛ばしたのかなんだかわからないけど
大きな穴があいて破損させた馬鹿がいたよね? 犯人つかまったの? あれだけの穴があいていて音が聞こえなかったなんておかしいよね? こんな不祥事はこの会社しかないだろうしあれだけ人が多いロッカーで誰も気がつかないのもこの会社だけw アホJALグランドサービスw
- 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 >仕様を書く人は誤解を生まないように気を付けた方が良いし >仕様を読む人は思い込みをしないように気を付けた方が良い 随分ぬるいがwまあそういうことだ。記号病達にはこれも伝わらないのじゃないかな
- 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
アスペの上に、言葉づかいの癖から見てクズのようだからもう相手しないが >それを「細かいこと」なんて言う人が それが細かくない(本質的である)と思っているということは、君は未定義動作や実装依存をなくせばCのソースも形式仕様だと言うんだな それから、形式的ということと細かいということは同じことではないんだよ
- 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
>それが細かくない(本質的である)と思っているということは、 この前提から > 君は未定義動作や実装依存をなくせばCのソースも形式仕様だと言うんだな こんな帰結を導出する人には、形式手法は無理です。(きっぱり
- 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]
- 久しぶりに来たが、超過疎ってるなw
形式仕様なんてどれもクソだって分かったかw
- 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
結局ソフトウェアエンジニアリングがクソだと言ったか?w > それは排他制御を抽象化しての話 > 排他制御自体の検証には向いていないと思う これは何言ってる?
- 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]
- えー!
極端な場合で考えてみなよ ギャップ=0ということはモデルの意味がないということだ
- 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]
- どいつもこいつもwこの分野のやつらはw
そんなのを抽象化なんて言うから世間から笑われるんだ 単なるアバウトって言うんだよ
- 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
|

|