【Alloy】形式言語による仕様記述【VDM】
■ このスレッドは過去ログ倉庫に格納されています
>>100 >>133 >>137 この人センスいいねえ >>111 >>136 この人は単なる学習者 へー(ニヤニヤ Zの言語仕様がデカいと思っている人のセンスがいいとか言うのって 本人以外考えられないけどw で、Zの言語仕様のどこがデカいわけ? ぼくちゃん学習者なんで教えてくださいませ〜 >>152 単一化と導出・融合だけの pure Prolog に較べると途方もなく大きいのではないか。 Zの言語仕様には単一化もレゾリューションもNAFもないよ。 どうして実行機構を持たないZのほうが言語仕様がデカいと思うんだい? 言語仕様の大きさは 処理系やツールを実装する人にとっては重要かもしれないけど ユーザにとっては重要じゃないよね。 何ができるか・何をしないといけないかが重要。 そしてそれは言語仕様の大きさと必ずしも対応しない。 言語仕様の大きさで議論しようというのがそもそも筋が悪い。 言語仕様を全部把握していないと使えない訳じゃあるまい。 その>>100 を「センスいい」と言っちゃう>>149 も筋悪。 すじわる、って将棋以外で聞かない単語だよね。 まあ筋が悪いとは普通に使うんだから字面を見てわかると思うけど。 >>154 ここでいう言語仕様とは学習しなくてはならない範囲の 意味が強いと思う。そういう意味なら、一人で使う場合は 別だが、他者の形式仕様を読む場合にはひと通りは抑えて いなくてはならず、Zはその点やはり負担が大きい。 Zは基本的に述語論理と型付集合論がわかってれば 覚えなければならない事はとても少ないだろ。 むしろVDMやAlloyあたりのほうが 述語論理や型付集合論以外の言語要素が多いと思う。 Zで苦労するのは他の言語/手法と比べてツールサポートが少ないことだろ。 ZもVDMも基本は70年代の言語だからなぁ 比較的新しい言語だとCafeOBJなんかがあるけど 二木先生の関わっていない利用例を知らない >>155 >言語仕様の大きさは >処理系やツールを実装する人にとっては重要かもしれないけど >ユーザにとっては重要じゃないよね。 誰にとっても同じだ。 同じことをするんなら小さい方がよいのに決まっとる >>160 だからZは要らんと言っとる >>163 CafeOBJが新しいのか >>164 そんなに言語仕様が小さいのがいいのならBrainf*ckなんか最高だよね チューリング完全だから「計算可能性の観点においては」 他の言語と同等のことができるよ 観点は計算可能性だけじゃないだろ まだチューリング完全なんて言ってるのか 観点は言語仕様の大きさだけじゃないだろ って話だよ チューリング完全ならどれも一緒だなんて誰も思っちゃいねーよ だれかこの辺の議論のような口喧嘩のようなことを交通整理できる人はいないでしょうか そういった態度というのは単に自信が無いだけなので、 生暖かく放置すればいいのではないかと思われ ところで、Prologで仕様記述やその検証ができるなら試してみたいんだが、 その方法を解説した本やWebサイトとかあるのかな? 「理論的にはできるはず」だけだとProlog自体よく知らない俺には無理だが。 >>170 >ところで、Prologで仕様記述やその検証ができるなら できないんじゃね? 過去には「できるはず...」という願望もしくは妄想に基づく意見(>>95-)はあったけど、 それに対する反論には何も意見を言えず議論を終えた 個人的には、型の無い純粋Prologを形式言語と呼ぶには無理があると考える Prologへの願望を語りたいという気持ちは理解できるが、 それはPrologスレで大いに語ればいい、それが妄想であってもいい Prologで仕様記述しますなんていう例は山ほどある。 知らないんなら論文読まなさすぎ。 どれも結論は 「表現力不足だよね」 「表現上の制限が強すぎて、かえって表現が冗長になってダメだね」 「最低限FOLは必要だよね、やっぱし」 なわけだが。 >>164 >だからZは要らんと言っとる つまりZの言語仕様はデカくないという意見に反論できないってことね。 理由も言えずに「要らん」としか表現できない人が形式仕様とか、鼻で笑っちゃうねw Alloyの本を読んでもちっとも頭に入っていきません。 この本を読むうえで必要な前提知識って何でしょうか? また、その知識を得るのに最適な書籍があれば教えてください。 今は組込み関係の仕事(主に車関係)をしていて、知ってる言語はC言語のみです。 知識はともかく 詳細仕様や実装仕様じゃなく 純粋なシステム仕様の読み書きをした経験がいるんじゃないかな 組込み関係だとシステム仕様と実装仕様がごっちゃになってる印象がある 実装仕様レベルの形式記述もできるけど そういうのは実装言語(C言語)のツールを使った方がいいと思う >>174 その存在自体が無駄だと言っとるんだから、さらに何を言う必要がある? Zや言語仕様の大きさなんていうくだらんことにどんだけ時間を浪費するんだ Zを否定した根拠が「言語仕様のデカさ」だったのに 今更なにを喚いているんだい、負け犬くんw >>164 は自分の主張が矛盾しているのに気付かない可哀想な子 >>160 が言うように、Zは「述語論理と型付集合論」を知っていれば学習の壁は低い つまり、もしも>>164 の言葉「同じことをするんなら小さい方がよいのに決まっとる」が正しければ、 仕様の小さなZは優れていていることになるが、その一方でツールサポートの少ない「Zは要らん」と言う では、ナゼそんな矛盾が生まれたのか?これは形式手法へ拒絶反応を起こす人によくあるパターンで、 形式手法を扱うのに前提となる素養(論理と集合)が欠けているからだろう だから>>164 にはZの仕様が(とほうもなく)巨大に見えて尻込みしてしまう 逆にAlloyはツールで実際に動かしながら試行錯誤できるから容易い存在に見える 実際にはAlloyの全容は巨大で難解なものだけど、>>164 には表層の一部しか見えていない おそらく、>>164 はERM/OMT/UMLのような「仕様の視覚化手法(visualize method)」には 十分な経験と自信があるのだろう ところが残念なことに、その延長で「仕様の形式化手法(formal method)」を 理解しようとして、その狭間(ギャップ)で「もがいている」のだと思われる >>175 述語論理ですかねー。あの変なシンタクスがオブジェクト指向と関係なくて、回りくどく表現された述語論理だと思うとたぶんわかってくる気がする。 あとAlloyだとたぶんその仕事にはあまり直接的に活かせないような。>>84-86 に同じような話があるけど。 >>180 そうだね、>>164 みたいな人は10年か20年ぐらい前にもいたねえ。 「オブジェクト指向」でギャップに嵌ってる人達がね…(遠い目 UMLは図を「コトバ」として読む力が必要とされるんだけど、 形式手法では式を「コトバ」として読んじゃいけない。 式はあくまで記号列として読まないと「形式」の意味がわからない。 それができない人にはZは地獄のような言語かもしれない。 そういう人ほどZで徹底した形式主義を身につけたほうがいいと思うけど、 大抵は実行系中心の軽量形式手法で「これが形式手法かー」と思っちゃうんだよな… >>180 確かに、 Zは「述語論理と型付集合論」を知っていれば学習の壁は低いのだろうが、 そういう人材を一般企業では集められなかったからZは顧みられなかった のではないか。 述語論理も型付集合論も大学の教養レベルの数学で十分なのだから 「人材を集められなかった」のではないと思う。 単に、Zに限らず形式手法なしでもシステムを作れると思ってたんだろ。 だから、Zに限らずモデル規範型の形式手法は顧みられなかった。 >>182 >形式手法では式を「コトバ」として読んじゃいけない。 >式はあくまで記号列として読まないと「形式」の意味がわからない。 ここは何を言ってるの?記号列として読んでいるのでは意味が分かっていない と言われそうだけど。 >>185 横レスだけど、形式手法の証明においては式に含まれる記号の意味は「無価値」だということ 記号の意味を分かる必要は無いし、 証明の過程で記号の意味は完全に無視され「形式(公理や定理)」だけが価値を持つ ソフトウェア仕様記述は現実世界のモヤモヤした実体(=モノ)をある体系でモデル化することから始まる たとえばUML等のOOA/OODでは現実世界をオブジェクトの集まりと捉え、オブジェクトの持つ属性や オブジェクト間の(継承や部分といった)関係を定義することによって(非形式的な)モデル化を進める ここでは実体をコトバとして抽象化する事を、具体的には定義するオブジェクト/属性/関係などの 命名(naming)を、つまり(人にとっての)直感的な意味を重要視する これによって(人にとって)分かりやすく、特に共同作業下における仕様イメージの統一的な共有化を図る これに対して、形式手法では現実世界をモデル化することは(視覚化手法と)同じだけれど、 数学という形式的な体系を用いる点が異なる つまり、ある式(=モデル)が直感的には(=人にとっては)いかに分かりやすくて正しく見えようとも、 いいかえるといかにOO的視点では優れた設計であっても、形式に矛盾があれば誤りであると見なす >>186 こっちも横レスだけど 証明は形式意味論のレイヤーで行われるけれど 形式仕様自体は現実世界の概念(「コトバ」)とリンクしている 「コトバ」であり「記号列」であることを理解できないと 形式仕様を理解したことにはならんだろう >>186 >形式手法の証明においては式に含まれる記号の意味は「無価値」だということ それは証明器にとって、ということでしょう。人間にとってではない。 >これに対して、形式手法では現実世界をモデル化することは(視覚化手法と)同じだけれど、 そのモデル化の時点で、「意味」が介在するよね。 >形式に矛盾があれば誤りであると見なす それは当たり前。矛盾というのは形式的なものだからね。 だからといって「意味」が不要ということにはならない。 「形式」手法 "form"-al method という言葉の意味からはじめないといけないようだな! >>189 およその意味はみんな分かってると思うが その厳密な定義もない(あるいは厳密に定義する意味もない)ことも含めて だがもし必要なら、そこからはじめてくれてもよいが みんな数学ガール/ゲーデルの不完全性定理 でも読んで和みたまえ(ステマ) >>187 ,188 現実世界を抽象化する過程に意味が伴うのはその通りで、視覚化手法も形式手法も同じ 形式手法にとっても抽象化の過程ではコトバの意味が大切なのに変わりはない 違うのは、抽象化の成果物である「仕様(設計書)の検証」において、視覚化手法では (人間が介在する)直感を頼りとしており、そこではコトバの意味が重要な位置を占める それに対して形式手法では仕様の検証に人の直感は介在せず、コトバの意味は無視する ここで、証明(=形式を元にした検証)を人力でやろうが証明器で自動化しようが同じ そして、もし証明が失敗すれば(仕様に矛盾を発見すれば)、現実世界の抽象化という前工程に立ち返る その時には、(数学としての)形式化の単純ミスもあるだろうけど、コトバの意味(の定義)の過ち、 つまり(抽象化の過程で)現実世界の解釈に何か誤りや漏れがあったことが発見できるだろう >>188 >>形式に矛盾があれば誤りであると見なす >それは当たり前。矛盾というのは形式的なものだからね。 いや、「非形式的な矛盾(=直感に基づく矛盾)」というのは存在する たとえばOOの仕様で、ある箇所では「XはYのサブクラスである」と記述され、 別の箇所では「YはXのサブクラスである」と記述されていれば、それは矛盾だろう ただし、サブクラスというオブジェクト間の関係は(人の)直感として定義されたものだから、 それは「形式的な矛盾」ではない この会話が成立していないのに 話が流れていく感じはすごいな 形式手法に言及しているのに 詭弁(誤謬)ばかりってのが皮肉 >>193 >「非形式的な矛盾(=直感に基づく矛盾)」というのは存在する 形式的に意味不明な言明だ。 論理的訓練が不十分のようだから指摘しておく。 >別の箇所では「YはXのサブクラスである」と記述されていれば、それは矛盾だろう 矛盾とはAかつ¬Aが帰結することだ。「XはYのサブクラスである」と 「YはXのサブクラスである」はまだ矛盾ではない。 >ただし、サブクラスというオブジェクト間の関係は(人の)直感として定義されたものだから、 そういう関係もまた形式的に記述するんだよ。 >>194 >形式手法に言及しているのに >詭弁(誤謬)ばかりってのが皮肉 意味不明。間違いがあれば指摘すればよい。 形式手法=無謬ということではない。形式手法を偶像崇拝してる? >>192 概ね妥当なコメントと思うが 「視覚化手法」なんてものを形式手法と対比させるのはいかがなものか それから、ここでは皆矛盾矛盾と言うが、矛盾がないというのは最低限の条件に過ぎない >>184 20年近く前に、私の周辺でZの研究会が次々と撃沈していったのを 知っている私としては、隔世の感ありだな。 >>197 撃沈の主な原因は何だったのですか? そのころなら述語論理や集合論ではないと思うのですが 計算機の性能だな 20年前のCPUの性能ではSAT SMTソルバーをぶん回すとかありえんだろう >>199 隔世とは、大学の教養レベルの水準が上がっているのだなぁという 漠然とした印象です。 直接の原因はテキスト(>>162 )にあったと思います。これに限らず、 勉強会がうまくいくかどうかには、早い段階で良い要約を誰かが 準備してくれるかどうかが大事ですが、それをしてくれる人が いなかった。それでほとんどの人に全貌が見えなかった。 >>195 スマン、言葉が足りなかったようだ >>193 での「非形式的な矛盾」とは「(UMLのような)非形式手法における矛盾」のこと そして非形式手法においても矛盾(という概念)は(人間的な)直感として存在していることを言いたかった たとえそれが形式主義の視点では「意味不明な言明」であったとしても.... >>ただし、サブクラスというオブジェクト間の関係は(人の)直感として定義されたものだから、 >そういう関係もまた形式的に記述するんだよ。 形式手法であれば、構築しようとする体系(システム)におけるサブクラスという関係を (形式的に)定義するのは当然のことだね ここで、もしもサブクラスの(形式的な)定義に交換律を含めれば、 「XはYのサブクラスである」かつ「YはXのサブクラスである」(という仕様記述)は矛盾ではなくなる つまり、(形式手法の)証明ではサブクラス(というコトバ)から人が連想する直感的な意味は無視される たとえば、仮にサブクラス(というコトバ)の代わりに机や椅子(というコトバ)で仕様が記述されていても (無矛盾であることを)証明できるのが形式手法であり、それが非形式手法との違いになる >>202 >交換律を含めれば 細かいのだが、ここは、反対称律を含めなければ、だな >つまり、(形式手法の)証明ではサブクラス(というコトバ)から人が連荘zする直感的な�モ味は無視されb >たとえば、仮にサブクラス(というコトバ)の代わりに机や椅子(というコトバ)で仕様が記述されていても >(無矛盾であることを)証明できるのが形式手法であり、それが非形式手法との違いになる この辺り、ヒルベルト流の「形式主義」の説明なら妥当だが、ソフトウェア工学の「形式手法」の 説明としては相当ズレてると思う >>203 識別子の字面に引きずられるようなら、その時点で形式手法を使う意味は半減するよ。 形式仕様を読み書きする時には、字面が持つ自然言語的意味を無視して あくまで記号操作の対象として扱う。 識別子の字面が大事になるのは、形式手法を知らない人に説明する時。 「形式的に」扱う訓練を受けていない人のために非形式的意味を使う。 非形式的な意味を持たせた時点で、その記述は形式仕様ではなくなる。 pi = 3.14159 e = 2.71828 と e = 3.14159 pi = 2.71828 で「後者に違和感を持つのは間違い」という奴の 形式仕様は読みたくないな 形式仕様からプログラムコードを自動生成してメンテナンスフリーというならともかく それがソフトウェアなり何なりの「仕様」を定めている以上 非形式的な意味は持たせてもいいし それによって非形式的仕様になる訳じゃない 非形式的な意味は形式的検証の結果に影響を与えないのだから >>205 >形式仕様を読み書きする時には、字面が持つ自然言語的意味を無視して >あくまで記号操作の対象として扱う。 そんなことをは君(人間)は気にする必要はないのだ。 放っておいても証明器は完璧にそうしてくれる。 同じことを君(人間)がやってもそれこそ効果は半減する。 書くことは人間にしかできないのだが,そのとき「記号」で書いていては, そもそもどういう対象を書いているかが分からないだろう?w >「形式的に」扱う訓練を受けていない人のために非形式的意味を使う。 訓練を受けているとかいないとかでなく、どんな相手だろうと、何を書いて いるかを伝えるためには、単なる記号では伝わらないんだよ。 >非形式的な意味を持たせた時点で、その記述は形式仕様ではなくなる。 これも違う。人間がどういう読み方をしようと、machine readableであれば 形式仕様なんだよ。 あと、君が「形式手法を知らない人」「訓練を受けていない人」とよく 言ってるらしいのが気になるな。 >>206 >これも違う。人間がどういう読み方をしようと、machine readableであれば >形式仕様なんだよ。 じゃあポインタをキャストしまくってるCのソースも形式仕様だねw >>206 >同じことを君(人間)がやってもそれこそ効果は半減する。 残念ながら、その形式言語の表現力がFOL以上であれば、 (非定理を含む)あらゆる式を自動的に証明可能なアルゴリズムは存在しない。 >>205 >e = 3.14159 >pi = 2.71828 まさに、こういうまやかしに惑わされないために 先入観を排して記号を記号として扱う訓練が必要なんだよ。 エラーや例外が発生しないプログラムが必ずしも「正しい」訳じゃないように 形式的に無矛盾な仕様が必ずしも「正しい」訳じゃない 無矛盾な証券決済システムの仕様は 鉄道運行管理システムの仕様としては全くもって正しくない 記号を記号として扱うのは機械でもできるし機械の方が得意だ しかし形式意味論では扱わない記号に込められた「意味」を読み取るのは 現状では人間にしかできない 機械が得意なことは機械に任せて 人間は人間にしかできないことに力を入れる方が得策だろう >>212 なら自然言語とか図形言語で仕様書いてれば? 機械が形式仕様を書いてくれるようになったら やってもいいかもね >>214 それが可能ならそれこそ形式仕様なぞ不要だな そもそも何でも証明器で検証するのが前提になってる>>206 は 形式手法にどんな夢を見ているんだ? >>206 > 放っておいても証明器は完璧にそうしてくれる。 > 同じことを君(人間)がやってもそれこそ効果は半減する。 残念ながら証明器は放っておいても何もしてくれない。 証明器を有効に使うために必要なエフォートを知った上での 主張とは思えない。 > どんな相手だろうと、何を書いて > いるかを伝えるためには、単なる記号では伝わらないんだよ。 piを「円周率」として読むレベルの厳密さで良いのであれば、 拘束文法による半形式仕様で十分だ。 >>215 とりあえず俺は>>206 じゃないが 複数の人間の発言を一緒くたにされても困る >>そもそも何でも証明器で検証するのが前提になってる 証明器での検証を前提としない軽量形式手法においては 人間に意味が伝わらない仕様は使い物にならない 形式仕様は自然言語の曖昧さの排除が目的であって意味の排除じゃない > 残念ながら証明器は放っておいても何もしてくれない。 人間が記号を記号として扱ってメタな意味を排除すると証明器は何かしてくれるの? >>216 > 証明器での検証を前提としない軽量形式手法においては 全てを証明器でやるわけではないからといって、 必ずしも証明器での検証を前提としないわけではないだろう。 形式仕様スレでこんな論理の基礎を指摘しなきゃいかんのか? > 人間が記号を記号として扱ってメタな意味を排除すると証明器は何かしてくれるの? はあ? まだ証明器が何もかもやってくれるとでも思ってるのか。 証明器はドラえもんのポケットじゃないぞ。 言葉が通じないというか 相手の発言の意図を汲もうという気が感じられないな 発言の意図を汲み取ってクレクレ言う人が形式手法とは恐れ入った! 現行の証明器の能力が限られてることと 人間が非形式的な意味を排して形式仕様を読まなければいけないことの間に 随分と論理の飛躍があると思うんだけど 非形式的な意味を排して形式仕様を読める能力が必要だとして 形式仕様から非形式的な意味を読み取るor 形式仕様に非形式的な意味を書き記す能力が 同時に成立しない・成立させてはいけない理由は何? 両方の能力が必要なんじゃないの? >>212 >無矛盾な証券決済システムの仕様は >鉄道運行管理システムの仕様としては全くもって正しくない ミスリードが2つある。 1つ目は、無矛盾な証券決済システムの仕様があったとしても その仕様が証券決済システムの仕様としてvalidとは限らない。 なのにあたかも証券決済システムとしてvalidであるかのように、 鉄道運行管理システムの仕様としてinvalidだと主張している。 2つ目は、条件なしに「全くもって正しくない」と書いていることから、 「全ての」無矛盾な証券決済システムの仕様が 鉄道運行管理システムの仕様として「完全にinvalid」だという主張になる。 これは正しくない。 無矛盾な証券決済システムの仕様のうちいくつかは 鉄道運行管理システムの仕様としてinvalidな部分がある、 というならば、それはそうだろう。 もっとも、 無矛盾な証券決済システムの仕様のうちいくつかは 証券決済システムの仕様としてinvalidな部分がある、 も正しいがな。 >>220 「同時に成立しない・成立させてはいけない」なんて主張はしていない。 それは>>204 を読んでくれ。 その>>204 に対して 「いや、証明器があるから、人間は形式仕様を自然言語的な意味で解釈すればいいんだ。人間が自然言語的な意味を排除する必要なんてないんだ。」 という主張をしている人がいるんだ。 >>221 言ってる内容については理解するけどね そういう揚げ足取りをするなら 「全くもって」を全体と部分の議論にすり替えてるのはミスリードじゃないの? >1つ目は、無矛盾な証券決済システムの仕様があったとしても >その仕様が証券決済システムの仕様としてvalidとは限らない。 それを理解している人なら >e = 3.14159 >pi = 2.71828 を「まやかし」だなんて思わないだろう >>222 > 形式手法を使う意味は半減するよ。 これが文字通り意味が50%になるって主張なら「同時に成立させてはいけない」とは言ってない。 しかし明らかにこの発言には「識別子の字面に引きずられてはいけない」という 否定的な主張が含まれている。 違うかね? >>223 いや、実際その例はまやかしだよ。 じゃあ pi = 3.1415926532 だったらどうする? piを円周率だと思って読み進めて地雷作る? eだろうがpiだろうが3.14159だろうが3.1415926532だろうが 「記号として書いてある通り」 に理解して 「記号として定義されている通り」の振る舞いについて validityを評価するしかあるまい? >>224 字面に引きずられて、それで「形式手法やってます」と言えるの? >>225 お前は自然言語が使えるんだろ? 「ここの記述はミスじゃないですか?」 「書き換えても検証結果は変わらないしミスということで直しましょう」 こんなやりとりもできないの? >>226 形式的な意味しかない記号の列を作って「仕様書いてます」と言えるの? >>227 つまり>>204 に賛成なわけだね? 形式仕様として読む上では記号列をして操作し、 非形式的な説明においては自然言語的意味を使う。 そういうことだろ? ところで、 >>225 > じゃあ > pi = 3.1415926532 > だったらどうする? このpiは円周率ではないことには気付いたよな? >>228 それで正しいシステムが出来れば、堂々と「仕様書いてます」と言っていいだろ。 もちろん、形式手法やっていない人とは非形式的意味を使って説明した上で。 「形式仕様として扱う時には記号列として操作する」 ここから「全ての状況において非形式的扱いをしない」を導き出しちゃうとはね。 どんな論理体系なんだろうな。 >>228 まさか形式仕様スレでこんな幼稚な主張が出てくるとはね… 「自然言語的な意味に引きずられずに、記号を記号として操作する訓練が必要」 ここからどうして 「形式的な意味しかない記号の列を作って」 となるかが不明。 この人にとって形式仕様とは一体何なんだろう。 例えば注釈なしのペトリネットやオートマトンで記述したものは 仕様を構成するドキュメントとは認めないのだろうか? ぜひ拝聴したくなった。 批判するなら>>182-の文脈を加味してもらいたいものだね >>180 と>>182 の2人は理論と経験が伴ってるね >>234 君を含めて、三人は理論と経験が伴ってることになるね。 【会社の即戦力の定義とは】 「社会の一員として人々の役に立つ価値を提供すること」 会社にとって喉から手が出る程欲しい人材とは、 この求められる価値を提供するために、解決すべき 課題を正しく共有し、一緒になって価値を生み出す ことが出来る人材なのです。 ところがJALグランドサービスの即戦力って言っている奴らは自分の気の合う人には仲良くするけど 気に入らない人間には粘着してとことんまで罵倒したりパワハラしたり自分にはとことん甘いくせに人の揚げ足ばかり探して 仕事中も喋ってばかりで口元緩んでばかりじゃないか 先に暴言を吐けば自分が強いと思わせることができるなんて考えているみたいだけどそれは違う それは弱い動物がキャンキャン吼えているのと同じことだよ JALグランドサービスは仲良しクラブ会社 仕事中 趣味の話で盛り上がって手が止まってんだよw たまには仕事まじめにやったらどうだね? JALグランドサービスは貧乏性でテーブル拭いて汚れたタオルを次の清掃場所 さらに次の清掃場所にもっていって汚れたタオルを使えっていってきた タオルからはなんともいえない臭いが漂い色もケチャップやなんやらがこびりついていて汚かった お客さまのためにを毎日言っている会社なのになにこれ? 矛盾してるよね? 青タオルはウンコがこびりついていて汚い それをキレイなタオルといいラバーのほかギャレー 床のゲロ掃除などさまざまなところで活用している バケツにそのタオルを濡らすとき気持ちが悪い バケツもすごく汚いよね バケツ洗っているところみたことがないし JALはこんな会社です 白タオルは生乾きで蒸れた悪臭がしている それでお客様がつかうテーブルを拭いているんだから あのテーブルは菌をひろげているようなもんだ JALグランドサービスはパートやアルバイト、契約社員に対し若い正社員ですら横柄かつ高圧的な言動(恫喝行為など)を取ることが常態化されていて それを正せる上司が一人もいないというのが特徴の会社 人が見えにくい場所で係長がとある気弱な社員のわき腹を殴ったり 蹴っ飛ばしたり頭を殴ったりしていた あれをパワハラといわずになんていうのか? こんな屑なことばかりやっている悪質な会社JALの傘のなかでふんぞり返っているのだから JALそのものがたいしたことがないといえるだろう 班長 係長 課長とも人間としての品格を疑うことがおおい 常軌を逸した行動を認知していながらそれを容認しているJALグランドサービス フィロソフィなどただ毎日口にだして読んでればそれで満たされる ただそれだけのもの どんなりっぱな言葉を並べたとこでそれを毎日読んでる人間が バカじゃ意味がない 陵辱 ひとの足をひっぱったり人を不幸にしている JALグランドサービスが物心両面の幸せだと? 笑わせるなw クズ会社がw ロッカーの一番奥の壁を誰かが蹴っ飛ばしたのかなんだかわからないけど 大きな穴があいて破損させた馬鹿がいたよね? 犯人つかまったの? あれだけの穴があいていて音が聞こえなかったなんておかしいよね? こんな不祥事はこの会社しかないだろうしあれだけ人が多いロッカーで誰も気がつかないのもこの会社だけw アホJALグランドサービスw >>188 =>>206 が暴れているだけで 他の人は多少の立場の違いはあっても 根っこの部分は妥当なことを言ってるな 素朴に疑問に思ったのだが このスレは時折 「形式主義を否定した形式手法」 とおぼしきものが主張されているようだが これは軽量形式手法の一派か何かなのか? 通常のソフトウエア工学では 形式手法とはシステム記述に形式主義を導入して 形式主義的な検証や開発をおこなうこと を指すと思うのだが... 技術として否定的(悲観的というべきか)であっても 形式主義の否定はしてないんじゃ? 表現が拙いだけで 「通常のソフトウェア工学」とかしれっと言っちゃうあたり >>246 も大して変わらんレベルなような印象を受けるが >>205 >e = 3.14159 >pi = 2.71828 >で「後者に違和感を持つのは間違い」という奴の >形式仕様は読みたくないな そういう話なのか? hoge = 2.0 * pi * r という形式的定義があった時に 円周率や半径の類推から piやrの形式的定義を辿らずに hogeを円周の長さだと思い込んではいけない という話なんじゃないのか? >>247 例えば>>188 は 形式主義を真っ向から否定しているようだが? ■ このスレッドは過去ログ倉庫に格納されています
read.cgi ver 07.5.1 2024/04/28 Walang Kapalit ★ | Donguri System Team 5ちゃんねる