仕様は論理式により記述し、プログラムはそれを関数を使って実現する。 プログラムが正しく仕様を満たしているかどうかを調べる方法はいろいろある。 一つは、プログラムのステートメントごとに、その前後で満たしている性質を 論理式で記述する方法である。これはHoare logic と呼ばれる。
{Pre Condition}
S
{Post Condition}
例えば、
{b!=0 ∧ gcd(a,b) = gcd(x,y)}
a := a mod b
{gcd(a,b)=gcd(x,y)}
これを使って理論的にはほとんどのプログラムを検証することがで
きる。でも、実際にやってみると、
より実用的に使われている方法は、型を使った検査である。プログラミング 言語は、変数などに格納できる値の形式が決まっているのが普通である。 その基本的な形を組み合わせることにより、より複雑なデータ構造を 作ることができる。例えば、Java では、
整数 byte 8bit
short 16bit
int 32bit
long 64bit
小数 float 32bit
double 64bit
文字 char 16bit
真理値 boolean true/false
が基本的なデータ構造であり、これが型を構成している。これらを組み合わせた
ものとして、
配列 array[] 文字列 Stringなどなどがある。Javaでは、データ構造はclassを定義することにより拡張 することになっている。その意味では、Javaでは、class = 型ということも できる。
型は集合ととらえることもできる。あるいは、入力が、その範囲を 満たすと言う論理式だと考えることもできる。後者のようにとらえ ると、Hoare logicのpre condtion/post conditionとして型を使う こともできる。こうすると、プログラムの値を問題にしないので、 Hoare logicの検証は簡単になり、実際にコンパイル時にチェック することが可能になる。
型には包含関係がある。例えば、int は long の部分集合である。 もちろん、short の配列は、longの配列の部分集合である。代入や 関数の値を渡す時に、型の変換をおこなうことができるが、この時 に、その変換が正当なものかを調べることがおこなわれる。より大 きな集合に変換する場合をup cast、より小さい集合に変換する場 合をdown cast という。down cast では情報が失われる可能性があ る。(だから、down castに文句をいうたこなコンパイラも存在する ようだ)
classで作ったデータの型の包含関係はさらに複雑になる。この複雑な 関係を調べたり、どうやって作りあげていくかを調べることが、オブジェクト 指向設計の重要な役目の一つである。
宿題