BYOB によるホーア論理入門∗
神戸大学人間発達環境学研究科
高橋真

この資料はビジュアルプログラミング環境の BYOB(Build Your Own Blocks)1 を利用してホーア論理の初歩を分かりやすく解説することを目的としています．

∗
1

この資料は JSPS 科研費 23650507 の助成を受けた研究の過程で得られたものです．
http://byob.berkeley.edu/

1 BYOB プログラムの正当性

計算機数学講義資料 2016

BYOB プログラムの正当性

1

プログラムを作成するときに気をつけることというと、まず思いつくのは間違いのない
プログラムを作成することであろう．間違いのないプログラムというときには、何をもって間違いがないと判断するのであろうか．通常は、何か目的をもってプログラムを作り、プログラムを動作させて必要な情報を手にいれるのである．従って、プログラムを動かしたときに、止まらなかったり2 或いは止まっても目的と違う結果が出てきたのでは困り、そのようなプログラムは 正しい プログラムとは呼べない．プログラムが正しいとか間違っているとか言うときには、このように前もってプログラムに求めるものが決まっている．それをまとめたものを仕様 (speciﬁcation) と呼ぶ．言い替えるとプログラムの正しさとは仕様に対して決まるのである3 ．
『プログラムの正しさは仕様に対して決まる』とはどのようなことか次の BYOB のプ
ログラムを例にとって考えよう．

このプログラムは、正整数 x と y の最大公約数を求める関数ブロックである．変数 x と yの値を与えてブロックをクリックすると、変数 a の値が報告されそれが x と y の最大公約
数になる．

2
3

ここでは止まらないことが求められるプログラムは除外している．
この章の内容は文献 [1] を参考にしている．

1

1 BYOB プログラムの正当性

計算機数学講義資料 2016問題 1.1 入力 x = 145, y = 35 に対し出力は 5 であることを変数表を書いて確かめよ．
しかし、これで本当に最大公約数が求められているのであろうか．適当な値を x と y に与えると、確かに a の値は最大公約数になっているが 本当に 任意の値に対して最大公約数を求めているのか．変数 x と y に負の整数を与えたとき、上のプログラムはどういう結果を出力するだろうか．

上のプログラムは整数 x と y の最大公約数を求めるプログラムとすると間違いである．
少なくとも一方が 0 ではない整数 x と y の最大公約数を求める正しいプログラムはとしなければならない．

2

1 BYOB プログラムの正当性

計算機数学講義資料 2016

最初のプログラムは、正整数に対して最大公約数を求めるという仕様に対しては正し
いが、すべての整数に対して最大公約数を求めるという仕様に対しては正しくないのである．
BYOB プログラムで関数ブロックを入れて議論すると複雑になるので、この授業では次のような BYOB のプログラムに対しての 正しさ について考察する．

1. 式とはレポーター型のブロックで次のように再帰的に定義する．

2. ブール式は述語型のブロックで次のように再帰的に定義する．

3. プログラムはコマンド型のブロックで次のように再帰的に定義する．それぞれ代入
文，複合文，条件文，until 文とよぶ．

定数や変数の定義がないが，任意の自然数を定数として扱え，変数は整数を値にもつもので BYOB で定義できるものとする．特に変数の値が整数であることに注意が必要な場
合を除き，今後変数の値が整数であることは特に言及しない。
以上の BYOB プログラムの構成的な定義に従うと、BYOB プログラムが 正しい ということを証明方法として，構造に関する帰納法を適用することが考えられる．しかし、

3

1 BYOB プログラムの正当性

計算機数学講義資料 2016

上で述べたようにプログラムが正しいとか正しくないというのは、仕様抜きでは考えられない．
そこでホーア論理とよばれるプログラムの正しさを検証するための論理学的方法が考えられた．ホーア論理では表明つきプログラムというものを使って、プログラムが仕様を満たすということを表現する．
A, B を何らかの条件を表わす（論理）式、P をプログラムとする．

