仕様は論理式により記述し、プログラムはそれを関数を使って実現する。 プログラムが正しく仕様を満たしているかどうかを調べる方法はいろいろある。 一つは、プログラムのステートメントごとに、その前後で満たしている性質を 論理式で記述する方法である。これは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)}
この場合は、gcd(a,b)=gcd(x,y) というのがstatement a:= a mod b
の前後で保存されている。このようなものを、不変式という。
実際にはループの間で、どのような不変式が成り立つかを見付けることが、 Hoare logic によるプログラムの検証の重要な部分になる。 これを使って理論的にはほとんどのプログラムを正しさを証明することがで きるはずである。でも、実際にやってみると、
より実用的に使われている方法は、型を使った検査である。 これは、プログラムが「正しい」ことを保証するものではないが、 ある決まった範囲内での整合性を保証する。
プログラミング 言語は、変数などに格納できる値の形式が決まっているのが普通である。 その基本的な形を組み合わせることにより、より複雑なデータ構造を 作ることができる。例えば、Perl では、
整数 32bit 小数 double 64bit 文字列 "abcd" 真理値が基本的なデータ構造であり、これが型を構成している。これらを組み合わせた ものとして、
配列 $array[5]
連想配列 $array{'a'}
などがある。Perlでは、データ構造はObjectを定義することや、TIEと
呼ばれる連想配列の機能の拡張
によりさらに拡張
可能である。
(型とObjectにどういう関係があるかは、まだ研究途中の話題である)
型は集合ととらえることもできる。あるいは、入力が、その範囲を 満たすと言う論理式だと考えることもできる。後者のようにとらえ ると、Hoare logicのpre condtion/post conditionとして型を使う こともできる。こうすると、プログラムの値を問題にしないので、 Hoare logicの検証は簡単になり、実際にコンパイル時にチェック することが可能になる。
型には包含関係がある。例えば、整数は 小数の部分集合である。 もちろん、整数の配列は、小数の配列の部分集合である。 包含される型からの包含する型への代入は安全であるが逆は 危険である。
代入や 関数の値を渡す時に、型の変換をおこなうことができるが、この時 に、その変換が正当なものかを調べることがおこなわれる。より大 きな集合に変換する場合をup cast、より小さい集合に変換する場 合をdown cast という。down cast では情報が失われる可能性があ る。(だから、down castに文句をいうたこなコンパイラも存在する ようだ)
classで作ったデータの型の包含関係はさらに複雑になる。この複雑な 関係を調べたり、どうやって作りあげていくかを調べることが、オブジェクト 指向設計の重要な役目の一つである。
Perlでは、型付けは非常に弱く、積極的に型変換が行なわれる。これは、 便利な一方で、間違いの元になりやすいので注意を要する。一般に、強い 型付けの言語は、時間がかかるが安全性の高いプログラミングを提供し、 弱い型付けの言語は速いが安全性の低いプログラミングを提供する。
型の整合性の検査には、Unification (単一化)という方法が知られている。 この方法では特に、一部に不定の型があった時に、その型に関する特殊化 の度合いも知ることができる。不定の型は「タイプ変数」とも呼ばれる。
C++ ではテンプレートと呼ばれる機能により限られた意味でのタイプ変数を 使うことができる。MLと呼ばれる言語では、タイプ変数と型の単一化が 積極的に使われており効果を挙げている。MLは計算理論のグループの間では 良く使われている。
C言語で以下の型は何を表すのか。日本語または英語で説明せよ。 また、その型をtypedefで宣言する例題を作れ。
| 4 | char * | char A |
| 5 | int *(float,char *) | A (float,char *) |
| 6 | int (*[])() | B [] |
| 7 | int (*)() | B * |
| 8 | A (A *, char *) | (B *) (B ** ,C) |
Perlでは、変数には型を表す記号が付けられている。これには、 以下のようなものがある。
| 記号 | 意味 |
| $a | スカラ (0次元の値) |
| @a | 配列全体 ベクタ (1次元の値) |
| $a[1] | 配列の値 |
| %a | 連想配列全体 |
| $a{1} | 連想配列の値 |
| <a> | ファイルハンドル |
| &a | 手続き呼び出し |
| \$a | 参照の取り出し |
| $$a | 参照の値 |
| () | リスト |
| [] | 無名の配列 |
| {} | 無名の連想配列 |
| -- | 真理値は、if(), while()などで使われる |
$a = @a;
($a,$b,@c) = (1,2,3,4,5,6);
print "yes\n" if($a) ;
$c = ("12"."23") + 1;
Perlのような型を記号で明示する方法と、Cのように型を宣言して指定する 方法の利点と欠点について300文字程度で考察せよ。
Perlの型の変換について、実例を用いて5個程度考察すること。
Perl の宿題は、メールでSubjectを
Subject: Report on Software Engineering Lecture 5/12
として提出すること。この講義の問題を提出する時には、
Subject: Practice on Software Engineering Lecture 5/21
とすること。