Software Engineering Lecture 5/11

先週の復習



Perlの構文

条件文

  1. if ($i++ <10 ) { print $i; }
  2. print $i if ($i++ <10 );
  3. print $i unless ($i++ > 9 );
  4. open(FD,"<test") || die("error $@\n");
  5. open(FD,"<test") or die("error $@\n");

練習1

それぞれの条件文をdebuggerで動作を確認せよ。

制御構造

  1. while(<>) { $i++; }; print $i;
  2. print $_ while(<>);
  3. while(<>) { print $_; last if ($i++ > 10); }
  4. while(<>) { next if ($i++ < 10); print $_; last if ($i++ > 20); }
  5. while(<>) { print if (10..20); }
  6. do { print "$i\n"; } until($i++ < 10) ;

練習2

それぞれの制御構造をdebuggerで動作を確認せよ。

subroutine の作り方

sub gcd0 {
    my ($a,$b) = @_;
    return ($a > $b) ? $a % $b : $b % $a;
}

練習3

gcd0 の役割をdebugger で確認せよ。

perldoc

Perldoc の使い方を調べよう。

$@ などの意味

特別変数の使い方を理解しょう。$_, @_, $@ とは何か?


正しいプログラムかどうかを調べる

仕様は論理式により記述し、プログラムはそれを関数を使って実現する。 プログラムが正しく仕様を満たしているかどうかを調べる方法はいろいろある。 一つは、プログラムのステートメントごとに、その前後で満たしている性質を 論理式で記述する方法である。これは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 の前後で保存されている。このようなものを、不変式という。

問1

gcd を計算するプログラムをPerlで記述し、不変式が実際に保存されている ことをdebuggerでチェックせよ。



実際にはループの間で、どのような不変式が成り立つかを見付けることが、 Hoare logic によるプログラムの検証の重要な部分になる。 これを使って理論的にはほとんどのプログラムを正しさを証明することがで きるはずである。でも、実際にやってみると、

などの問題があって、実用的でない。だからといって勉強しなくても良いわけでは ない。(参考文献: プログラム検証論 林 晋 共立出版 ISBN4-320-02658-6)



型 type

より実用的に使われている方法は、型を使った検査である。 これは、プログラムが「正しい」ことを保証するものではないが、 ある決まった範囲内での整合性を保証する。

プログラミング 言語は、変数などに格納できる値の形式が決まっているのが普通である。 その基本的な形を組み合わせることにより、より複雑なデータ構造を 作ることができる。例えば、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で宣言する例題を作れ。

  1. char *
  2. int *(float,char *)
  3. int (*[])()
C言語で以下の型が整合するように、タイプ変数A,B,Cに適合する型を決めよ。
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のデータ型

Perlでは、変数には型を表す記号が付けられている。これには、 以下のようなものがある。

Perlの型を表す記号
記号意味
$aスカラ (0次元の値)
@a配列全体 ベクタ (1次元の値)
$a[1]配列の値
%a連想配列全体
$a{1}連想配列の値
<a>ファイルハンドル
&a手続き呼び出し
--真理値は、if(), while()などで使われる
$a には、数値、文字列、参照などが入る。

これら、相互の型の変換は、整合性が損なわれないように、極めて自由に 設定されている。例えば、 
      $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/11
として提出すること。この講義の問題を提出する時には、 Subject: Practice on Software Engineering Lecture 5/11
とすること。