〈A〉 P 〈B〉 {A} P {B}のように表現されたものを表明つきプログラム、A を事前表明、B を事後表明とよぶ．事
前表明事後表明をあわせて単に表明とよぶ．P の前後に表明をつけることで P に対する仕様を表現しているのである．仕様のわからないプログラムに対しては 正しい とか 正
しくない ということは何も言えなかったが、表明つきプログラムに対しては定義可能である．〈A〉 P 〈B〉 、 {A} P {B} が正しいということをそれぞれ次のように定義する．
〈A〉 P 〈B〉 が正しいとは、A が成り立っているときにプログラム P を実行すると、その実行は停止し、さらに停止後 B が成り立つときをいう．
{A} P {B} が正しいとは、A が成り立っているときにプログラム P を実行するとき、もし実行が停止するならば停止後 B が成り立つときをいう．
（従って、P の実行が停止しない場合は{A} P {B} は正しいと考える．
）
前者にはプログラムの停止性が含まれているが、後者には含まれていない．〈A〉 P 〈B〉を完全正当性、{A} P {B} を部分正当性とよぶ．
以上のように表明付き BYOB プログラム {A}P {B} を定義することにより，それらが正しいことをプログラムの構成に関する帰納法で証明することが可能になる．具体的には、代入文の公理から複合文、条件文、until 文の推論規則及び帰結の推論規則を用いて証明をする．
（BYOB プログラムのホーア論理の健全性：証明可能なものは正しい）
BYOB のプログラムをそのまま記載すると見にくいため，今後次のように BYOB のプ
ログラムを略記することにする．
代入文

は x := t， 複合文

条件文

は if A then P1 else P2 ﬁ，

until 文は until A do P1 od

は P1 ; P 2 ，で表すことにし，場合により BYOB プログラムを記載することにする．
また，

4

2 代入文の公理と帰結の規則

計算機数学講義資料 2016は A ∧ B,は A ∨ B,は ¬Aで表し，表明の表現にも同じ論理記号 ∧ , ∨, ¬ を用いることにする．
問題 1.2 次の BYOB プログラムを上で述べた略記法により記述せよ。

2

代入文の公理と帰結の規則

例 2.1 {y > 2} x := y + 1 {x > 3}は正しい．
代入文 x := y + 1 の実行前に変数 y の値が 2 より大きいとすると，代入文 x := y + 1 の実行により変数 x の値は y + 1 の値になるから，実行後の x の値は 2 + 1 = 3 より大きくなる．従って，この表明付きプログラム{y > 2} x := y + 1 {x > 3}は正しい．
例 2.2 {x > 5} x := x + 1 {x > 6}は正しい．
代入文 x := x + 1 の実行前に変数 x の値が 5 より大きいとすると，代入文 x := x + 1 の実行により変数 x の値は 1 増加するから，実行後の x の値は 6 より大きくなる．従って，
この表明付きプログラム{x > 5} x := x + 1 {x > 6}は正しい．

5

2 代入文の公理と帰結の規則

計算機数学講義資料 2016

R[x → t] を表明 R(x) の中にある変数 x を式 t ですべて置き換えて得られる表明とする．
例えば，R(x) ≡ [x > x2 + 6] で t ≡ x + 1 のとき，R[x → t] ≡ [x + 1 > (x + 1)2 + 6] である．このような表記法の下で，{R[x → t]} x := t {R(x)} は常に正しい表明つきプログ
ラムである．この理由を考えてみる．代入文 x := t の実行前に R[x → t] が成り立つとする．すなわち，変数 x の代わりに t を考えているので，表明 R(x) 中の x の値を t の値にすると成り立つことになる．x := t を実行すると，変数 x の値は t の値になるので，実行
後に R(x) が成り立つことになる．従って，{R[x → t]} x := t {R(x)} は常に正しい表明
付きプログラムとなる。{R[x → t]} x := t {R(x)} の形の表明付きプログラムを代入文の公理とよぶことにする．
．
注意 {R(x)} x := t {R[t/x]} は正しい表明とはいえない．
例 2.3 {x < 5} x := x + 1 {x + 1 < 5} は正しくない．
（x の値が 4 のときを考える．
）
代入文の公理は，代入文 x := t に関し、任意の事後表明 R に対しそれに適切な事前表明
として R[t/x] がとれることを示している．もちろん、部分正当性の定義から A → R[t/x]が正しい表明ならば、{A} x := t {R} も正しい表明つきプログラムである．
例 2.4• {x + 1 > 1} x := x + 1 {x > 1}

