* 2 ホーア論理入門
** 2.1 表明付きプログラム
- ホーア論理では、表明付きプログラム(asserted
program)というものを書く。
{A}P{B}
<A>P<B>
のごとく。Pはプログラム本体であり、それを囲むも
のは一種の仕様(そのプログラムに関する)である。
- Aを前条件(precondition)、Bを後条件
(postcondition)と言う。
- <A>P<B>は、Pが停止し、どちらも真になることで全
体が真となる。(完全正当性)
- {A}P{B}は、Pが停止たときにA,Bどちらも真になると
きに真であり、Pが停止しないときも真である。(部
分正当性)
** 2.2 表明とコメント
- 表明って、コメントで関数の入出力仕様を書くのと
同じだよね。
** 2.3 部分正当性と完全正当性
- 完全正当性 = 部分正当性 + 停止性.
- ホーア論理では、主に部分正当性を扱う。
** 2.4 表明付きプログラムの正しさの証明
- 表明付きプログラムの正しさの証明は、公理と推論
規則にて実施する。
*** 2.4.1 正しさの証明とプログラムの分割
- プログラムは部分的なプログラムから出来ている。
- ホーア論理は部分的なプログラムの正しさを証明で
きれば、プログラム全体の正しさが証明されるよう
になっている。
- Common Lispにとってホーア論理ってどうなのかなぁ。
*** 2.4.2 複合文の正しさ
- 分割しやすいようにver2を書き換える。
---
;; { 整数x,yの少なくとも一方はゼロでない。 }
(defun gcd-ver2 (x y)
(progn
(setf a x)
(setf b y)
(while (/= b 0)
(progn
(setf a (mod a b))
(setf c a)
(setf a b)
(setf b a)))
(if (> a 0)
a
(- a))))
;; {変数aの値はxとyの最大公約数である。}
---
- こいつを分割した。
---
;; AP1:
;; {整数x,yの少なくとも一方はゼロでない。}
(setf a x)
;; {変数aの値はxである。
;; ただし、整数x,yの少なくとも一方はゼロでない。}
;; AP2:
;; {変数aの値はxである。
;; 整数x,yの少なくとも一方はゼロでない。}
(setf a x)
;; {変数a,bの値はlx,yである。
;; ただし、整数x,yの少なくとも一方はゼロでない。}
;; AP3:
;; {整数a,bの値はx,yである。
;; ただし、整数x,yの少なくとも一方はゼロでない。}
(while (/= b 0)
(progn
(setf a (mod a b))
(setf c a)
(setf a b)
(setf b a)))
;; {|a|はxとyの最大公約数である。}
;; AP4:
;; {|a|はxとyの最大公約数である。}
(if (> a 0)
a
(- a))
;; {変数aの値はxとyの最大公約数である。}
---
- ホーア論理：複合文の規則
この本のもの
{A}P1{S1}...{Sn-1}Pn{B}
-------------------------
{A}begin P1;...;Pn end{B}
Common Lisp用
{A}P1{S1}...{Sn-1}Pn{B}
-------------------------
{A}(progn P1 ... Pn){B}
*** 2.4.3 代入文の正しさ
- ホーア論理：代入文の公理
この本のもの
{A[t/a]} a := t {A}
Common Lisp用
{A[t/a]} (setf a t) {A}
- うお。公理なのね。
- A[t/a]は、表明Aの中の項aをtで置換えたもの。
- この公理の形でAP1の代入を書いてみよう。
;; AP1:
;; {変数xの値はxである。
;; ただし、整数x,yの少なくとも一方はゼロでない。}
(setf a x)
;; {変数aの値はxである。
;; ただし、整数x,yの少なくとも一方はゼロでない。}
- になるらしい。これなんか変？ しらべる。
- A[x/a]は、表明Aの中の項aをで置換えたもの。
- そうすると表明Aはなんだっけ？となる。
- 表明Aは後条件のことだからそれにしたがっ
て書く。
A は {変数aの値はxである。
ただし、整数x,yの少なくとも一方はゼロでない。}
- そうすると、後条件から導き出した前条件は、
A[x/a] は {変数xの値はxである。
整数x,yの少なくとも一方はゼロでない。}である。
- なので常に真となる代入文の形で、これらを書くと、
;; {変数xの値はxである。
;; 整数x,yの少なくとも一方はゼロでない。}である。
(setf a x)
;; {変数aの値はxである。
;; 整数x,yの少なくとも一方はゼロでない。}である。
- 変数xの値がxであるのは自明とすれば、これはAP1と
同じである。よって、AP1は正しい。
- うーん。だからどーした、という感じ。
- AP2についてやってみる。
AP2は、
;; AP2:
;; {変数aの値はxである。
;; 整数x,yの少なくとも一方はゼロでない。}
(setf b )
;; {変数a,bの値はx,yである。
;; ただし、整数x,yの少なくとも一方はゼロでない。}
である。これが正しいことを証明する。証明はこのAP2
が代入文の公理の形式として適格であることによって示
す。
まず後条件Aは次のとおりである。
;; {変数a,bの値はx,yである。
;; ただし、整数x,yの少なくとも一方はゼロでない。}
代入文はbにyを代入しているので、前条件はこれのbをx
に変えたものである。
;; {変数a,yの値はx,yである。
;; ただし、整数x,yの少なくとも一方はゼロでない。}
変数yの値がyのことは自明なので、この前条件は次のも
のと同じと考えてよい。
;; {変数aの値はxである。
;; ただし、整数x,yの少なくとも一方はゼロでない。}
これはAP1の前条件と同一である。ゆえにAP1は代入文の
公理にすぎない。よってこれは真である。
*** 2.4.4 表明の置き換え
- ホーア論理:帰結規則
AならばB {B}P{C} CならばD
-------------------------
{A}P{D}
*** 2.4.5 while文の正しさ
- ホーア論理:while文の規則
{"式tの値は真" and A}P{A}
--------------------------------------
{A} while t do P {"式tの値は偽" and A}
- Aはループ不変表明と呼ぶ。こいつがポイント。これ
に何をえらぶかでwhileの正しさを証明できるかどう
かがきまる。ここでは、
gcd(a,b) = gcd(x,y)
を選ぶ。
するとwhile文の規則の前条件は、
;; {"式(/= b 0)の値は真" and gcd(a,b) = gcd(x,y)}
(progn
(setf a (mod a b))
(setf c a)
(setf a b)
(setf b a))
;; {gcd(a,b) = gcd(x,y)}
となる。このPは地道に計算をすれば正しいことがわか
る。そこで、これを推論規則にしたがってゴールに変
換する。
;; {gcd(a,b) = gcd(x,y)}
(while (/= b 0)
(progn
(setf a (mod a b))
(setf c a)
(setf a b)
(setf b a)))
;; {"式(/= b 0)の値は偽" and gcd(a,b) = gcd(x,y)}
これは推論規則により正しいプログラムである。さて、
この後条件は、b = 0なので、gcd(a,b)が|a|になるこ
とから、AP3と同じである。よって、AP3も正しい。
*** 2.4.6 条件文の正しさ
- whileよりは簡単だ。
{"式tの値は真" and A}P{B}
---------------------------
{A}if t then P fi{B}
{"式tの値は真" and A}P{B} {"式tの値は偽" and A}Q{B}
-----------------------------------------------------
{A}if t then P else Q fi{B}
- Common Lisp版は割愛。
- 推論規則で、このように併記される場合は、andの意
味かな。
** 2.5 whileプログラムのホーア論理
- 複合文、代入文、while文、条件文だけでできている
プログラムをwhileプログラムと言う。
*** 2.5.1 合成性
- ホーア論理(の照明)は、部品の正しさに還元できる。
これを合成性と呼ぶ。
*** 2.5.2 公理・推論規則と文の対応
- ホーア論理の使い方の整理。
- まず、帰結規則以外の規則は逆向き推論の方法は
確定している。よって、プログラムをホーア論理
で分析するときの初手として、プログラムを部品
に分解していくわけだが、その分解する単位とい
うか分解の仕方はまあ決まってしまうということ。
- ただし、分解した後に間をつなぐ前条件とか後条
件を部品につけるわけだが、これは発案しなけれ
ばいけない作業。
- また、whileに対するループ不変量も発見しなけれ
ばいけないものである。
- まとめると、プログラムの書きぶりを反映した分解
と、各種条件(表明)を発見的に立案する作業(ここ
で必要に応じて帰結規則をつかる)が第一ステップ
として存在する。
- あとは、立案した表明が正しいこと証明できるか
どうかである。それが証明できれば、プログラム
の正しさは証明されたことになる。
** 2.6 完全正当性の証明
- while文の規則以外は部分正当性の規則と公理がその
まま適用できる。まあ、ループ無いしね。
- while文の規則の完全正当性版。
<bound = n and "式tの値は真" and A>P<bound < n and A>
-------------------------------------------------------
<A> while t do P <"式tの値は偽" and A>
ここで、boundは非負整数を表す式(数学的な式でよい)
であり、nは非負整数を表わす変数である。nはPの中に
登場してはいけない。
- これを自分なりに読む。これは、停止するwhileは上
段のように書けるということを教えてくれている。逆
にこの上段のように書けなければ、そのwhileが停止
するかどうかはわからない。さて、上段のように書け
るということはどういうことなのか読み解く。それは、
Pの処理に絡み仮にboundと呼ぶ非負の量が存在してい
ることをまず求めている。そのboundという量は、Pの
処理によって処理前より小さくなるというような量だ。
かつ負にはならないことも条件付けされている。さて、
そういう量が実際に存在したとしよう。下段に目を移
すと、それはPの背後にいる隠れた値とも考えられる。
処理Pを下段のようにwhile文で繰返し実行したとする。
すると隠れた変数boundは、Pを一回処理するごとに小
さくなり、かつ非負である。さて、具体的にnが何で
あるかは、boundの定義によるわけだが、上段が常に
成立するといことは、bound = 0ということが起り得
ないということであるから？、下段のwhile文は停止
すると言える。？？？ なんだかよくわからん。
*** 2.6.1 ループの限度についての注意
- うーん。Lispのプログラミングだと、ループを再帰で
書くときに、再帰が必ず停止するように注意するこ
とに相当すると思うんだけど、なんかそれを回りく
どく扱っているように思える。
- ループ不変量についても、第一義にはproperly tail
recursiveに書けますか、というような気がする。た
だ、properly tail recursiveじゃなくてもループ不
変量が存在するというならばそれはおもしろい事実
ではある。
** 2.7 ホーア論理の能力
*** 2.7.1 whileプログラムの相対完全性
- うーん。よくわからん。ホーア論理の実体が何であっ
て、それが証明する正しさが何かがいまいちピンと
こない。だからwhileプログラムの相対完全性もピン
とこない。これは形式化をやればいいかな、という
ことで次章に送る。
*** 2.7.2 ホーア論理とプログラム検証の限界
- Algol-likeの意味にびっくりした。
- 1.手続き定義可能。局所手続きも定義可能。
- 2.手続きを引数として渡せる。
- 3.再帰呼び出し可能。
- 4.静的スコープが可能。
- 5.大域変数可能。
- Algol記法というのは文とコードブロックを多様する
統語論に対するものだと思うが、言語機能で言うと、
Algolって普通に関数プログラミングができる言語な
んですね。
ホーア論理は命令型プログラミングを対象としていることがわかった。
こつこつ。
0 件のコメント:
コメントを投稿