【Alloy】形式言語による仕様記述【VDM】
■ このスレッドは過去ログ倉庫に格納されています
>>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 は 形式主義を真っ向から否定しているようだが? >>248 そういう話も包含されているだろうね 仕様を書く人は誤解を生まないように気を付けた方が良いし 仕様を読む人は思い込みをしないように気を付けた方が良い そんな凡庸な結論では刺激が足りない人が 極論で言葉遊びしているのがこのスレ >>249 もっと具体的に言ってくれないと同意も否定もできん 式に含まれる記号の意味は証明(記号の操作)に無関係である しかし人間は様々な形式化されていない知識を持っている それは当該の公理系においては誤ったあるいは誤っているかどうか判断出来ない 推論規則をもたらす知れないが無価値とは言えない どのくらいの価値があるかは適用場面や人の価値観によるだろう >>209 >じゃあポインタをキャストしまくってるCのソースも形式仕様だねw ということになるね。なぜダメ? あなたの定義は? Cは未定義動作や実装依存があるから 形式的意味論が定義されているとは 言えないんじゃないかなー 機械可読なら形式仕様って それじゃエクセル方眼紙も形式仕様かよw >>246 >形式手法とはシステム記述に形式主義を導入して >形式主義的な検証や開発をおこなうこと >を指すと思うのだが... ちょっと違う。「主義」をはずせばよい。 >>248 >そういう話なのか? >hoge = 2.0 * pi * r >という形式的定義があった時に >円周率や半径の類推から >piやrの形式的定義を辿らずに >hogeを円周の長さだと思い込んではいけない >という話なんじゃないのか? いや、そもそもhogeやrを円周や半径と思ってはいけないと言ってるんだろ? それに、いくら形式的定義を辿ってもhogeが円周だとはわからないよ >>249 >形式主義を真っ向から否定しているようだが? 形式主義を否定してるんじゃなくて、形式手法=形式主義ではないと言ってる >>250 >仕様を書く人は誤解を生まないように気を付けた方が良いし >仕様を読む人は思い込みをしないように気を付けた方が良い 随分ぬるいがwまあそういうことだ。記号病達にはこれも伝わらないのじゃないかな >>255 > 「主義」をはずせばよい。 formal methodsからformalismを取ったら何が残るの?ばかなの? > それに、いくら形式的定義を辿ってもhogeが円周だとはわからないよ hogeを円周と読むなって話だということが理解できない?ばかなの? >>255 既に誰かが指摘しているようだが あなたが形式手法と呼んでいるものは 制限文法による仕様記述なのでは? >>256 >formal methodsからformalismを取ったら何が残るの? アスペを相手にしたくないので、短く言うが、数学と記号表記の関係と同じ。 >hogeを円周と読むなって話 だから、>>255 で、君達はそう言ってるんだろ、と言っただろ。よく読め >>253 >Cは未定義動作や実装依存があるから それは細かいことではないか。それに、未定義の所は使わければよいし、実装依存ならその実装に従えばよいし >>254 >それじゃエクセル方眼紙も形式仕様かよw 方眼紙だけだと何もない形式仕様ということになるね >>257 なんの限定もついていない形式手法について話してるつもりだが? しかも言ってることは、「記号操作が本質なのじゃないよ」ということだけ >>256 >hogeを円周と読むなって話 そんならそもそもお前は何を書いているんだという話 >>260 "制限文法" "仕様記述" でggrks >>259 それを「細かいこと」なんて言う人が 形式手法に何の用があるんだい?あほ? >>263 アスペの上に、言葉づかいの癖から見てクズのようだからもう相手しないが >それを「細かいこと」なんて言う人が それが細かくない(本質的である)と思っているということは、君は未定義動作や実装依存をなくせばCのソースも形式仕様だと言うんだな それから、形式的ということと細かいということは同じことではないんだよ まずJavascriptで書きます。 次に実行します。 ここでエラーが出たら間違いがあるということです。 正しく実行できたら正しく実行できるということです。 なんというトートロジー エラーが出なくても正しいとは限らないのは>>212 で言われているとおり >>264 >それが細かくない(本質的である)と思っているということは、 この前提から > 君は未定義動作や実装依存をなくせばCのソースも形式仕様だと言うんだな こんな帰結を導出する人には、形式手法は無理です。(きっぱり Alloyの本を読んで容易に理解できるには、前提知識として何が必要ですか? このブログ http://d.hatena.ne.jp/rabbit2go/20110802/1312252092 でも初心者だが容易に理解できたとあるが、私は読んでもさっぱりわかりません。。。 佐原伸 @donkeyshin: ちゅうか、機関銃買ってレイシスト撃ち こrしたくなるので米国ボイコット^_^ RT @tomooda: まあそうなんだけど、USAもユートピアとはほど遠い。全体主義も吹き荒れるし,雇用だって安定しないくせに階層間の流動性は日本以上に低い。レガシーとしか言いようがない古く非合理的な。 SPINを勉強し始めたところなんだけど、ミューテックス/セマフォ/モニタって promelaでどう記述するのが一般的なんだろう? セマフォはBasic Spin Manualにあったけど、どこかにまとまった情報がないかな。 久しぶりに来たが、超過疎ってるなw 形式仕様なんてどれもクソだって分かったかw クソではないよ 適用分野がとっくに収束してて適用分野も枯れてる 誰も語る事がなくなっただけだ 質問もないから新しく始める人もいないってことだろうな。 >>273 >>274 歯切れが悪くて何を言ってるか分からんが、 もうオワタ、でオーケー?何も残さんで 形式仕様なんてどれもクソだが クソ未満の非形式仕様が溢れかえっている喜劇 >>271 ミューテックスとセマフォの違いって排他制御の「実装」レベルの話なんじゃ 例えばデッドロックを回避する機構を入れたいなら そういうコードを書かなきゃいけない ミューテックスの一般的と言えるような実装がない以上 promelaでの一般的な記述もないような 余計なお世話かも知れんが モデル検査は排他制御のあるシステムの検証には適しているといえるけど それは排他制御を抽象化しての話 排他制御自体の検証には向いていないと思う >>276 結局ソフトウェアエンジニアリングがクソだと言ったか?w > それは排他制御を抽象化しての話 > 排他制御自体の検証には向いていないと思う これは何言ってる? >>271 の問題はまさにそこのところ、モデルと実際のプログラムをどう対応付けるかなんだろう。 VDMが実際の開発に導入されている話は聞くがAlloyについてはあまり聞かないのは やはり抽象度のギャップの要因が大きいように思う。 >>278 抽象度のギャップは大きいほどいいじゃないか なんで大きいほどいいの? ギャップ=0で、動くプログラムがそのまま検査できるのが理想じゃないのか。 >>280 ん?言葉の違いか? ギャップってモデルと実際のプログラムの間の抽象度の違いのことじゃないのか? うん、その違いだよ。 抽象度の高いモデルで正しさを証明できたとして、それをもって現実のプログラムの 正しさの証明とするにはギャップは小さいほうがいいと思うが。 書き換えの段階で間違いが入ったらそもそも意味がないし。 ギャップが大きいほどいいとする理由は? えー! 極端な場合で考えてみなよ ギャップ=0ということはモデルの意味がないということだ モデルの意味って何ぞ? >>278 の言う現実のプロジェクトではモデルを構築することそれ自体が目的じゃなくて 実際のシステムに誤りがないことを保証したいわけだろう。 モデルはそのための道具でしかない。 モデルがなぜそのための道具になりえるとしたら、それはモデルが何だからか考えてみな モデルがそのための道具になりえるとしたら、それはモデルが何だからかを考えてみな ここでそういう質問が出るとは思わなかったが、形式手法におけるモデルの意義は 機械的に検証可能であることに尽きるだろう。現実のプログラムではそれが難しいから モデルで代用していると言ってもいい。 たぶんあんたが考える「モデルの意味」は違うんだろうけど、じゃあそれ説明して。 まぁ色々な側面があると思うけどね 形式手法によって手戻りを低減するには できるだけ早期に検証することが有効で 建前としては仕様が実装に先行するのだから 検証の対象は実装より抽象度が高くなる とはいえギャップが大きすぎるのも実際的ではない だからBやZで言われる段階的詳細化が意味を成す 別の大きな側面としては 抽象化しないと現在の計算機・理論ではまともに検証できない というのがある 簡単に言えば状態変数として二値変数が64個あるだけで 状態空間を表現するのにアドレス空間を食いつぶしてしまう 自然数や実数を扱うプログラムをまともに自動検証できるようにするには ハードにせよ計算理論にせよ技術革新が必要 勿論「矛盾がない」という検証結果が 実際的な時間・コストで得られないとしても 「矛盾がある」という結果が早期に得られる場合もあるので 計算機ぶん回すのも無意味ではないが それはいわゆる形式手法というより「テスト」の範疇だと思う >建前としては仕様が実装に先行するのだから >検証の対象は実装より抽象度が高くなる >抽象化しないと現在の計算機・理論ではまともに検証できない 積極的に抽象化すべき理由じゃなくて単なる結果だな。 自然言語の曖昧さの排除という使命がある以上 闇雲に抽象化すればいいってもんでもないだろ さらに言うなら「単なる結果」でない 形式手法を使う積極的理由なんてあるのか? どいつもこいつもwこの分野のやつらはw そんなのを抽象化なんて言うから世間から笑われるんだ 単なるアバウトって言うんだよ >>294 アバウトなのは、抽象に関するあんたの理解。 質問に罵倒なんぞは自然言語でいいが、主張は形式手法言語で書いてくれ。 Event-Bしか読めないけど。 形式言語で表現できるのは形式的意味でしかなく 主張するところの、いわゆる意味を示すことはできない そして論理的に矛盾の無い主張だからといって有意義とは限らない ここで「偶数+奇数は奇数だ!」と主張したところで スレチとなるだけ ま、自然言語から意味を見出しているのも幻想かもしらんが Alloyって楽しいな。 コンピュータと対話しながら、記述対象に対する自分の理解を深められるのがとても楽しい。 ■ このスレッドは過去ログ倉庫に格納されています
read.cgi ver 07.5.4 2024/05/19 Walang Kapalit ★ | Donguri System Team 5ちゃんねる