• {x2 > x2 y} x := x2 {x > xy}
問題 2.5 次の代入文と事後表明に対し，代入文の公理となるように事前表明を定めよ．
（式を計算せずに形式的に求める．
）
代入文
事後表明
(a) x := x + 7 x + y > 20(b) x := x − 1 x2 + 2x = 3(c) x := x − 1 (x + 1)(x − 1) = 0(d) y := x + y y = x(e) y := x + y y = x + y
一般に{A} P {B} が正しい表明つきプログラムで C → A, B → D がともに正しい表
明ならば，{C} P {D} は正しい表明つきプログラムである．このことを次のような図式で表し，帰結の推論規則とよぶ．
帰結の推論規則{A} P {B}{C} P {D}(ただし C → A,B → D がともに真のとき)6

3 複合文，条件文，UNTIL 文の部分正当性

計算機数学講義資料 2016

この図式は，C → A,B → D がともに真のときに，{A} P {B} が正しければ，{C} P {D}も正しいことを表す．今後，このようにいくつかの表明付きプログラムから別の表明付きプログラムを導く推論規則を定義するが，そこに現れる図式中の横棒は ∴ と考えれば良い．また帰結の推論規則を用いるとき，C → A,B → D が自明ではないときは，それが成り立つ理由を推論規則の横に記載することにする．
例 2.6{x + 1 > 1} x := x + 1 {x > 1}
{x > 0} x := x + 1 {x > 1}(∵ x > 0 ならば x + 1 > 1))

上式の{x + 1 > 1} x := x + 1 {x > 1}は代入文の公理であるから正しい表明つきプログ
ラムで，下式の{x > 0} x := x + 1 {x > 1}は帰結の規則により導かれている。よって，{x > 0} x := x + 1 {x > 1}も正しい表明付きプログラムである．
問題 2.7 問題 2.5 で求めた事前表明を簡単な事前表明に書き換え，それを事前表明にもつ表明付きプログラムの正しさを代入文の公理と帰結の推論規則を用いて示せ．

3

複合文，条件文，until 文の部分正当性

3.1

複合文の部分正当性

次のような表明付きの複合文を考える．

{a = 2 ∧ b = 3} c := a; a := b; b := c {a = 3 ∧ b = 2}
複合文の実行は前から逐次的に行われるからこれは正しい表明付きプログラムである．我々は表明つきプログラムの正しさをその部分プログラムの正しさから導き出そうと考えている．したがって複合文においても，その部分プログラムの正しさから全体の正しさを導けるように考えたい．上記の例でそのことをみていこう．上の表明付きプログラムでそれぞれの代入文の実行前後で正しくなる表明を考えてみよう．まず，最初の代入文 c := a では変数 c に変数 a の値が代入されるから，{a = 2 ∧ b = 3} c := a {c = 2 ∧ b = 3}は正しい表明つきプログラムである．さらに，これは代入文の公理の形をしていることに注意をしよう．同じように，{c = 2 ∧ b = 3} a := b {c = 2 ∧ a = 3}, {c = 2 ∧ a = 3} b := c {b = 2 ∧ a = 3}
も正しい表明つきプログラムである．最後の表明つきプログラムにおいて b = 2 ∧ a = 3 →a = 3 ∧ b = 2 が常に成り立つから，帰結の推論規則より事後表明を a = 3 ∧ b = 2 に変更
してできる表明つきプログラム7

計算機数学講義資料 2016

3 複合文，条件文，UNTIL 文の部分正当性{c = 2 ∧ a = 3} b := c {a = 3 ∧ b = 2}

も正しい表明つきプログラムである．これを逆に考えるとまず代入文の公理と帰結の推論
規則から，{a = 2 ∧ b = 3} c := a {c = 2 ∧ b = 3}{c = 2 ∧ b = 3} a := b {c = 2 ∧ a = 3}{c = 2 ∧ a = 3} b := c {a = 3 ∧ b = 2}
が正しいことがわかり，このことから最初の表明つきプログラム{a = 2 ∧ b = 3} c := a; a := b; b := c {a = 3 ∧ b = 2}の正しさが判断できるようになる．このように表明付きの複合文{A} P1 ; P2 ; · · · ; Pn {B}が与えられたときにその正しさを証明するには，新たに n − 1 個の表明 S1 , S2 , · · · Sn−1 を適切に選んで{A} P1 {S1 },{S1 } P2 {S2 },· · · ,{Sn−1 } Pn {B}という n 個の表明つきプログラムの正しさを示すことができれば{A} P1 ; P2 ; · · · ; Pn {B} の正しさを証明できることになる．このことをつぎのような推論規則で表すことにする．

