* 1 プログラムの検証
** 1.1 本書の目指すところ
- プログラムの正しさ、ということ自体を明確にする。
- 形式的技法(実用可能なプログラム検証論)への入口
になる。
** 1.2 プログラム検証論の目的
- プログラマが、自分が正しく作ったと言っても正し
さの証明にはならない。
- 権威あるアルゴリズムを使っているから大丈夫、と
言っても正しさの証明にはならない。
- ソースコードを単純に開示するだけでは、正しさの
証明にはならない。(それを見る人がどう見るかにも
よるが)
- テストは検証の手法のひとつであるが、正しさの証
明にはならないことが多い。
- お題としてのGCD。
GCD プログラム ver.1:
---
begin
a := x; b := y;
while b != 0 do
a := a mod b;
c := a; a := b; b := c
end
end
---
これ、言語、なんだろ？ Pascal?
- ユークリッドのアルゴリズムって何だっけ？
- ユークリッドの互除法
- 2つの自然数m,nの最大公約数を求める。
- m>nとする。
- m = q0 n + r1 (0 <= r1 < n)
- とする。
- r1 が0でなければ、次のようにする。
- n = q1 r1 + r2 (0 <= r2 < r1)
- 同様のことを続ける。
r1 = q2 r2 + r3 (0 <= r3 < r2)
r2 = q3 r3 + r4 (0 <= r4 < r3)
- r1>r2>...なので、今、自然数について扱っている
ことからrk>0,rk+1 = 0となるkが存在する。
rk = qk rk
このqkが、m,nの最大公約数である。
- 自分なりの言葉でポイントを。
- m = q0 n.であればnが最大公約数だよね。
- m = q0 n + r1.と余りがでちゃった。
- そうすると、m,nの最大公約数というのは、nとr1の
最大公約数になる。なんで？ それをgとすれば、
- m = q0 a g + b g.
= (q0 a + b) g.
になるから、mもgで割り切れる。で、gを1でも大き
くしたら、mは割り切れない。なぜかというそれが、
gがn,r1の最大公約数ということだから。
- なるほど。再帰的なんだな。
- Common Lispで書いてみる。
---
(defun mygcd (m n)
(if (> m n)
(gcd-aux m n)
(gcd-aux n m)))
(defun gcd-aux (m n)
(let ((r (mod m n)))
(if (= r 0)
n
(gcd-aux n r))))
---
とか。
---
(defun mygcd2 (m n)
(labels ((g (a b &optional (r (mod a b)))
(if (= r 0)
b
(g b r))))
(if (> m n)
(g m n)
(g n m))))
---
とか。サンプルをそのままCommon Lispにもってくると、
---
(defun gcd-ver1 (x y)
(let ((a x)
(b y))
(while (/= b 0)
(setf a (mod a b))
(setf c a
a b
b c))
a))
---
とか。そうか、引数の大小は一回目のmodで対処される
んだな。
** 1.3 プログラムの正しさを証明する
- で、これらプログラムが最大公約数を計算すること
を数学的に証明したい、ということ。
- うーん。この本に書かれている例がプログラムの動
作の証明、なのか。。。まあ確かに数学の証明っぽ
い感じはするが。なんか釈然としない。
- というのは、やはり、もともとそういう証明を考え
ることがプログラムを作るときに考えることじゃな
いかなぁ、というのがあり。
- さて、負の整数に対する公約数の定義は何だろう。
- まず除法定理。
- 任意の整数a,b(b>0)に対して、a = q b + r (0 <= r
< b)となる整数q,rがただ一組存在する。
qを、aをbで割った商(quotient)、rを剰余
(remainder)と呼ぶ。
- 次に、約数の定義。
- a,b(b/=0)について、a = q bとなる整数qが存在する
とき、bはaの約数であるという。
- 次に、最大公約数の定義。
- どれかは0でない整数a1,...,anの共通な約数を公約
数といい、正の公約数のうちで最大のものを最大公
約数と呼ぶ。
- すると、a,bともに正の場合は簡単だが、負が入る場
合はどうなるのかな。a,b(a<0,b>0)の場合、a = q b
だとすると、qも負であるがこの式は成立しているこ
とは間違いない。すると、b = 1 bでもあるからbは
a,bの公約数である。これしか公約数が無いとき、こ
れを最大公約数と呼びたくなるが、最大公約数の定
義によると資格があるのは正の公約数だけではない
か。こまった。
- 以上は岩波数学辞典の話。
- そこで、CRC Encyclopedia of Mathematicsをみる。
- こちらはgcdは正の整数について、と定義されている。
- 情報処理ハンドブックにはgcdのエントリが無い。
- うむー。困ったもんだ。
- ここでは、著者の言うとおり、負の整数が絡む最大
公約数は正負を逆転させると鵜呑みにしよう。
---
(defun gcd-ver2 (x y)
(let ((a x)
(b y))
(while (/= b 0)
(setf a (mod a b))
(setf c a
a b
b c))
(if (> a 0)
a
(- a))))
---
- ところで気になるのが、剰余定理とCommon Lispの
modとremの関係。
- ためす。
CL-USER(18): (mod -7 3)
2
CL-USER(19): (rem -7 3)
-1
- すると
-7 = -3 * 3 + (mod -7 3)
-7 = -2 * 3 + (rem -7 3)
であるから、剰余としてはmodがばっちり。よかった。
** 1.4 仕様：正しさの基準
- おお、公約数って負の整数についても存在するのね。
- ソフトウエアは要求を満足しなければいけない。
- 要求に合わない仕様は間違いである。
- 要求に合わない仕様に基づくプログラムは間違いで
ある。
- 要求に合う仕様に基づかないプログラムは間違いであ
る。
- 要求に合わない仕様に基づかないプログラムは間違い
であるかどうかはわからない。
- この本では仕様に対するプログラムの正しさだけを
扱う。ちなみに形式的手法では、仕様の正しさもプ
ログラムと同等以上に扱う。
** 1.5 本書の組み立て
- 特になし。
こつこつ。
0 件のコメント:
コメントを投稿