逐次プログラムの正当性（２） 帰納的アサーション法（フロイド法）

Presentation on theme: "逐次プログラムの正当性（２） 帰納的アサーション法（フロイド法）"— Presentation transcript:

1 逐次プログラムの正当性（２） 帰納的アサーション法（フロイド法）
表現系工学特論 逐次プログラムの正当性（２） 帰納的アサーション法（フロイド法）

2 １．正当性アサーション（復習） precondition loop invariant potential function
post condition

3 ２．正当性の証明（復習） 部分正当性 もし実行が停止すれば，その時点で事後条件が成り立つ． 停止性 必ず実行が停止する．
部分正当性　 　　　　もし実行が停止すれば，その時点で事後条件が成り立つ． 停止性　 　　　　必ず実行が停止する． partial correctness termination

4 ３．帰納的アサーション法（Floyd法）による部分正当性の証明
Put at least one assertions in each loop. (2) For each path starting from and ending at prove the following statement: ■ is true at if when the control has reached then

5 ３．帰納的アサーション法（Floyd法）による部分正当性の証明
プログラムのループの少なくとも1カ所に 　　必ずアサーションを書く． (2) アサーション を書いた位置 からアサーション に到達するすべての経路ごとに 次のことを証明する． ■位置 が真のとき， に到達した時点で は真である で その経路に沿ってプログラムを実行して 位置 　ただし，経路の途中で他のアサーションが書かれた位置を 通過しないものについてのみでよい． 　経路がループのとき，i = j でもよい．

6 ■例題　挿入ソート

7

8 挿入ソート（Java版） //loop invariant: A[0]..A[i-1] are sorted; // ≦i≦n for(i=1; i!=n; i++) { w=A[i]; 　 //insert w into (or append w to) A[0]..A[i-1] // to make A[0]..A[i] sorted. //loop invariant: A[0]..A[j],A[j+2]..A[i] are sorted; // (try to place w at A[j+1]) // w＜A[j+2] if j<i-1; // ≦i≦n-1; -1≦j≦i-1 for(j=i-1; j>=0 && w<A[j]; j--) { A[j+1]=A[j]; } A[j+1]=w; }

9 経路ごとの証明(1/7) #1 #2 (0)→(1) (1)→(4) (1)→(2) (2)→(3) #1 (2)→(3) #2
(3)→(1) (2)→(2) #1 #2

10 経路ごとの証明(2/7)：(0)→(1) ，(1)→(4)
(0)→(1)： I = 1より自明． (1)→(4)： I = nより自明．

11 経路ごとの証明(3/7)：(1)→(2) 2 3 5 4 6 7 8 9 J sorted W Ｉ I ≠ n W = A[I]
J = I - 1

12 経路ごとの証明(4/7)：(2)→#1→ (3)の証明
sorted J = -1 J Ｉ 1 2 3 5 6 7 8 9 1 ＜ A[0] = W

13 経路ごとの証明(5/7)：(2)→#2→ (3)の証明
sorted J ≧ 0 J Ｉ #2 2 3 4 5 6 7 8 9 ≦ 4 ＜ A[J] ≦ W A[J+1] = W

14 経路ごとの証明(6/7)：(3)→(1)の証明 2 3 4 6 7 8 9 5 sorted Ｉ sorted 2 3 4 6 7 8 9

15 演習問題 経路ごとの証明(7/7)： (2)→(2)の証明
演習問題　経路ごとの証明(7/7)： (2)→(2)の証明 2 3 5 4 6 7 8 9 J sorted ＜ Ｉ J ≧ 0 ＞ W < A[J] sorted 2 3 6 7 8 9 J 5 4 ＜ Ｉ A[J+1] = A[J]