{A} P1 {S1 } {S1 } P2 {S2 } · · · {Sn−1 } Pn {B}{A} P1 ; P2 ; · · · ; Pn {B}
例題 3.1 {A} x := x + 1; y := x − y {x < y} が表明付きプログラムとして正しくなる
ように事前表明 A を定めよ．
証明： 代入文の公理より，{x < x − y} y := x − y {x < y} は正しい表明付きプログラム
で，同様に，{x + 1 < x + 1 − y} x := x + 1 {x < x − y} も正しい表明付きプログラムである．従って，A として x + 1 < x + 1 − y をとると，{A} x := x + 1; y := x − y {x < y}は正しい表明付きプログラムとなる．なお帰結の推論規則を用いて，A として，y < 0 をとってもよい．
（こちらの方が適切ではある．
）¤
問題 3.2 次の複合文と事後表明に対し，表明付きプログラムとして正しくなるように事
前表明を定めよ．
複合文
事後表明
2(a) x := x − 1; x := xx>0(b) x := x − y; y := x + y x = 1 ∧ y = 2(c) x := x2 ; y := x + y
x = 1∧y = 28

3 複合文，条件文，UNTIL 文の部分正当性

計算機数学講義資料 2016

例題 3.3 {(x + y)2 > x} x := x + y; y := x − y; x := x2 {x > y} は正しい表明つきプロ
グラムであることを代入文の公理，帰結の推論規則及び複合文の推論規則を用いて示せ．
証明：A ≡ (x+y)2 > x, S1 ≡ x2 > x−y, S2 ≡ x2 > y, B ≡ x > y, C ≡ (x+y)2 > (x+y)−yとおく．C ≡ S1 [x → x + y], S1 ≡ S2 [y → x − y], S2 ≡ B[x → x2 ] である．よって，{C} x := x + y {S1 }{A} x := x + y {S1 } {S1 } y := x − y {S2 } {S2 } x := x2 {B}{A} x := x + y; y := x − y; x := x2 {B}であるから与えられた表明つきプログラムは正しい4 ．

¤

上の証明では代入文の公理に形をあわせるために帰結の推論規則が用いられたことに注意しよう．
問題 3.4 {xy + 1 > 0} x := xy; y := x + 1; x := x + 1 {x + y > 0} は正しい表明つきプ
ログラムであることを代入文の公理，帰結の推論規則及び複合文の推論規則を用いて示せ．

3.2

条件文の部分正当性

次の表明付きの条件文を考える．

{A} if α then P1 else P2 ﬁ {B}
この条件文の実行はブール式 α が真であるか偽であるかにより決まる．α が真のときはP1 が実行され α が偽のときは P2 が実行される．従って，上の表明つきプログラムが正しいものであるためには，A が成り立っているとき，P1 , P2 のいずれの実行においても B が成り立つことが必要である．すなわち，{A ∧ α} P1 {B},{A ∧ ¬α} P2 {B}が正しい表明
つきプログラムのとき，{A} if α then P1 else P2 ﬁ {B} が正しいと判断できる．このことを次のような推論規則を用いて表す．

{A ∧ α} P1 {B} {A ∧ ¬α} P2 {B}{A} if α then P1 else P2 ﬁ {B}
例題 3.5 {x = a ∧ y = b} if x ≥ y then z := x else z := y ﬁ {z = max{a, b}} は正しい表
明つきプログラムであることを代入文の公理，帰結の推論規則及び条件文の推論規則を用
いて示せ．

4

このような図式を証明図 (proof ﬁgure) とよぶ．

9

計算機数学講義資料 2016

3 複合文，条件文，UNTIL 文の部分正当性

証明： z = max{a, b} を A で表す．

