program_verification

B4 ゼミ
4章 Program Verification
上田研究室 M1
飛田伸一
2005/07/04
導入
• 何故コードの仕様記述と検証をすべきか
• ソフトウェア検証の枠組み
–
–
–
–
2005/7/4
コアプログラミング言語
Hoare triples
部分正当性と完全正当性
プログラム変数と論理変数
2
この発表での表記法
• は|=と書く
• は<=と書く
• は>=と書く
• φRはφRと書く
• ( )は(| |)と書く
2005/7/4
3
無限状態空間ならどうするか
• 3章の方法は、制御が主な問題となるが複雑な
データが無いような通信プロセスの検証システム
に適している。そしてこのシステムは有限状態で
ある
• ここでデータ型に整数型、リスト、ツリーの変数を
認めると無限状態空間の機械の領域にいること
になる
こういうときはどうするか？
2005/7/4
4
この章で出てくるメソッド(1)
• 証明ベース(Proof-based):
– モデル検査としてするように、余すところなくシステムが入る事が出来る
毎状態検査しない。プログラム変数は無限に沢山の相互関係のある値
を持つ事が出来るのでこれは不可能である
– その代わりとして、証明計算を用いて、システムはプロパティを満たすと
いう証明を組み立てる
• 半自動(Semi-automatic):
– 多くのプログラムがその仕様記述を満たすということを証明する事を含
む段階(step)は機械的である。いくつか知性を含むstepがあり、それはコ
ンピュータによってアルゴリズム的に実行されることができない
• プロパティ指向(Property-oriented):
– 振る舞いの完全な仕様(記述)よりもむしろプログラムのプロパティを検
証する。
2005/7/4
5
この章で出てくるメソッド(2)
• アプリケーション領域(Applicaton domain):
– アプリケーションの領域は逐次変換的プログラム(sequential
transformational programs)
– 逐次とは、プログラムは単一プロセッサではしると仮定し、そして
並列問題なしであるという事を意味する
– 変換的とは、プログラムは入力をとり、計算の後出力とともに終
了するという事を要求することを意味する
• Pre/Post-development:
– この章の技法は同一であると証明できる仕事を実行するプログ
ラムの小断片のためにコーディング過程の間使われるべきであ
る。機能的バグを避けるために開発過程の間使われるべきであ
る
2005/7/4
6
4.1 何故コードの仕様記述と検証をすべきか
検証の議論は次のものを含んでいる
• Documentation
– プログラムの仕様記述はそのdocumentationにおいて重要な構
成要素であり、プログラムのdocumentingの過程は重要な問題を
起こしたり解決したりするかもしれない。適当な論理の式で書か
れた形式的仕様記述の論理構造は一般にその実装を書こうとし
ようとする時に方針の手引きとして役に立つ
• Time-to-market
– テストフェーズの間に大きなシステムをデバッグする事はコストが
大きく、時間の浪費であり、局所「修正」はしばしば他のフェーズ
における新たなバグをもたらす
2005/7/4
7
何故コードの仕様記述と検証をすべきか
• Refactoring
– はっきりした仕様記述があれば、仕様記述と検証をされたソフト
ウェアは当然再利用するのが容易
• Certification audits
– 安全性が重大なコンピュータシステム(原子力発電所の冷却シス
テムの制御や近代的な航空機のコクピットのような)はソフトウェ
アが出来る限り精密そして几帳面に仕様記述及び検証されてい
る事を要求する。商業的に重大(commercially critical)なものも同
様である。
– すなわち適切な使用で正しく実行されるという保証でがついてい
るべきである。プログラムが仕様記述を満たすという証明はこの
保証のようなものである
2005/7/4
8
Costとbenefit
• 検証技術が進歩するのでコストは減ってきている
• ソフトウェアの複雑性と社会がそれに頼る範囲が増加し
ているのでその利益はより重要になっている
2005/7/4
9
4.2 ソフトウェア検証の枠組み
•
ソフトウェアを作るための枠組み
1. アプリケーション領域の為の要求の非形式的記述R
を記号論理の等価の式φRに変換する
2. 会社から与えられた、もしくは個々の顧客から望ま
れたプログラミング環境でφRを実現する事を意図し
たプログラムPを書く
3. プログラムPは式φRを満たすということを証明する
2005/7/4
10
RとφR
• 非形式の領域と形式的仕様記述の間の「いったりきたり」
は必要
– 非形式的要求Rは形式的記述φRと等価であるかどうかを検証す
る事は不可能だから
• Rの適した形式化φRを見つける過程は最大級の注意を
要求する
– もしそうでなければ、φRはRで記述されたものと異なった振る舞
いを仕様記述するということがいつも可能である
– さらに悪い事に、要求Rはしばしば矛盾する
2005/7/4
11
4.2.1 コアプログラミング言語
• ここで勉強するプログラミング言語は命令型言語の典型
的なコア言語である。
• その言語を構成するもの
–
–
–
–
整数値変数とboolean値変数への代入
if文
while文
直列結合(sequential compositions)
• オブジェクト、プロシージャー、スレッド、再帰的データ構
造を持っていないが、CやJavaのような大きな言語によっ
て計算出来ることは、この言語によっても計算出来る
2005/7/4
12
Integer expressions
E ::= n | x | (-E) | (E+E) | (E-E) | (E*E)
(4.1)
nは{...,-2,-1,0,1,2,...}の数字、xは変数
• 束縛順序
– (単項)- > (乗算)* > (加算)+ , (減算)-
• 整数式の例
5, x,
2005/7/4
4+(x-3), x+(x*(y-(5+z)))
13
Boolean expressions
B ::= true | false | (!B) | (B&B) | (B||B) | (E<E) (4.2)
• !は否定、&はboolean式の論理積、||はboolean式
の論理和である。
• 束縛順序
– ! > & > ||
• 注意
– 等価性検査E1 == E2 は!(E1 < E2) & !(E2 < E1)に
よって表現してよい
– !(E1 == E2)を(E1 != E2)と書いてよい
2005/7/4
14
Commands
C ::= x=E | C;C | if B {C} else {C} | while B {C} (4.3)
• 大括弧{と}は、if文やwhile文の中のコードのブロックの
範囲をを示す。また、ブロックが単一文から成るならば省
略する事が出来る
2005/7/4
15
プログラミング構成の直感的意味(1)
1.
2.
単一命令 x = Eは一般に代入文である。現在のストア
の状態で整数式Eを評価する。そして現在ストアされて
いるxの値をその評価の結果で上書きする
複合命令 C1;C2はC1とC2の直列結合である。現在の
ストアの状態でC1を実行することによって始まる。もし
その実行が終われば、その時C1の実行の結果のスト
レージの状態でC2を実行する。もしC1の実行が終わら
なければ、C1;C2の実行も終わらない。直列結合は制
御構造の例である
2005/7/4
16
プログラミング構成の直感的意味(2)
3.
4.
if B { C1 } else { C2 }は最初に、現在のストアの状態でboolean式
Bを評価する。もし、結果がtrueだったらC1が実行さる。もし、Bが
falseであればC2が実行される。if B { C1 } else { C2 }は制御構造
である
while B { C }は繰り返し実行されるような文を書くことを可能にす
る。While B { C }は制御構造である。その意味は
1. boolean式Bは現在のストアの状態で評価される。
2. もしBがfalseなら、そのcommandは終わる。
3. さもなければ、Cは実行される。もしその実行が終わるなら、最
新版のストアの状態は値が変わっているかも知れないのでB
を再評価しステップ(1)を再び始める。
2005/7/4
17
例 4.2 階乗関数 -Fac1自然数nの階乗 n!は帰納的に定義される。
def
0! = 1
def
(n+1)! = (n+1)・n!
次のプログラムFac1はxの階乗を計算し、
yにその結果をストアすることを意図したものである。
y = 1;
z = 0;
while(z != x){
z = z + 1;
y = y * z;
}
2005/7/4
18
4.2.2 Hoare triples
• (4.3)によって生成されたプログラムの断片は機械の「状
態」で実行し始める。
• 我々のプログラミング言語はプロシージャや局所変数を
持っていないので、機械の「状態」は単にプログラムで使
われている全ての変数の値のベクトルのように表現する
ことが出来る
そのようなプログラムのための要求の形式的仕様
記述φRに対して、どのような構文を使うべきか？
2005/7/4
19
triplesが必要な理由(出力)
• プログラムの出力に興味があるのだから、プログラムが
実行した後の状態の変数について、等価性=や不等号<
のような演算子を使って問い合わせ出来るようにするべ
き
2005/7/4
20
triplesが必要な理由(入力)
• 例えば、非形式的要求Rが「平方しても入力xより小さくなるような数y
を計算しろ」なら、適切な仕様記述はy・y<xであるかもしれない
– 入力xが-4であるなら？
• 非形式的要求Rを訂正して、要求は「もし入力xが正の数であるなら、
平方したものがxより小さい数を計算しろ」となる
プログラム実行後での状態についてだけでなく、プログラム実行前の状
態についても考える必要がある
triplesを使って仕様記述する
2005/7/4
21
Hoare triples
(|φ|) P (|ψ|)
(4.5)
φ:事前条件
ψ:事後条件
P:プログラム
「もしプログラムPがφを満たす状態で実行されるな
らば、その時Pの実行の結果生じる状態はψを満
たすだろう」ということを意味する
2005/7/4
22
例
平方してもxより小さいという数を計算するプログラムPの仕様記述
(|x>0|)P(|y・y<x|)
(4.6)
• これはもしPをx>0のような状態で実行するなら、その結果生じる状態
はy・y<xのようなものであるだろうことを意味する。
• xの正の値でない時についての要求は無いので、プログラマーはそ
の場合に何をするかは自由である。
• x<=0の場合にゴミを生み出すプログラムでも、x>0の間は正しく動け
ば仕様記述を満たすといえる
2005/7/4
23
定義 4.3
1.
2.
3.
4.
5.
コンピュータ科学者のC.A.R. Hoareにちなんで仕様記述(|φ|) P
(|ψ|)はHoare tripleと呼ばれている
(4.5)で、式φはPの事前条件(precondition)、ψは事後条件
(postcondition)と呼ばれる
ストアやコアプログラムの状態は個々の変数xに整数l(x)を代入す
る関数lである
関数記号-(単項),+,-,*,(二項)と二項述語記号<と=を用いた述語論
理の式φに対して、もし、128ページからM |=l φが成り立つならば、
その場合に限って、状態lがφを満たす若しくは、lがφ状態( l |= φで
書かれる)である。そしてそこで、lは参照表としてみなされ、モデル
Mは集合Aとして全ての整数を持ち、標準の方法で関数と述語記
号を解釈する。
(4.5)のHoare triplesについて、φとψの中の作用素(quantifier)はプ
ログラムPの中で出現しない変数だけに束縛することを要求する
2005/7/4
24
例 4.4
状態lに対して、l(x)=-2,l(y)=5,l(z)=-1である
•
•
•
l |= ￢(x + y < z)は成り立つ。
–
x+yは-2+5=3と評価されて、zはl(z)=-1と評価され、3は-1より小
さくない
l |= y - x * z < zは成り立たない
–
左辺の式は5と評価されて-(-2)・(-1)=3それは全然l(z)=-1より
小さくない
l |= ∀u(y<u→y*z<u*z)は成り立たない
–
uが7である時、l |= y<uは成り立つ。しかしl |= y*z < u * zは成
り立たない。
2005/7/4
25
事前条件が必要ないとき
• どんな状態であってもプログラムを実行し、その結果の
状態がψを満たすべきであるとしたい時は、事前条件にT
をセットすればよい。Tは恒真のことである。
2005/7/4
26
Hoare triplesは仕様記述
• 仕様記述(|x>0|)P(|y・y<x|) を満たすプログラムPは唯一でない
例
y = 0;
while (y * y < x) {
y = y + 1;
}
y = y - 1;
前のプログラムとは異なっているが、両方とも仕様記述を満たしている。
• xが22の時
– 最初に出てきた方はy=0
– 2番目に出てきた方は、y=4
2005/7/4
27
4.2.3 部分正当性と完全正当性
• (|φ|) P (|ψ|)が成り立つ時の説明はどちらかとい
えば形式的ではなかった
• 特に、もしPが終わらなければ、どう結論を出す
べきかという事は言わなかった
• 実際には、この状態を扱う2つの方法がある
– 部分正当性はプログラムが終わる事を要求しない
– 完全正当性では、我々はプログラムの終了を強いる
2005/7/4
28
定義 4.5(部分正当性)
• もし、φを満たす全ての状態に対して、Pが実際に
終わるとき、Pの実行の結果から生じた状態が事
後条件ψを満たすなら、(|φ|) P (|ψ|)は部分正当性
のもとで満たされるという
• この場合、関係 |=par (|φ|) P (|ψ|)が成り立つ
• |=parを部分正当性充足関係と呼ぶ
2005/7/4
29
部分正当性
while true {x = 0;}
上のプログラムは無限にループし、決して終わらない
しかし、全ての仕様記述を満たす
何故なら、部分正当性はもしプログラムが終わるのなら、
何が起こるべきかということだけを問題とするから
2005/7/4
30
定義 4.6(完全正当性)
• もし、事前条件φを満たしPが実行される全ての
状態に対して、Pが停止する事が保証され、結果
状態が事後条件ψを満たすなら、(|φ|) P (|ψ|)は完
全正当性のもとで満たされるという
• この場合、関係 |=tot (|φ|) P (|ψ|)が成り立つ
• |=totを完全正当性充足関係と呼ぶ
2005/7/4
31
完全正当性
while true {x = 0;}
上のプログラムは全ての入力で永久にループするので
完全正当性で全ての仕様記述を満たさない
完全正当性の証明 = 部分正当性の証明 + 停止性の証明
2005/7/4
32
例 4.7.1 後継関数 -Succa = x + 1;
if (a - 1 == 0) {
y = 1;
} else {
y = a;
}
上のプログラムSuccは部分正当性と完全正当性の下で仕様記述
(|T|) Succ (|y=(x+1)|)を満たす。
このコードは最適ではないということに注意する
つまり、プログラムが最適で無かったとしても、証明規則はプログラム
の振る舞いを証明出来ることが必要である
2005/7/4
33
例4.7.2 階乗関数 -Fac1- (1)
y = 1;
z = 0;
while(z != x){
z = z + 1;
y = y * z;
}
上のプログラムFac1はxが非負数のときにだけ終わる
2005/7/4
34
例4.7.2 階乗関数 -Fac1- (2)
• |=tot (|x >= 0|) Fac1 (|y=x!|)が成り立つということを証明
できるべきである。
• |=tot (|x >= 0|) Fac1 (|y=x!|)は、x>=0という条件でFac1を
実行するとy=x!という結果を伴い終わるということを式で
しめしたものである
• Fac1はxが負数なら終わらないので|=tot (|T|)Fac1(|y=x!|)
が成り立つということを証明できるべきでない
• 部分正当性については、|=par (|x>=0|)Fac1(|y=x!|)と
|=par(|T|)Fac1(|y=x!|)の両方の文が証明可能であるべき
である。
2005/7/4
35
定義 4.8
1. もし、(|φ|)P(|ψ|)の部分正当性が、部分正当性
計算(partial-correctness calculus)で証明するこ
とが出来るなら、シーケント ├par (|φ|)P(|ψ|)は
妥当である
2. 同様に、完全正当性計算で証明することが出
来るなら、シーケント ├tot (|φ|)P(|ψ|)は妥当であ
る
※部分正当性計算、完全正当性計算は後に示さ
れる
2005/7/4
36
正当性
• もしPが部分正当なら、|=par (|φ|)P(|ψ|)が成り立
つ。
• 一方├par (|φ|)P(|ψ|)の妥当性は、計算によってP
が部分正当であるという事を証明出来るというこ
とを意味する。
• つまり、|=par (|φ|)P(|ψ|)は実際に正当だという事
を意味し、├par (|φ|)P(|ψ|)は我々の計算により
証明できる正当だということを意味する。
2005/7/4
37
健全性と完全性(1)
• もし、証明出来るものの全てがtrueであるなら、計算は健
全であるといえる。つまり、もしfalseであるものを証明する
ことが不可能なら、計算は健全であるといえる
• もしtrueである全てのものを証明することが可能であるな
ら、計算は完全であるという
2005/7/4
38
健全性と完全性(2)
• 健全性
– もし、全てのφ,ψ,Pに対して、├par(|φ|)P(|ψ|)が妥当である時はい
つでも|=par (|φ|)P(|ψ|)が成り立つならば├parは健全である
– もし、全てのφ,ψ,Pに対して、├tot (|φ|)P(|ψ|)が妥当である時はい
つでも|=tot (|φ|)P(|ψ|)が成り立つならば├totは健全である
• 完全性
– もし、全てのφ,ψ,Pに対して、|=par (|φ|)P(|ψ|)が成り立つ時はいつ
でも├par (|φ|)P(|ψ|)が妥当であるならば├parは完全である
– もし、全てのφ,ψ,Pに対して、|=tot (|φ|)P(|ψ|)が成り立つ時はいつ
でも├tot (|φ|)P(|ψ|)が妥当であるならば├totは完全である
2005/7/4
39
健全性と完全性(3)
• 一般に個々の証明規則の健全性は他のものと独立に証
明されることが出来るので比較的に示すのが簡単である
• 一方で、完全性はお互い重なり合って働いている証明規
則の全体の集合によるので、完全性を示すのが難しい
• この性質は、これから勉強するプログラム論理(program
logic)についても成り立つ
2005/7/4
40
4.2.4 プログラム変数と論理変数
• 検証するプログラム中でこれまでに見た変数は
プログラム変数と呼ばれる。
• プログラム変数は仕様記述の事前条件と事後条
件にも現れてよい
• 仕様記述の式を立てるために、プログラム内に
現れない変数を使うことが必要なことがある
2005/7/4
41
例 4.9.1 階乗関数 -Fac2- (1)
y = 1;
while (x != 0) {
y = y * x;
x = x - 1;
}
もし上プログラムが終了するなら、xは0になりそしてyはxの初期値の階乗となる
よって(|x>=0|) Fac2 (|y = x!|)と書くのは良い考えではない
xがプログラムによって変更されるというのに対処するため、xの初期値を覚えて
おく方法が必要
2005/7/4
42
例 4.9.1 階乗関数 -Fac2- (2)
• 論理変数
検証されるコードには現れないが、事前条件と事後条件
を構成する論理式の中にだけ現れる変数を論理変数という
仕様記述 (|x=x0∧x>=0|) Fac2 (|y = x0!|)でx0は論理変数であり、
事前条件で全称化されるものとして読む
この仕様記述は
「全ての整数x0に対して、もしxがx0と等しく、x>=0であり、プログラムを
実行してそれが停止するなら、結果状態はyがx0!と等しいということを
満たす」と読む
2005/7/4
43
例 4.9.2 Sum関数 -Sumz = 0;
while (x > 0) {
z = z + x;
x = x - 1;
}
このプログラムはxまで整数を合計し、zにその結果をストアする
故に、(|x=3|) Sum (|z=6|)、(|x=8|) Sum (|z=36 |)となる
41ページの定理1.31から、全てのx>=0に対して1+2+…+x=x(x+1)/2
という事は分かっている
つまり仕様記述は(|x=x0∧x>=0|) Sum (|z=x0(x0+1)/2|)と書ける
2005/7/4
44
定義 4.10 論理変数
• (|φ|) P (|ψ|)に対して、その論理変数の集合
はφかψの中で自由である変数であり、Pの
中では出現しない
2005/7/4
45
END
2005/7/4
46
保留
• 現在、多くの会社は新たなハードウェア、ネットワーク環境、それに
加えて変わり続ける要求に適応しなければならない適切な
documentationなしで大昔のコードの遺産と戦っている。
• 多くの場合、コードの確かな一部をまだ覚えているかもしれない最初
のプログラマーは移籍したり死んでしまったりしている。
• ソフトウェアシステムは今やしばしば人間よりも長い平均余命を持っ
ている。
• そしてそれは耐久力、透過性とportable designそして実装過程を必要
とする。
• 2000年問題がちょうどその例にあたるようなものである。
• ソフトウェア検証はこれのうちいくつかを供給する。
2005/7/4
47
保留
• 顧客は普通、プログラムが正確にすべき事のかなり曖昧な考えを
持っている。
• 従って、アプリケーション領域にとっての要求の明確で統一性のある
記述Rは
• 成功したプログラミングですでに厳しいstepである。
• このphaseは理想的に、お互いに取った、机の周りやテレビ会議での
顧客とプロジェクトマネージャーによって
• 引き受けられる。(?)
• ソフトウェア開発の枠組みの次のphaseはプログラムPを作ることを含
む。
• そしてその後、最後の仕事はPはφRを満たすということを検証する事
である。
2005/7/4
48
• ここで再び、我々の枠組みは実際問題として続ける事を単純化しす
保留
• (この時)我々の課題(議題)、はプログラムPは(4.5)の事前条件φと事
後条件ψによって与えられた仕様記述を満たすこと我々に証明させ
る証明の表記法を開発することである。
• ((そのような証明は)証明したい式の構造を調べることによって成し
遂げられるところの)命題論理や述語論理のための証明計算を発展
させたことを思い出せ。
• 例えば、implication(含意) φ→ψを証明するために、φを仮定しそして
ψをどうにかして示さなければならない
• その証明はimplies-introductionの証明規則で終わりにすることがで
きる。
• 我々がまさに開発しようとしているその証明計算は似ている行に続く。
2005/7/4
49
保留
• それらは我々が前に勉強した論理と異なる。
• それらは2つの異なった種類のもの(論理式φ,ψ v.s. コードPの断片)
から出来ているtriplesを証明するので、
• 我々の証明計算は適切にそれらのそれぞれに取り組まなければな
らない。
• それにもかかわらす、我々は(構成の)証明戦略(方法)を保つ。
• 今やPの構造の中でなくて。(?)
• これは大きなプロジェクトの検証で重要な利点であることに注意する。
• そこ(大きなプロジェクト)ではコードは多数のモジュールから出来て
いる。
• such that含まれる部分の正当性は含まれるほかの部分の正当性に
よるだろう。(?)
• それ故、あなたのコードはあなたのプロジェクトの他のメンバーがま
さにコードしたサブルーチンを呼ぶかもしれない。
2005/7/4
50
• しかし、あなたはすでにサブルーチンがそれら独自の仕様記述を満

Download Report