逐次プログラムの正当性(2) 帰納的アサーション法(フロイド法) 表現系工学特論 逐次プログラムの正当性(2) 帰納的アサーション法(フロイド法)
1.正当性アサーション(復習) precondition loop invariant potential function post condition
2.正当性の証明(復習) 部分正当性 もし実行が停止すれば,その時点で事後条件が成り立つ. 停止性 必ず実行が停止する. 部分正当性 もし実行が停止すれば,その時点で事後条件が成り立つ. 停止性 必ず実行が停止する. partial correctness termination
3.帰納的アサーション法(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
3.帰納的アサーション法(Floyd法)による部分正当性の証明 プログラムのループの少なくとも1カ所に 必ずアサーションを書く. (2) アサーション を書いた位置 からアサーション に到達するすべての経路ごとに 次のことを証明する. ■位置 が真のとき, に到達した時点で は真である で その経路に沿ってプログラムを実行して 位置 ただし,経路の途中で他のアサーションが書かれた位置を 通過しないものについてのみでよい. 経路がループのとき,i = j でもよい.
■例題 挿入ソート
挿入ソート(Java版) //loop invariant: A[0]..A[i-1] are sorted; // 1≦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; // 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; }
経路ごとの証明(1/7) #1 #2 (0)→(1) (1)→(4) (1)→(2) (2)→(3) #1 (2)→(3) #2 (3)→(1) (2)→(2) #1 #2
経路ごとの証明(2/7):(0)→(1) ,(1)→(4) (0)→(1): I = 1より自明. (1)→(4): I = nより自明.
経路ごとの証明(3/7):(1)→(2) 2 3 5 4 6 7 8 9 J sorted W I I ≠ n W = A[I] J = I - 1
経路ごとの証明(4/7):(2)→#1→ (3)の証明 sorted J = -1 J I 1 2 3 5 6 7 8 9 1 < A[0] = W
経路ごとの証明(5/7):(2)→#2→ (3)の証明 sorted J ≧ 0 J I #2 2 3 4 5 6 7 8 9 ≦ 4 < A[J] ≦ W A[J+1] = W
経路ごとの証明(6/7):(3)→(1)の証明 2 3 4 6 7 8 9 5 sorted I sorted 2 3 4 6 7 8 9
演習問題 経路ごとの証明(7/7): (2)→(2)の証明 演習問題 経路ごとの証明(7/7): (2)→(2)の証明 2 3 5 4 6 7 8 9 J sorted < I J ≧ 0 > W < A[J] sorted 2 3 6 7 8 9 J 5 4 < I A[J+1] = A[J]