{A[z → x]} z := x {A}{A[z → y]} z := y {A}{x = a ∧ y = b ∧ x ≥ y} z := x {A} {x = a ∧ y = b ∧ ¬(x ≥ y)} z := y {A}{x = a ∧ y = b} if x ≥ y then z := x else z := y ﬁ {A}x = a ∧ y = b ∧ x ≥ y ならば max{a, b} = a = x であるから，A[x/z] が成り立つ．また，
x = a ∧ y = b ∧ ¬(x ≥ y) ならば max{a, b} = b = y であるから，A[y/z] が成り立つ．よって，最初の二つの推論は帰結の推論規則の条件をみたす．従って，与えられた表明つきプ
ログラムは公理と推論規則で導かれるので，正しい表明つきプログラムである．
¤
問題 3.6 次の表明つきプログラム正しい表明つきプログラムであることを推論規則を用いて示せ．

1. {x > 5} if x ≤ y then x := x else c := x; x := y; y := c ﬁ {x ≤ y}
2. {x = a} if x < 0 then x := −x else x := x ﬁ {x = |a|}3. {y は自然数 ∧ y > 0 ∧ z · xy = a}if odd(y) then z := z · x; y := y − 1 else x := x2 ; y := y/2 ﬁ{y は自然数 ∧ y ≥ 0 ∧ z · xy = a}
ただし，odd(y) は y が奇数であるかどうか判定する述語である．

3.3

BYOB プログラムと帰納的関数

前節の最後の問題で条件文に odd(y) という述語を用いたが，このような述語を用いることは BYOB プログラムの範囲を逸脱しないのだろうか．条件文に用いられるブール式に用いることのできる論理記号は ∧ , ∨ , → , ¬ のみで，odd(y) ≡ (∃x)x<y [y = 2x+1] であるから5 ，このままでは我々の定義した BYOB プログラムには使用できないように思える．しかし，そうではなく実は任意の帰納的関数 f (x1 , · · · , xn ) を用いて代入 y := f (x1 , · · · , xn )を行ったり，任意の帰納的述語 R(x1 , · · · , xn ) を条件文のブール式として使用しても我々の BYOB プログラムの範疇からは逸脱しないことが示される．それは以下の定理によって保証される．
定理 3.7 任意の帰納的関数は BYOB プログラムにより計算できる．

5

従って，odd(y) は原始帰納的述語である．

10

3 複合文，条件文，UNTIL 文の部分正当性

計算機数学講義資料 2016

この定理より f (x1 , · · · , xn ) が帰納的関数のとき{true} P {y = f (x1 , · · · , xn )} を正しくす
る BYOB プログラム P が存在するので，プログラム中で z := f (x1 , · · · , xn ) となっているところを P ; z := y でおきかえると，もともとの BYOB プログラムの文法で書かれたプログラムになる．また，条件文で帰納的述語 R(x1 , · · · , xn ) を用いて， if R then P1 else P2 ﬁと使われている場合は，R(x1 , · · · , xn ) ⇔ f (x1 , · · · , xn ) = 1 となる帰納的関数 f が存在するので，この f を計算する BYOB プログラム P を用いて，（f の値が変数 y に入っているとすると），P ; if y = 1 then P1 else P2 ﬁ とするとやはりこれも，もともとの BYOB
プログラムの文法で書かれたプログラムになる．以上のことから，代入文や条件文，until
文に帰納的な関数や述語を用いてもそれに対応する BYOB プログラムが存在するので，自由に使用してよいということになる．

3.4

until 文の部分正当性

次の表明つきプログラムを考える．

{a = 0 ∧ b = 3} until b = 0 do a := a + 1; b := b − 1 od {a = 3 ∧ b = 0}
a = 0, b = 3 で上の until 文を実行すると，until 文のループが回る間に変数 a, b は

ループ回数
a
b

0 1 2 30 1 2 33 2 1 0となって確かに a = 3, b = 0 で止まるから，上の表明つきプログラムは（完全正当性の意
味でも）正しい．
我々は表明つきプログラムの正しさをその部分プログラムの正しさから導き出そうと考えている．したがって until 文においても，until 文中の do · · · od の間にあるプログラムの正しさから，全体の正しさを導くような規則が欲しい．つまり{A} P {B}{A′ } until α do P od {B ′ }となるような推論規則がほしい．
従って，until 文のループの実行中にループの回る回数に無関係の条件があって，それが常に成り立っている状況が必要である．
このとき，A, B に求められるものは何であろうか．まず until 文で P が実行されるのは
α が偽のときのみであるから，A が成り立つときには α も偽であるような条件でなけれ

