知能ソフトウェア特論(第Ⅰ部)講義メモ
プログラムの正当性(1)
正当性証明の基本原理
1.アサーションとポテンシャル関数
■アサーション:流れ図の特定の位置(辺)でプログラム変数間に成り立つ関係式.特に
つぎの3つの種類は重要である.
 事前条件(precondition):受け入れ可能な入力についての記述
 事後条件(postcondition):正しい出力が満たすべき条件の記述
 ループ不変条件(loop invariant):ループの出入口で常に成り立つ条件式
■ポテンシャル関数(potential function):流れ図の特定の位置(辺)で定義される,プログ
ラム変数を用いた関数.その値(ポテンシャル)は常に非負であり,かつ,制御がこ
こを通過する毎にその値が必ず1以上減少する.
2.プログラムの正当性の定義
事前条件を満たす任意の入力に対して,つぎの2つの性質を証明する.
性
質
部分正当性
内
容
もし実行が停止すれば,その時点で事後条件が成り立つ
(計算結果がもし得られれば,それは正しい)
停止性
必ず実行が停止する
(必ず計算結果が得られる)
3.部分正当性の証明方法
 ループ不変条件がその位置で常に真であることを数学的帰納法で証明する.
 基礎ケース : はじめてその位置に実行が到達したときに真であること.
 帰納ステップ: いまその位置で真で,かつループの継続条件が真であるならば,
再度その位置に実行が到達したときにも真であること.
 ループ不変条件が真でかつループの終了条件が真ならば,事後条件が成り立つこと.
4.停止性の証明方法
ループの入り口で定義されたポテンシャル関数についてつぎの事項を証明する.
 関数値(ポテンシャル)が常に非負であること(ループ不変条件)
 その位置に実行が到達するたびに関数値(ポテンシャル)が1以上減少していること.
■例題 自然数 m と n の積 P を加算のみで求めるプログラム
START
1
m0
事前条件
I 0
P 0

P  In, I  m
ループ不変条件
2
ポテンシャル関数
5
I m
事後条件
P  mn
T
3
F
f (I , P)  m  I
END
P Pn
I  I 1
4
mとnの積P
演習問題 1
つぎの流れ図は,入力として自然数 a, b (a  0, b  0) が与えられたとき, a  b の商 Q と余り
R を加算と減算のみで求めるプログラムである.その正当性を証明せよ.
START
1
a  0, b  1
Q0
Ra
 a  bQ  R, 0  R

 f (Q, R)  R
2
Rb
T
5
a  bQ  R, 0  R  b
F
3
Q  Q 1
R  R b
4
a÷b の商Qと余りR
END
ダウンロード

プログラム理論特論講義メモ