Commits

camlspotter committed 4806bd1

updated

Comments (0)

Files changed (1)

 例えば一番簡単な静的なプログラム検証はプログラムを実行する前にパースしてみて文法があっているかどうか
 調べることだ。これはあまりに簡単すぎて普通は静的検証とは言わないのだが、ロケットを飛ばしてみて月着陸寸前に
 ここの何行目にミススペルがあったのでプログラムの実行を中断しますテヘッっという通信をロケットから
-受け取りたくなければ、まあ、事前にやっといて損はないだろう。
+受け取りたくなければ、まあ、費用もかからないし、事前にやっといて損はないだろう。
 
 凄くコストの掛かる方の静的検証はモデル検査とか呼ばれる奴が代表。要はプログラムを実際に動かすのだが、
 さすがにそのまま動かしていたらキリが無いので色々と簡略化する(連中はカッコよく、抽象化する、と言っている)。
 例えば整数は無限にあるから整数に関するプログラムの検証は虱潰しにではテストしていられない(無限である)が、
 整数を素数か合成数かと大まかに二つに抽象化してやるとうまくするとそのレベルでは虱潰しが有限で現実的な物になる、
-かもしれない。で、うまくすると…この関数は必ず合成数しか返さないので東工大生が狂喜乱舞しないので会社は黒字になる、
-ということが証明できたりする。
+かもしれない。で、うまくすると…この関数は必ず合成数しか返さないので東工大生が狂喜乱舞しないので会社は黒字になる、ということが証明できたりする。抽象化の度合いによっては検査に膨大な時間とメモリ、つまり金がかかる訳だが、どこまで頑張るかは、世知辛いけどお財布とか、マジでコケた時にどれくらい損が出るかとかを考えることになる。
 
-静的型検査というのはこの中間位の検査方法だ。型検査ではプログラムを抽象化して安価に実行する、というよりは
-むしろプログラムの部品部品の型を見て組み合わせ部分の整合性を確認する。外科手術で使う麻酔ガスを始めとする
-ガス管のつなぎの部分はガスの種類に寄って異なってデザインされており、間違ったガスが -- 例えば麻酔ガスの
-所に二酸化炭素が -- 流れないようになっているのだが、これに似ている。ボンベ、チューブ、マスク、それぞれ
-接続するところが合っていれば、正しいガスが流れてくる。とりあえず接続してみてから医者が(看護師でもいいですけど、
-まあ、高職位が責任を取らないとネ!)試しにマスクを被ってみて、ペロッ、これは麻酔ガs zzzzz...とか一々
-やらなくても安全が保証できる。コストがかからない。実際にガスを吸わないところがキモなのでこれは覚えておいて欲しい。
+静的型検査というのはこの中間位の検査方法だ。型検査ではプログラムを抽象化して安価に実行する、
+というよりはむしろプログラムの部品部品の型を見て組み合わせ部分の整合性を確認する。
+外科手術で使う麻酔ガスを始めとするガス管のつなぎの部分はガスの種類に寄って異なってデザインされており、
+間違ったガスが -- 例えば麻酔ガスの所に二酸化炭素が -- 流れないようになっているのだが、
+これに似ている。
+ボンベ、チューブ、マスク、それぞれ接続するところが合っていれば、正しいガスが流れてくる。
+とりあえず接続してみてから医者が(看護師でもいいですけど、まあ、高職位が責任を取らないとネ!)試しにマスクを被ってみて、
+ペロッ、これは麻酔ガs zzzzz...とか一々やらなくても安全が保証できる。
+コストがかからない。
+実際にガスを吸わないところがキモなのでこれは覚えておいて欲しい。
 (一方の動的型検査ではチューブの形を見るのではなく、実際にガスを吸ってみる。)
 
-静的型検査が剛直であるというのはそういう点だ。どう見たって安全じゃないですか、ほら、ボンベから患者の口まで
-こう流れてるんだから麻酔ガスしか流れないっすよ?決まった規格のプラグ付きでないと使えないとか面倒くさくないっすよ?
+静的型検査が剛直であるというのはそういう点だ。どう見たって安全じゃないですか、
+ほら、ボンベから患者の口までこう流れてるんだから麻酔ガスしか流れないっすよ?
+決まった規格のプラグ付きでないと使えないとか面倒くさくないっすよ?
 とは言ってもこれは規則で決まっているんだ、規則は規則、キミも人事に睨まれたくは無いだろう?
 悪いようにはならないヨ。
 
 (これはどんな安全性に関しても同じ事だ。幾ら静的プログラム検証でプログラムの正しさが検証されていても
 CPU にバグがあれば意味がない。)
 
+また、このプラグの形による静的安全性は、流れるガスの種類が想定ないであることしか保証しない。
+ガス圧が100気圧くらいで患者が風船のようにボン!となるかもしれないがそれはもちろん保証外である。
+ガス圧も静的に保証したいなら圧力調整弁を買いなさい。それに見合うお金があって、破裂した患者から
+訴えられるのが嫌なら。
+
 ついでだから、求められる安全性というものは相対的なものだという事も言っておこう。
 例えば、ボンベ、チューブ、マスクのプラグの形が合っていなければ使えないという安全性のデザインは