11

3 複合文，条件文，UNTIL 文の部分正当性

計算機数学講義資料 2016

ばならない．従って A は ¬α ∧ A0 のような表明でなければならない（あるいは意味がない）．
またループが１回実行されたとき，次にブール式 α の値を評価して偽になったときには，再び P を実行したいのであるから，B から A が導けなければならない．すなわち，少なくとも{¬α ∧ A0 } P {A0 }が正しいことが求められる．
このような A0 はループの実行中に常に成立しているものなので，ループ不変表明と呼ばれる．
それでは上の例でこのような A0 に対応するものは何であろうか．
ループ回数
a
b

0 1 2 30 1 2 33 2 1 0ループの実行中に常に成立している関係を考えると a + b = 3 ∧ 0 ≤ a ≤ 3 ∧ 0 ≤ b ≤ 3
である．a, b は整数であると仮定すると，a + b = 3 ∧ 0 ≤ a ≤ 3 ∧ 0 ≤ b ≤ 3 ⇔ a + b =3 ∧ a ≥ 0 ∧ b ≥ 0 である．このとき，特に a + b = 3 ∧ ∧ b ≥ 0 について考えると{b ̸= 0 ∧ (a + b = 3 ∧ b ≥ 0)} a := a + 1; b := b − 1{a + b = 3 ∧ b ≥ 0}は正しい．従って a + b = 3 ∧ b ≥ 0 はこの until 文のループ不変表明である6 ．それでは，
until 文の推論規則の上式を{¬α ∧ A0 } P {A0 }にしたとき，それからどのような表明つきの until 文が正しいといえるか．until 文を実行する前に A0 が偽の場合は，部分正当性の意味から A0 を事前条件に持つ表明つきプログ
ラムはすべて正しい．A0 が真のとき，もし α の値が真ならば until 文はなにもせずに終了するから，事後条件は事前条件から論理的に導かれるものならばよい．従って A0 が真で，α が偽であるときが問題で，このときは上の式から α の値が偽である限りループが実行され，ループの停止後は α が真になる（このとき A0 は真のままである）．そこで until 文の推論規則として，{¬α ∧ A0 } P {A0 }{A0 } until α do P od {α ∧ A0 }を考えると確かに上式が正しければ，下式も正しくなる．A ≡ a, b ∈ Z ∧ a + b = 3 ∧ b ≥ 0として，
6
a + b = 3 だけでもループ不変表明であるが，後で見るように全体での推論を考えると a + b = 3 ∧ b ≥ 0にする必要がある．

12

3 複合文，条件文，UNTIL 文の部分正当性

計算機数学講義資料 2016

上の例に当てはめると{b ̸= 0 ∧ A} a := a + 1; b := b − 1 {A}{A} until b = 0 do a := a + 1; b := b − 1 od {b = 0 ∧ A}となる．従ってこの推論規則を使って最初の表明つきプログラムの正しさを示すには次のような証明図を作成すればよい．
{}{}(a+1)+(b−1) = 3
a + (b − 1) = 3
a := a + 1
b−1≥0
b−1≥0
{
}
{
}
{
}
a + (b − 1) = 3
a + (b − 1) = 3
b ̸= 0a := a + 1
b := b − 1 {A}
b−1≥0
b−1≥0
A
{b ̸= 0 ∧ A} a := a + 1; b := b − 1 {A}{A} until b = 0 do a := a + 1; b := b − 1 od {b = 0 ∧ A}
{
}
{
}
a=0
a=3
until b = 0 do a := a + 1; b := b − 1 od
b=3
b=0
ここで，最上式の二つの表明つきプログラムはどちらも代入文の公理をみたし，帰結の規則を使用している 2 箇所は適用条件をみたしている．例えば，b ̸= 0 ∧ A → (a + 1) + (b − 1) = 3 ∧ b − 1 ≥ 0 は次のように示される．
b ̸= 0, a + b = 3, b ≥ 0 とする．a + b = (a + 1) + (b − 1) より，(a + 1) + (b − 1) = 3 である．b は整数で，b ̸= 0, b ≥ 0 であるから，b − 1 ≥ 0 である．
問題 3.8

