Software Engineering Lecture 5/19

Menu Menu

先週の復習

集合の表し方
写像、関数
論理
プログラムの意味
Perlを実行して見る

動けば良いだけのプログラミングから、良いプログラムへ

動かせるだけが精一杯、人のプログラムをコピーして手直し。それでいいのか?

例えば、「プログラム書法第二版」Brian W.Kernighan ISBN4-320-02085-5 C3041 は、Fortan を使ったすごく古い本だが、今でも有効な規則が多く載っている。

ライブラリ関数を使おう

効率のために、わかりやすさを犠牲にしてはいけない

多方向の枝分かれをつくる時には if..else if. else を使おう

プログラムが簡単になるようなデータの表現を選ぼう

第一版ができたところでやめてしまってはいけない。

だめなプログラムを修正するのはやめて、全部書き直そう

大きいプログラムは小部分ごとに書き、テストするようにしよう

入力の妥当性、現実性をテストしよう

読み合わせのしやすい入力形式を選ぼう

入出力はサブルーチンの中に閉じ込めよう

すべての変数を使う前に忘れずに初期化しよう

虫取り向きのコンパイラを使おう

プログラムを境界値でテストしよう

0.1の10.0倍は1.0にはならない

速くする前に正しくしよう

速くしたかったら単純さを保とう

プログラムをひねくりまわすのはやめて、もっと良いアルゴリズムをみつけよう

注釈とプログラムを一致させよう

意味のある変数名を使おうもちろん、今となっては、まちがっている規則もたくさんある。「一時変数はなるべく使わない」なんていう規則はもはや時代遅れだといえる。

良いプログラムとは何か?

どんなにきれいに書いてあり、どんなに規則に従っていても、間違ったプログラムは、良いプログラムとはいえない。

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

仕様は論理式により記述し、プログラムはそれを関数を使って実現する。プログラムが正しく仕様を満たしているかどうかを調べる方法はいろいろある。一つは、プログラムのステートメントごとに、その前後で満たしている性質を論理式で記述する方法である。これは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 によるプログラムの検証の重要な部分になる。これを使って理論的にはほとんどのプログラムを正しさを証明することができるはずである。でも、実際にやってみると、

すごく手間がかかる
この証明自身にバグないともいいきれない
有限な入出力に対してしか有効で無い

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

さらに、正しく動作するかどうか決定できないプログラムがある言うことががゲーデルによって示されている。なので、プログラム検証には本質的な限界がある。

問2

このプログラム検証の限界と、最初にあげたプログラミングの規則にはどういう関係があるのか300文字程度で記述せよ。

Perlの構文

条件文

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

練習1

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

制御構造

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

練習2

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

subroutine の作り方

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

これら、相互の型の変換は、整合性が損なわれないように、極めて自由に設定されている。例えば、

      $a = @a;
      ($a,$b,@c) = (1,2,3,4,5,6);
      print "yes\n" if($a) ;
      $c = ("12"."23") + 1;

Perlのデータ構造のマニュアルを見て、Perl のデータ構造を理解しよう。

練習4

上の例で、どのような型変換が起きているのかを指摘せよ。

宿題

Perlのような型を記号で明示する方法と、Cのように型を宣言して指定する方法の利点と欠点について、実例を用いて5個程度考察すること。300文字程度で考察せよ。

Perl の宿題は、メールでSubjectを

    Subject: Report on Software Engineering Lecture 5/9 <br>

として提出すること。この講義の問題を提出する時には、

    Subject: Practice on Software Engineering Lecture 5/9 <br>

とすること。

記号	意味
$a	スカラ (0次元の値)
@a	配列全体ベクタ (1次元の値)
$a[1]	配列の値
%a	連想配列全体
$a{1}	連想配列の値
<a>	ファイルハンドル
&a	手続き呼び出し
\$a	参照の取り出し
$$a	参照の値
()	リスト
[]	無名の配列
{}	無名の連想配列
--	真理値は、if(), while()などで使われる