-野戦病院では全くの邪魔でしかないかもしれない。
+野戦病院では全くの邪魔でしかないかもしれない。野戦病院に行ったことがないので知らないが。
 
 型付けが強いとか弱いとか
 =============================
 
-普通の街の病院、ボンベ、チューブ、マスクのプラグの形が合っていなければ使えないはずの
-ところでも、ガスを間違えて患者が死んだり植物状態になったりすることがある。バカが間違ったプラグでも
-よく噛んでから無理やり力技でハメて使ってしまうからである。手術を受けるのが怖くなりましたか?
-静的型検査にもこういうのがある。
+普通の街の病院、ボンベ、チューブ、マスクのプラグの形が合っていなければ使えないはずのところでも、
+ガスを間違えて患者が死んだり植物状態になったりすることがある。
+バカが間違ったプラグでもよく噛んでから無理やり力技でハメて使ってしまうからである。
+手術を受けるのが怖くなりましたか?静的型検査にもこういうのがある。
 
 型を使って静的に検証したので、必ず(CPUにバグがあるとか飼い猫がマシンの上でおしっこをしたとか、
 想定外の自体が無い限りは)何か良い性質が保証されている場合は、強い型付けがされている、などと言う。
 
 一方、型を使って静的に検証したので、まあ、大抵、何か良い性質があるんですが、
-たまに、ほら、ね?わかるでしょう、あなたもオトナだ。金か?金が欲しいのか?みたいなのは弱い型付けという。
+たまに、ほら、ね?わかるでしょう、あなたもオトナだ。金か?金が欲しいのか?
+みたいなのは弱い型付けという。
 要するに気休めでしかない。剛力(あやめではない)がいる病院の麻酔システムはプラグがちゃんとしていても
 弱い型付けしかされていないかもしれない。
 基本的に弱い型付けは何の保証にもならないので、普通の人間は相手にしない。
 動的型検査ではプログラム実行中にプログラム内を流れる実際の値の型を見てそれが今からやる演算に対して
 使えるものかどうか確かめる。麻酔ガスのマスクの所で手術中、本当に麻酔ガスが流れているかどうか、
 常に味見をするようなものである。医師(か看護師)は窒息するかもしれないが患者の家族からは訴えられないし、
-医師(か看護師)は交換が効くからね。
+医師(か看護師)は交換が効くアセットである。もちろん理事長のあなたは交換が効かない。そういうものでしょう?
 
 動的型検査が柔軟だというのはそういう点だ。野戦病院では資材が足りないからプラグの形なんかでチューブやら
-なんたら複数揃えてられない。だから適当につなぐ。適当につないでもどこかクリティカルな所で実際に流れてくる
-やつが安全かどうか確かめればいいわけだ。医師や看護師が吸ってたら困るから、誰が他人が試しに吸うことになるが誰が?
+なんたら複数揃えてられない。だから適当につなぐ。適当につないでもどこかクリティカルな所で実際に流れてくるやつが安全かどうか確かめればいいわけだ。野戦病院では理事長はいないし、医師や看護師が吸ってたら困るから、誰が他人が試しに吸うことになるが誰が?
 お察しください。
 
 例えば次のようなコードを大抵の動的型システムでは何の問題もない::
 大変ユニイクな文字列の掛け算概念を提唱していない限り。
 筆者ら(FIXME)はパなんとかとかルなんとかという言語の事は知ってるから指摘不要)
 
-
-だらららら
+だらららら(何か埋草を書きましょう)
 
 そういう見切り発車は困る、という場合はテストをやる。テストの方法にはいろいろある。各部品に分けたテスト
 はユニットテストと言う。小部品に分けてテストするのでテストすべき組み合わせが減りコストが下がる。
 筆者ら(FIXME)は静的型検査と動的型検査のどちらが良いのかを主張しない。
 まあ、基本的に静的方検査の方が理論とか難しいのでカッコイイ、というのはあるが…
 
-静的型付き言語を使っていても、全ての保証したいことが静的型システムで保証できるわけではない。
+静的型付き言語を使っていても、全ての保証したいこと、特にプログラムを動かせば私が大金持ちになってイケメンになっている、とか、が静的型システムで保証できるわけではない。
 むしろ静的型システムで保証できることは非常に限られている。その上、保証したいことを強くした場合、
-型システムが非常に難解になったり、プログラムに沢山型を書かなくてはいけなくなったり、いろいろと
-使いにくくなってくる。
+型システムが非常に難解になったり、プログラムに沢山型を書かなくてはいけなくなったり、
+いろいろと使いにくくなってくる。
 「静的型ぁ?あいつら静的型で強い安全とか言ってるけど何が保証できるってんだよ?馬鹿?」
 とか仰る静的型付けの無い括弧の多い言語使用者がままいらっさるが、そういう意味である。
 そんな時は静的型付き言語使用者ももちろん動的な検査を行う。それは文字通り動的型検査と呼ばれたり、