- 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
- 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]
- モデルがなぜそのための道具になりえるとしたら、それはモデルが何だからか考えてみな
|
 |