1. 次の表明つき BYOB プログラムは与えられた整数 n と x の積を求めるプログラムである．
{i = 0 ∧ p = 0 ∧ n ≥ 0} until i = n do i := i + 1; p := p + x od {p = n · x}(a) n = 5 の場合に変数 i と p がどのように変化していくか次の変数表に値を書いて正しい答えが得られることを確かめよ．また，p = i · x ∧ i 5 n がループ不変表明になることを確かめよ．
（⊤ は真であることを表す．
）
ループ回数
i
p
p=i·x
i5n

0
0
0
⊤
⊤

1 2 3 4 5(b) この表明付きプログラムの正しさを推論規則を用いて示せ．
（変数が整数値をとることは仮定して良い．
）
13

3 複合文，条件文，UNTIL 文の部分正当性

計算機数学講義資料 2016

2. 次の表明つき BYOB プログラムは与えられた数 a と b に対し，a を b で割ったときの商 [a/b] と余り a mod b を求めるプログラムである．上の問題を参考にして適切なループ不変表明を定め，この表明付きプログラムの正しさを推論規則を用いて示せ．
{a ≥ 0 ∧ b > 0 ∧ q = 0 ∧ r = a}until r < b do q := q + 1; r := r − b od
{q = [a/b] ∧ r = a mod b}3.5

帰結規則の使い方

ここまで複合文，条件文，until 文の推論規則を説明していくつか例をみてきた．その例をみるとわかるが表明つきプログラムが与えられたときそれを部分に分割して推論規則を適用していくステップは帰結の推論規則を除くと唯一に決まっている．すなわち，複合文には複合文の推論規則，条件文には条件文の推論規則そして until 文には until 文の推論規則が適用される．ただし，適用できるといっても until 文の推論規則を適用するためには，事前表明と事後表明の形に制限があるので，一般にはそのままでは適用できない．
また，代入文の公理にも事前表明と事後表明の形に制限がある．それらを調整するために帰結の推論規則が使用される．

3.6

公理と推論規則のまとめ

ここまで考察してきた公理と推論規則をまとめると次のようになる．
代入文の公理{R[x → t]} x := t {R}
帰結の推論規則{A} P {B}{C} P {D}

複合文の推論規則(ただし C → A,B → D がともに真のとき){A} P1 {S1 } {S1 } P2 {S2 } · · · {Sn−1 } Pn {B}{A} P1 ; P2 ; · · · ; Pn {B}

条件文の推論規則{A ∧ α} P1 {B} {A ∧ ¬α} P2 {B}{A} if α then P1 else P2 ﬁ {B}14計算機数学講義資料 2016

until 文の推論規則

3 複合文，条件文，UNTIL 文の部分正当性{¬α ∧ A} P {A}{A} until α do P od {α ∧ A}

15

4 完全正当性

計算機数学講義資料 2016

4

完全正当性

前章において部分正当性の意味で正しい表明つきプログラム導くための公理と推論規則について考察した．ここでは完全正当性について考えてみよう．部分正当性と完全正当性に違いはプログラムの停止性の保証があるかどうかである．部分正当性では停止性を保証する必要がなかったが，完全正当性ではプログラムの正しさばかりでなく停止性についても考慮しないといけない．代入文は必ず停止する．また前章で考察した部分正当性に関する推論規則のなかで until 文の推論規則を除くと，推論規則の上式が停止するプログラム
ならば下式は必ず停止することがわかる．一方 until 文の推論規則では，上式が停止する
プログラムであっても下式が停止するとは限らない．例えば部分正当性の until 文に関する推論規則をそのまま適用して次のような完全正当性に関する推論を考えてみよう．

〈1 = 1 ∧ x > a〉 x := x + 1 〈x > a〉〈x > a〉 until 1 ̸= 1 do x := x + 1 od 〈1 = 1 ∧ x > a〉
明らかに上式は停止するが，下式は停止しない．
従って、部分正当性に関する until 文の推論規則を完全正当性に移し替えた〈¬α ∧ A〉 P 〈A〉〈A〉 until α do P od 〈α ∧ A〉
は上式の条件だけでは下式の停止性を保証できないため誤った推論であることになる．それではこの下式が（完全正当性の意味で）正しい表明つきプログラムであるためには上式の表明がどのような条件をみたしていればよいであろうか．ここで以前にとりあげた例をもう一度みてみよう．

{b ̸= 0 ∧ A} begin a := a + 1; b := b − 1 end {A}{A} until b = 0 do a := a + 1; b := b − 1 od {b = 0 ∧ A}
この例では下式は b の値がどんな値であっても停止することがわかる．それは until 文のdo 以下を実行するごとに b の値が 1 減るためにループを b 回くり返すと b の値が 0 になる
ことがわかるからである．ここでは b がカウンターの役目をしていてループが回るごとにb の値がへり、やがて b の値が 0 になった時点で実行が終了するのである．
従って、一般の場合にもこの b に相当するカウンターがあってループが回るたびに減少してやがて 0 になるそのようなものがとれれば、停止性を示すことができる．そこで整数を値にもつ式 T で次の性質をみたすものを考える．

1. T はループの繰り返しで減少する．すなわち、〈¬α ∧ A ∧ v = T 〉 P 〈A ∧ T < v〉 が正しい．
2. ループの繰り返しの間は T の値は正である．すなわち、¬α ∧ A → T > 0 である．
16

4 完全正当性

計算機数学講義資料 2016

もし、与えられた表明付きの until 文に対してこのような T を見つけることができれば、その until 文の停止性を示すことができる．このような式 T を上界関数7 とよぶ．そこで次のような推論規則を考える．

〈¬α ∧ A ∧ v = T 〉 P 〈A ∧ T < v〉 （ただし、T は整数を値にもつ式で〈A〉 until α do P od 〈α ∧ A〉
¬α ∧ A → T > 0 をみたす）
この推論規則では、確かに上式が正しい表明つきプログラムならば下式も正しい表明つきプログラムである．これを用いることで多くの表明つきプログラムの正当性を示すことができる．例えば問題 3.8 において次の表明つきプログラムの正しさを証明したが、これの完全正当性版を考えてみよう．

{i = 0 ∧ p = 0 ∧ n ≥ 0} until i = n do i := i + 1; p := p + x od {p = n · x}
T := n − i とおくと、この T が上界関数であることをわかるので、上記の推論規則より完全正当性の意味でも正しいことがわかる．
問題 4.1〈i < n ∧ p = i · x ∧ v = n − i〉 i := i + 1; p := p + x 〈i 5 n ∧ p = i · x ∧ n − i < v〉
が正しいことを示せ．
完全正当性に関する公理と推論規則をまとめると次のようになる．
完全正当性に関する公理と推論規則
代入文の公理〈R[t/x]〉 x := t 〈R〉帰結の推論規則

複合文の推論規則

条件文の推論規則

7〈A〉 P 〈B〉〈C〉 P 〈D〉(ただし C → A,B → D がともに真のとき)〈A〉 P1 〈S1 〉 〈S1 〉 P2 〈S2 〉 · · · 〈Sn−1 〉 Pn 〈B〉〈A〉 P1 ; P2 ; · · · ; Pn 〈B〉〈A ∧ α〉 P1 〈B〉 〈A ∧ ¬α〉 P2 〈B〉〈A〉 if α then P1 else P2 ﬁ 〈B〉

上界関数を用いたが，一般の場合には整礎集合上の順序を用いる必要がある．

17

4 完全正当性

計算機数学講義資料 2016

until 文の推論規則〈¬α ∧ A ∧ v = T 〉 P 〈A ∧ T < v〉 （ただし、T は整数を値にもつ式で〈A〉 until α do P od 〈α ∧ A〉
¬α ∧ A → T > 0 をみたす）

参考文献[1] プログラム検証論

林晋著

共立出版

[2] コンピュータサイエンス入門 論理とプログラム意味論
田辺誠・中島玲二・長谷川真人著

岩波書店[3] プログラム仕様記述論 荒木啓二郎・張漢明著 オーム社

平成 25 年 3 月 28 日作成
平成 25 年 4 月 19 日修正
平成 25 年 9 月 4 日修正
平成 26 年 7 月 30 日修正
平成 27 年 9 月 18 日修正
平成 28 年 6 月 22 日修正18