Krakatoa and Jessieを用いた、Javaプログラムの正当性＆安全性証明(アルゴリズムもあるよ！)
概要
Javaプログラムに専用の記法で満たすべき条件を形式的に記述し、それをCoqの問題に変換して手動で証明する。
この記事はCompetitive Programming Advent Calendar 2011
用意するもの
- Why 2.30 および Why3 0.71 (両方必要)
- Why 2.30に同梱されているKrakatoa and Jessieを用いる。
- Coq
- 上記ソフトウェアが動作するOS (ここではUbuntu 11.10)
流れ
Javaプログラムを書く
作業用ディレクトリを作り、Max.javaを以下のようにする。
public class Max {
/*@ ensures \result == 0;
@ */
public static int max(int a, int b) {
return 0;
}
}
Krakatoaを起動
$ krakatoa Max.java
すると、krakatoaがMax.javaを処理し、Why3 IDEが立ち上がる。
ここで、リストの「WP Jessie-program」を選択し、左側のツールボックスにある「Alto-Ergo 0.93」を押すと
簡単な命題だったため、自動定理証明プログラムであるAlto-Ergoが全部証明してくれた。
少し難しい証明にする
Max.javaを書き換えて
public class Max {
/*@ ensures (\result == a || \result == b) &&
@ (\result >= a && \result >= b);
@*/
public static int max(int a, int b) {
return a>b ? a : b;
}
}
として、Krakatoaを再起動すると
一番上がobsoleteになっている。
この程度の命題ならAlt-Ergoでも証明できてしまうが、今度はCoqで証明してみよう。
まず、Alt-Ergoの証明が邪魔なので、「normal postcondition」内の「Alt-Ergo 0.93」を選び、「Remove」で削除する。
次に、リストの「normal postcondition」を選択し、「Coq 8.3pl2」を押すと
そこで、この(?)マークがついている行を選択し、左側のペインの「Edit」を押すと、CoqIDEが起動する。
左から7番目の「一番下まで行く」ボタンを押すと、証明を最後まで検証しようとしてくれる。
しかし、途中で止まってしまう。
これを証明してみよう。該当箇所を以下のように変更して、左側から3番目のボタンを使って一歩ずつ進んでみればよい。
Coqに関する詳しい説明は、随所でなされているので、ググるべし。
(* YOU MAY EDIT THE PROOF BELOW *) intuition. (* ソースコード中の条件式(a<b)に応じた場合分けはKrakatoaが行ってくれているので、 * それぞれについて証明を行えば良い。 *) (* a>bのときの、第1条件(どちらかと等しい) *) (* A or Bの左側が正しいので *) left. (* return1 = aを代入 *) rewrite H1. (* 両辺が同じなので *) reflexivity. (* a>bのときの、第2条件(a以上) *) (* return1 = aを代入 *) rewrite H1. (* 整数不等式の証明 *) omega. (* a>bのときの、第3条件(b以上) *) (* return1 = aを代入 *) rewrite H1. (* 整数不等式の証明 *) omega. (* !(a>b)のときの、第1条件(どちらかと等しい) *) (* A or Bの右側が正しいので *) right. (* return1 = bを代入 *) rewrite H1. (* 両辺が同じなので *) reflexivity. (* a>bのときの、第2条件(a以上) *) (* return1 = bを代入 *) rewrite H1. (* 整数不等式の証明 *) omega. (* a>bのときの、第3条件(b以上) *) (* return1 = bを代入 *) rewrite H1. (* 整数不等式の証明 *) omega. (* 証明終了 *) Qed. (* DO NOT EDIT BELOW *)
これで、最後のQedを通過することができ、無事証明できた。
証明を保存し、CoqIDEを終了する。リスト上の「Coq 8.3pl2」を選択し、左側のペインの「Coq 8.3pl2」を押す。
すると内部でCoqが実行され、正しく検証されたことがわかる。
情報オリンピックの予選に挑戦してみる
ここでは、実装と仕様に十分な差がありながら、証明がそれほど難しくないであろう問題として、星座探しを解いてみよう。
入出力関係は証明で扱えないので、別ファイルにする。(Main.java)
import java.util.*; import java.io.*; public class Main { public static void main(String[] args) throws IOException { Scanner in = new Scanner(System.in); int m = in.nextInt(); int[] x1s = new int[m]; int[] y1s = new int[m]; for(int i = 0; i < m; i++) { x1s[i] = in.nextInt(); y1s[i] = in.nextInt(); } int n = in.nextInt(); int[] x2s = new int[n]; int[] y2s = new int[n]; for(int i = 0; i < n; i++) { x2s[i] = in.nextInt(); y2s[i] = in.nextInt(); } int[] result = Constellation.constellation(m, x1s, y1s, n, x2s, y2s); System.out.printf("%d %d\n", result[0], result[1]); } }
そして、これに呼ばれるConstellation.javaが
/*@ predicate corresponding_star_exists{L}(
@ integer m, int[] x1s, int[] y1s,
@ integer n, int[] x2s, int[] y2s,
@ integer kx, integer ky, integer i, integer j) =
@ \exists integer jj; (0 <= jj && jj < j) &&
@ (x1s[i]+kx==x2s[jj]&&y1s[i]+ky==y2s[jj]);
@*/
/*@ predicate all_star_exists{L}(
@ integer m, int[] x1s, int[] y1s,
@ integer n, int[] x2s, int[] y2s,
@ integer kx, integer ky, integer i) =
@ \forall integer ii; (0 <= ii && ii < i) ==>
@ corresponding_star_exists(m,x1s,y1s,n,x2s,y2s,kx,ky,ii,n);
@*/
/*@ predicate position_exists{L}(
@ integer m, int[] x1s, int[] y1s,
@ integer n, int[] x2s, int[] y2s,
@ integer k) =
@ \exists integer kk; (k <= kk && kk < n) &&
@ all_star_exists(m,x1s,y1s,n,x2s,y2s,x2s[kk]-x1s[0],y2s[kk]-y1s[0],m);
@*/
public class Constellation {
/*@
@ requires ((1 <= m && m <= 200) &&
@ (1 <= n && n <= 1000) &&
@ x1s != null && x1s.length == m &&
@ (\forall integer i; 0 <= i && i < m ==> 0 <= x1s[i] && x1s[i] <= 1000000) &&
@ y1s != null && y1s.length == m &&
@ (\forall integer i; 0 <= i && i < m ==> 0 <= y1s[i] && y1s[i] <= 1000000) &&
@ x2s != null && x2s.length == n &&
@ (\forall integer i; 0 <= i && i < n ==> 0 <= x2s[i] && x2s[i] <= 1000000) &&
@ y2s != null && y2s.length == n &&
@ (\forall integer i; 0 <= i && i < n ==> 0 <= y2s[i] && y2s[i] <= 1000000) &&
@ (\exists integer kx; \exists integer ky;
@ (-1000000 <= kx && kx <= 1000000) && (-1000000 <= ky && ky <= 1000000) &&
@ all_star_exists(m,x1s,y1s,n,x2s,y2s,kx,ky,m)
@ )
@ );
@
@ ensures \result != null &&
@ (\result).length == 2 &&
@ all_star_exists(m,\old(x1s),\old(y1s),n,\old(x2s),\old(y2s),(\result)[0],(\result)[1],m);
@
@*/
public static synchronized int[] constellation(final int m, final int[] x1s, final int[] y1s, final int n, final int[] x2s, final int[] y2s) {
/*@ loop_invariant (0 <= k && k <= n) &&
@ position_exists(m,x1s,y1s,n,x2s,y2s,k);
@ loop_variant n - k;
@*/
for(int k = 0; k < n; k++) {
boolean flag1 = true;
/*@ loop_invariant (0 <= i && i <= m) &&
@ (all_star_exists(m,x1s,y1s,n,x2s,y2s,x2s[k]-x1s[0],y2s[k]-y1s[0],i)
@ <==> (flag1==true));
@ loop_variant m - i;
@*/
for(int i = 0; i < m; i++) {
boolean flag2 = false;
/*@ loop_invariant (0 <= j && j <= n) &&
@ (corresponding_star_exists(m,x1s,y1s,n,x2s,y2s,x2s[k]-x1s[0],y2s[k]-y1s[0],i,j)
@ <==> (flag2==true));
@ loop_variant n - j;
@*/
for(int j = 0; j < n; j++) {
flag2 =
((x1s[i] + (x2s[k]-x1s[0]) == x2s[j]) &&
(y1s[i] + (y2s[k]-y1s[0]) == y2s[j])) || flag2;
}
flag1 = flag1 && flag2;
}
if(flag1) {
int[] ret = new int[2];
ret[0] = x2s[k]-x1s[0];
ret[1] = y2s[k]-y1s[0];
return ret;
}
}
return new int[2];
}
}
筆者の国語力と残り時間では説明が書ききれないので省略。
そして、これをKrakatoaで処理すると、Alt-Ergoで解けないものが2つ出てくる。
- メソッドconstellationの安全性
- メソッドconstellationの正当性
これをCoqコードとして出力すると、以下のような定理になる。
安全性:
Theorem WP_parameter__Constellation_constellation_safety : forall (m_2:int32), forall (x1s_2:(pointer usObject)), forall (y1s_2:(pointer usObject)), forall (n_2:int32), forall (x2s_2:(pointer usObject)), forall (y2s_2:(pointer usObject)), forall (intM_intP1:(memory usObject int32)), forall (usObject_alloc_table1:(alloc_table usObject)), ((left_valid_struct_Object y2s_2 0%Z usObject_alloc_table1) /\ ((left_valid_struct_Object x2s_2 0%Z usObject_alloc_table1) /\ ((left_valid_struct_Object y1s_2 0%Z usObject_alloc_table1) /\ ((left_valid_struct_Object x1s_2 0%Z usObject_alloc_table1) /\ ((1%Z <= (integer_of_int32 m_2))%Z /\ (((integer_of_int32 m_2) <= 200%Z)%Z /\ ((1%Z <= (integer_of_int32 n_2))%Z /\ (((integer_of_int32 n_2) <= 1000%Z)%Z /\ ((usNon_null_intM x1s_2 usObject_alloc_table1) /\ ((((offset_max usObject_alloc_table1 x1s_2) + 1%Z)%Z = (integer_of_int32 m_2)) /\ ((forall (i_1:Z), ((0%Z <= i_1)%Z /\ (i_1 < (integer_of_int32 m_2))%Z) -> ((0%Z <= (integer_of_int32 (select intM_intP1 (shift x1s_2 i_1))))%Z /\ ((integer_of_int32 (select intM_intP1 (shift x1s_2 i_1))) <= 1000000%Z)%Z)) /\ ((usNon_null_intM y1s_2 usObject_alloc_table1) /\ ((((offset_max usObject_alloc_table1 y1s_2) + 1%Z)%Z = (integer_of_int32 m_2)) /\ ((forall (i_2:Z), ((0%Z <= i_2)%Z /\ (i_2 < (integer_of_int32 m_2))%Z) -> ((0%Z <= (integer_of_int32 (select intM_intP1 (shift y1s_2 i_2))))%Z /\ ((integer_of_int32 (select intM_intP1 (shift y1s_2 i_2))) <= 1000000%Z)%Z)) /\ ((usNon_null_intM x2s_2 usObject_alloc_table1) /\ ((((offset_max usObject_alloc_table1 x2s_2) + 1%Z)%Z = (integer_of_int32 n_2)) /\ ((forall (i_3:Z), ((0%Z <= i_3)%Z /\ (i_3 < (integer_of_int32 n_2))%Z) -> ((0%Z <= (integer_of_int32 (select intM_intP1 (shift x2s_2 i_3))))%Z /\ ((integer_of_int32 (select intM_intP1 (shift x2s_2 i_3))) <= 1000000%Z)%Z)) /\ ((usNon_null_intM y2s_2 usObject_alloc_table1) /\ ((((offset_max usObject_alloc_table1 y2s_2) + 1%Z)%Z = (integer_of_int32 n_2)) /\ ((forall (i_4:Z), ((0%Z <= i_4)%Z /\ (i_4 < (integer_of_int32 n_2))%Z) -> ((0%Z <= (integer_of_int32 (select intM_intP1 (shift y2s_2 i_4))))%Z /\ ((integer_of_int32 (select intM_intP1 (shift y2s_2 i_4))) <= 1000000%Z)%Z)) /\ exists kx_1:Z, exists ky_1:Z, ((-1000000%Z)%Z <= kx_1)%Z /\ ((kx_1 <= 1000000%Z)%Z /\ (((-1000000%Z)%Z <= ky_1)%Z /\ ((ky_1 <= 1000000%Z)%Z /\ (all_star_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 kx_1 ky_1 (integer_of_int32 m_2) intM_intP1)))))))))))))))))))))))) -> forall (result:int32), ((integer_of_int32 result) = 0%Z) -> forall (k_0:int32), forall (intM_intP2:(memory usObject int32)), forall (usObject_alloc_table2:(alloc_table usObject)), ((0%Z <= (integer_of_int32 k_0))%Z /\ (((integer_of_int32 k_0) <= (integer_of_int32 n_2))%Z /\ (position_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 (integer_of_int32 k_0) intM_intP2))) -> ((((integer_of_int32 k_0) < (integer_of_int32 n_2))%Z -> forall (result1:int32), ((integer_of_int32 result1) = 0%Z) -> forall (i_5:int32), forall (flag1:bool), ((0%Z <= (integer_of_int32 i_5))%Z /\ (((integer_of_int32 i_5) <= (integer_of_int32 m_2))%Z /\ ((all_star_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 ((integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift x1s_2 0%Z))))%Z ((integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift y1s_2 0%Z))))%Z (integer_of_int32 i_5) intM_intP2) <-> (flag1 = true)))) -> ((((integer_of_int32 i_5) < (integer_of_int32 m_2))%Z -> forall (result2:int32), ((integer_of_int32 result2) = 0%Z) -> forall (j_0:int32), forall (flag2:bool), ((0%Z <= (integer_of_int32 j_0))%Z /\ (((integer_of_int32 j_0) <= (integer_of_int32 n_2))%Z /\ ((corresponding_star_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 ((integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift x1s_2 0%Z))))%Z ((integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift y1s_2 0%Z))))%Z (integer_of_int32 i_5) (integer_of_int32 j_0) intM_intP2) <-> (flag2 = true)))) -> ((((integer_of_int32 j_0) < (integer_of_int32 n_2))%Z -> ((((offset_min usObject_alloc_table2 x1s_2) <= (integer_of_int32 i_5))%Z /\ ((integer_of_int32 i_5) <= (offset_max usObject_alloc_table2 x1s_2))%Z) /\ let result3 := (select intM_intP2 (shift x1s_2 (integer_of_int32 i_5))) in ((((offset_min usObject_alloc_table2 x2s_2) <= (integer_of_int32 k_0))%Z /\ ((integer_of_int32 k_0) <= (offset_max usObject_alloc_table2 x2s_2))%Z) /\ let result4 := (select intM_intP2 (shift x2s_2 (integer_of_int32 k_0))) in ((0%Z <= (offset_max usObject_alloc_table2 x1s_2))%Z /\ let result5 := (select intM_intP2 (shift x1s_2 0%Z)) in ((((-2147483648%Z)%Z <= ((integer_of_int32 result4) - (integer_of_int32 result5))%Z)%Z /\ (((integer_of_int32 result4) - (integer_of_int32 result5))%Z <= 2147483647%Z)%Z) /\ forall (result6:int32), ((integer_of_int32 result6) = ((integer_of_int32 result4) - (integer_of_int32 result5))%Z) -> ((((-2147483648%Z)%Z <= ((integer_of_int32 result3) + (integer_of_int32 result6))%Z)%Z /\ (((integer_of_int32 result3) + (integer_of_int32 result6))%Z <= 2147483647%Z)%Z) /\ forall (result7:int32), ((integer_of_int32 result7) = ((integer_of_int32 result3) + (integer_of_int32 result6))%Z) -> ((((offset_min usObject_alloc_table2 x2s_2) <= (integer_of_int32 j_0))%Z /\ ((integer_of_int32 j_0) <= (offset_max usObject_alloc_table2 x2s_2))%Z) /\ ((((integer_of_int32 result7) = (integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 j_0))))) -> ((((offset_min usObject_alloc_table2 y1s_2) <= (integer_of_int32 i_5))%Z /\ ((integer_of_int32 i_5) <= (offset_max usObject_alloc_table2 y1s_2))%Z) /\ let result8 := (select intM_intP2 (shift y1s_2 (integer_of_int32 i_5))) in ((((offset_min usObject_alloc_table2 y2s_2) <= (integer_of_int32 k_0))%Z /\ ((integer_of_int32 k_0) <= (offset_max usObject_alloc_table2 y2s_2))%Z) /\ let result9 := (select intM_intP2 (shift y2s_2 (integer_of_int32 k_0))) in ((0%Z <= (offset_max usObject_alloc_table2 y1s_2))%Z /\ let result10 := (select intM_intP2 (shift y1s_2 0%Z)) in ((((-2147483648%Z)%Z <= ((integer_of_int32 result9) - (integer_of_int32 result10))%Z)%Z /\ (((integer_of_int32 result9) - (integer_of_int32 result10))%Z <= 2147483647%Z)%Z) /\ forall (result11:int32), ((integer_of_int32 result11) = ((integer_of_int32 result9) - (integer_of_int32 result10))%Z) -> ((((-2147483648%Z)%Z <= ((integer_of_int32 result8) + (integer_of_int32 result11))%Z)%Z /\ (((integer_of_int32 result8) + (integer_of_int32 result11))%Z <= 2147483647%Z)%Z) /\ forall (result12:int32), ((integer_of_int32 result12) = ((integer_of_int32 result8) + (integer_of_int32 result11))%Z) -> ((((offset_min usObject_alloc_table2 y2s_2) <= (integer_of_int32 j_0))%Z /\ ((integer_of_int32 j_0) <= (offset_max usObject_alloc_table2 y2s_2))%Z) /\ ((((integer_of_int32 result12) = (integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 j_0))))) -> forall (flag21:bool), (flag21 = true) -> ((((-2147483648%Z)%Z <= ((integer_of_int32 j_0) + 1%Z)%Z)%Z /\ (((integer_of_int32 j_0) + 1%Z)%Z <= 2147483647%Z)%Z) /\ forall (result13:int32), ((integer_of_int32 result13) = ((integer_of_int32 j_0) + 1%Z)%Z) -> forall (j_01:int32), (j_01 = result13) -> ((0%Z <= ((integer_of_int32 n_2) - (integer_of_int32 j_0))%Z)%Z /\ (((integer_of_int32 n_2) - (integer_of_int32 j_01))%Z < ((integer_of_int32 n_2) - (integer_of_int32 j_0))%Z)%Z))) /\ ((~ ((integer_of_int32 result12) = (integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 j_0)))))) -> forall (flag21:bool), ((flag21 = true) <-> (flag2 = true)) -> ((((-2147483648%Z)%Z <= ((integer_of_int32 j_0) + 1%Z)%Z)%Z /\ (((integer_of_int32 j_0) + 1%Z)%Z <= 2147483647%Z)%Z) /\ forall (result13:int32), ((integer_of_int32 result13) = ((integer_of_int32 j_0) + 1%Z)%Z) -> forall (j_01:int32), (j_01 = result13) -> ((0%Z <= ((integer_of_int32 n_2) - (integer_of_int32 j_0))%Z)%Z /\ (((integer_of_int32 n_2) - (integer_of_int32 j_01))%Z < ((integer_of_int32 n_2) - (integer_of_int32 j_0))%Z)%Z))))))))))) /\ ((~ ((integer_of_int32 result7) = (integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 j_0)))))) -> forall (flag21:bool), ((flag21 = true) <-> (flag2 = true)) -> ((((-2147483648%Z)%Z <= ((integer_of_int32 j_0) + 1%Z)%Z)%Z /\ (((integer_of_int32 j_0) + 1%Z)%Z <= 2147483647%Z)%Z) /\ forall (result8:int32), ((integer_of_int32 result8) = ((integer_of_int32 j_0) + 1%Z)%Z) -> forall (j_01:int32), (j_01 = result8) -> ((0%Z <= ((integer_of_int32 n_2) - (integer_of_int32 j_0))%Z)%Z /\ (((integer_of_int32 n_2) - (integer_of_int32 j_01))%Z < ((integer_of_int32 n_2) - (integer_of_int32 j_0))%Z)%Z))))))))))) /\ ((~ ((integer_of_int32 j_0) < (integer_of_int32 n_2))%Z) -> (((flag1 = true) -> forall (flag11:bool), ((flag11 = true) <-> (flag2 = true)) -> ((((-2147483648%Z)%Z <= ((integer_of_int32 i_5) + 1%Z)%Z)%Z /\ (((integer_of_int32 i_5) + 1%Z)%Z <= 2147483647%Z)%Z) /\ forall (result3:int32), ((integer_of_int32 result3) = ((integer_of_int32 i_5) + 1%Z)%Z) -> forall (i_51:int32), (i_51 = result3) -> ((0%Z <= ((integer_of_int32 m_2) - (integer_of_int32 i_5))%Z)%Z /\ (((integer_of_int32 m_2) - (integer_of_int32 i_51))%Z < ((integer_of_int32 m_2) - (integer_of_int32 i_5))%Z)%Z))) /\ ((~ (flag1 = true)) -> forall (flag11:bool), (~ (flag11 = true)) -> ((((-2147483648%Z)%Z <= ((integer_of_int32 i_5) + 1%Z)%Z)%Z /\ (((integer_of_int32 i_5) + 1%Z)%Z <= 2147483647%Z)%Z) /\ forall (result3:int32), ((integer_of_int32 result3) = ((integer_of_int32 i_5) + 1%Z)%Z) -> forall (i_51:int32), (i_51 = result3) -> ((0%Z <= ((integer_of_int32 m_2) - (integer_of_int32 i_5))%Z)%Z /\ (((integer_of_int32 m_2) - (integer_of_int32 i_51))%Z < ((integer_of_int32 m_2) - (integer_of_int32 i_5))%Z)%Z))))))) /\ ((~ ((integer_of_int32 i_5) < (integer_of_int32 m_2))%Z) -> (((flag1 = true) -> ((0%Z <= 2%Z)%Z /\ forall (usObject_tag_table1:(tag_table usObject)), forall (usObject_alloc_table3:(alloc_table usObject)), forall (result2:(pointer usObject)), ((strict_valid_struct_Object result2 0%Z (2%Z - 1%Z)%Z usObject_alloc_table3) /\ ((alloc_extends usObject_alloc_table2 usObject_alloc_table3) /\ ((alloc_fresh usObject_alloc_table2 result2 2%Z) /\ (instanceof usObject_tag_table1 result2 intM_tag)))) -> ((((offset_min usObject_alloc_table3 x2s_2) <= (integer_of_int32 k_0))%Z /\ ((integer_of_int32 k_0) <= (offset_max usObject_alloc_table3 x2s_2))%Z) /\ let result3 := (select intM_intP2 (shift x2s_2 (integer_of_int32 k_0))) in ((0%Z <= (offset_max usObject_alloc_table3 x1s_2))%Z /\ let result4 := (select intM_intP2 (shift x1s_2 0%Z)) in ((((-2147483648%Z)%Z <= ((integer_of_int32 result3) - (integer_of_int32 result4))%Z)%Z /\ (((integer_of_int32 result3) - (integer_of_int32 result4))%Z <= 2147483647%Z)%Z) /\ forall (result5:int32), ((integer_of_int32 result5) = ((integer_of_int32 result3) - (integer_of_int32 result4))%Z) -> ((((offset_min usObject_alloc_table3 y2s_2) <= (integer_of_int32 k_0))%Z /\ ((integer_of_int32 k_0) <= (offset_max usObject_alloc_table3 y2s_2))%Z) /\ let result6 := (select intM_intP2 (shift y2s_2 (integer_of_int32 k_0))) in ((0%Z <= (offset_max usObject_alloc_table3 y1s_2))%Z /\ let result7 := (select intM_intP2 (shift y1s_2 0%Z)) in ((((-2147483648%Z)%Z <= ((integer_of_int32 result6) - (integer_of_int32 result7))%Z)%Z /\ (((integer_of_int32 result6) - (integer_of_int32 result7))%Z <= 2147483647%Z)%Z) /\ forall (result8:int32), ((integer_of_int32 result8) = ((integer_of_int32 result6) - (integer_of_int32 result7))%Z) -> ((1%Z <= (offset_max usObject_alloc_table3 result2))%Z /\ (0%Z <= (offset_max usObject_alloc_table3 result2))%Z))))))))) /\ ((~ (flag1 = true)) -> ((((-2147483648%Z)%Z <= ((integer_of_int32 k_0) + 1%Z)%Z)%Z /\ (((integer_of_int32 k_0) + 1%Z)%Z <= 2147483647%Z)%Z) /\ forall (result2:int32), ((integer_of_int32 result2) = ((integer_of_int32 k_0) + 1%Z)%Z) -> forall (k_01:int32), (k_01 = result2) -> ((0%Z <= ((integer_of_int32 n_2) - (integer_of_int32 k_0))%Z)%Z /\ (((integer_of_int32 n_2) - (integer_of_int32 k_01))%Z < ((integer_of_int32 n_2) - (integer_of_int32 k_0))%Z)%Z))))))) /\ ((~ ((integer_of_int32 k_0) < (integer_of_int32 n_2))%Z) -> (0%Z <= 2%Z)%Z)). (* YOU MAY EDIT THE PROOF BELOW *) Qed. (* DO NOT EDIT BELOW *)
正当性:
Theorem WP_parameter__Constellation_constellation_ensures_default : forall (m_2:int32), forall (x1s_2:(pointer usObject)), forall (y1s_2:(pointer usObject)), forall (n_2:int32), forall (x2s_2:(pointer usObject)), forall (y2s_2:(pointer usObject)), forall (intM_intP1:(memory usObject int32)), forall (usObject_alloc_table1:(alloc_table usObject)), ((left_valid_struct_Object y2s_2 0%Z usObject_alloc_table1) /\ ((left_valid_struct_Object x2s_2 0%Z usObject_alloc_table1) /\ ((left_valid_struct_Object y1s_2 0%Z usObject_alloc_table1) /\ ((left_valid_struct_Object x1s_2 0%Z usObject_alloc_table1) /\ ((1%Z <= (integer_of_int32 m_2))%Z /\ (((integer_of_int32 m_2) <= 200%Z)%Z /\ ((1%Z <= (integer_of_int32 n_2))%Z /\ (((integer_of_int32 n_2) <= 1000%Z)%Z /\ ((usNon_null_intM x1s_2 usObject_alloc_table1) /\ ((((offset_max usObject_alloc_table1 x1s_2) + 1%Z)%Z = (integer_of_int32 m_2)) /\ ((forall (i_1:Z), ((0%Z <= i_1)%Z /\ (i_1 < (integer_of_int32 m_2))%Z) -> ((0%Z <= (integer_of_int32 (select intM_intP1 (shift x1s_2 i_1))))%Z /\ ((integer_of_int32 (select intM_intP1 (shift x1s_2 i_1))) <= 1000000%Z)%Z)) /\ ((usNon_null_intM y1s_2 usObject_alloc_table1) /\ ((((offset_max usObject_alloc_table1 y1s_2) + 1%Z)%Z = (integer_of_int32 m_2)) /\ ((forall (i_2:Z), ((0%Z <= i_2)%Z /\ (i_2 < (integer_of_int32 m_2))%Z) -> ((0%Z <= (integer_of_int32 (select intM_intP1 (shift y1s_2 i_2))))%Z /\ ((integer_of_int32 (select intM_intP1 (shift y1s_2 i_2))) <= 1000000%Z)%Z)) /\ ((usNon_null_intM x2s_2 usObject_alloc_table1) /\ ((((offset_max usObject_alloc_table1 x2s_2) + 1%Z)%Z = (integer_of_int32 n_2)) /\ ((forall (i_3:Z), ((0%Z <= i_3)%Z /\ (i_3 < (integer_of_int32 n_2))%Z) -> ((0%Z <= (integer_of_int32 (select intM_intP1 (shift x2s_2 i_3))))%Z /\ ((integer_of_int32 (select intM_intP1 (shift x2s_2 i_3))) <= 1000000%Z)%Z)) /\ ((usNon_null_intM y2s_2 usObject_alloc_table1) /\ ((((offset_max usObject_alloc_table1 y2s_2) + 1%Z)%Z = (integer_of_int32 n_2)) /\ ((forall (i_4:Z), ((0%Z <= i_4)%Z /\ (i_4 < (integer_of_int32 n_2))%Z) -> ((0%Z <= (integer_of_int32 (select intM_intP1 (shift y2s_2 i_4))))%Z /\ ((integer_of_int32 (select intM_intP1 (shift y2s_2 i_4))) <= 1000000%Z)%Z)) /\ exists kx_1:Z, exists ky_1:Z, ((-1000000%Z)%Z <= kx_1)%Z /\ ((kx_1 <= 1000000%Z)%Z /\ (((-1000000%Z)%Z <= ky_1)%Z /\ ((ky_1 <= 1000000%Z)%Z /\ (all_star_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 kx_1 ky_1 (integer_of_int32 m_2) intM_intP1)))))))))))))))))))))))) -> forall (result:int32), ((integer_of_int32 result) = 0%Z) -> (((0%Z <= (integer_of_int32 result))%Z /\ (((integer_of_int32 result) <= (integer_of_int32 n_2))%Z /\ (position_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 (integer_of_int32 result) intM_intP1))) /\ forall (k_0:int32), forall (intM_intP2:(memory usObject int32)), forall (usObject_alloc_table2:(alloc_table usObject)), ((0%Z <= (integer_of_int32 k_0))%Z /\ (((integer_of_int32 k_0) <= (integer_of_int32 n_2))%Z /\ (position_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 (integer_of_int32 k_0) intM_intP2))) -> ((((integer_of_int32 k_0) < (integer_of_int32 n_2))%Z -> forall (result1:int32), ((integer_of_int32 result1) = 0%Z) -> (((0%Z <= (integer_of_int32 result1))%Z /\ (((integer_of_int32 result1) <= (integer_of_int32 m_2))%Z /\ ((all_star_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 ((integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift x1s_2 0%Z))))%Z ((integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift y1s_2 0%Z))))%Z (integer_of_int32 result1) intM_intP2) <-> (true = true)))) /\ forall (i_5:int32), forall (flag1:bool), ((0%Z <= (integer_of_int32 i_5))%Z /\ (((integer_of_int32 i_5) <= (integer_of_int32 m_2))%Z /\ ((all_star_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 ((integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift x1s_2 0%Z))))%Z ((integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift y1s_2 0%Z))))%Z (integer_of_int32 i_5) intM_intP2) <-> (flag1 = true)))) -> ((((integer_of_int32 i_5) < (integer_of_int32 m_2))%Z -> forall (result2:int32), ((integer_of_int32 result2) = 0%Z) -> (((0%Z <= (integer_of_int32 result2))%Z /\ (((integer_of_int32 result2) <= (integer_of_int32 n_2))%Z /\ ((corresponding_star_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 ((integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift x1s_2 0%Z))))%Z ((integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift y1s_2 0%Z))))%Z (integer_of_int32 i_5) (integer_of_int32 result2) intM_intP2) <-> (false = true)))) /\ forall (j_0:int32), forall (flag2:bool), ((0%Z <= (integer_of_int32 j_0))%Z /\ (((integer_of_int32 j_0) <= (integer_of_int32 n_2))%Z /\ ((corresponding_star_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 ((integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift x1s_2 0%Z))))%Z ((integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift y1s_2 0%Z))))%Z (integer_of_int32 i_5) (integer_of_int32 j_0) intM_intP2) <-> (flag2 = true)))) -> ((((integer_of_int32 j_0) < (integer_of_int32 n_2))%Z -> forall (result3:int32), ((integer_of_int32 result3) = ((integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift x1s_2 0%Z))))%Z) -> forall (result4:int32), ((integer_of_int32 result4) = ((integer_of_int32 (select intM_intP2 (shift x1s_2 (integer_of_int32 i_5)))) + (integer_of_int32 result3))%Z) -> ((((integer_of_int32 result4) = (integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 j_0))))) -> forall (result5:int32), ((integer_of_int32 result5) = ((integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift y1s_2 0%Z))))%Z) -> forall (result6:int32), ((integer_of_int32 result6) = ((integer_of_int32 (select intM_intP2 (shift y1s_2 (integer_of_int32 i_5)))) + (integer_of_int32 result5))%Z) -> ((((integer_of_int32 result6) = (integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 j_0))))) -> forall (flag21:bool), (flag21 = true) -> forall (result7:int32), ((integer_of_int32 result7) = ((integer_of_int32 j_0) + 1%Z)%Z) -> forall (j_01:int32), (j_01 = result7) -> ((0%Z <= (integer_of_int32 j_01))%Z /\ (((integer_of_int32 j_01) <= (integer_of_int32 n_2))%Z /\ ((corresponding_star_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 ((integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift x1s_2 0%Z))))%Z ((integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift y1s_2 0%Z))))%Z (integer_of_int32 i_5) (integer_of_int32 j_01) intM_intP2) <-> (flag21 = true))))) /\ ((~ ((integer_of_int32 result6) = (integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 j_0)))))) -> forall (flag21:bool), ((flag21 = true) <-> (flag2 = true)) -> forall (result7:int32), ((integer_of_int32 result7) = ((integer_of_int32 j_0) + 1%Z)%Z) -> forall (j_01:int32), (j_01 = result7) -> ((0%Z <= (integer_of_int32 j_01))%Z /\ (((integer_of_int32 j_01) <= (integer_of_int32 n_2))%Z /\ ((corresponding_star_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 ((integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift x1s_2 0%Z))))%Z ((integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift y1s_2 0%Z))))%Z (integer_of_int32 i_5) (integer_of_int32 j_01) intM_intP2) <-> (flag21 = true))))))) /\ ((~ ((integer_of_int32 result4) = (integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 j_0)))))) -> forall (flag21:bool), ((flag21 = true) <-> (flag2 = true)) -> forall (result5:int32), ((integer_of_int32 result5) = ((integer_of_int32 j_0) + 1%Z)%Z) -> forall (j_01:int32), (j_01 = result5) -> ((0%Z <= (integer_of_int32 j_01))%Z /\ (((integer_of_int32 j_01) <= (integer_of_int32 n_2))%Z /\ ((corresponding_star_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 ((integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift x1s_2 0%Z))))%Z ((integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift y1s_2 0%Z))))%Z (integer_of_int32 i_5) (integer_of_int32 j_01) intM_intP2) <-> (flag21 = true))))))) /\ ((~ ((integer_of_int32 j_0) < (integer_of_int32 n_2))%Z) -> (((flag1 = true) -> forall (flag11:bool), ((flag11 = true) <-> (flag2 = true)) -> forall (result3:int32), ((integer_of_int32 result3) = ((integer_of_int32 i_5) + 1%Z)%Z) -> forall (i_51:int32), (i_51 = result3) -> ((0%Z <= (integer_of_int32 i_51))%Z /\ (((integer_of_int32 i_51) <= (integer_of_int32 m_2))%Z /\ ((all_star_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 ((integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift x1s_2 0%Z))))%Z ((integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift y1s_2 0%Z))))%Z (integer_of_int32 i_51) intM_intP2) <-> (flag11 = true))))) /\ ((~ (flag1 = true)) -> forall (flag11:bool), (~ (flag11 = true)) -> forall (result3:int32), ((integer_of_int32 result3) = ((integer_of_int32 i_5) + 1%Z)%Z) -> forall (i_51:int32), (i_51 = result3) -> ((0%Z <= (integer_of_int32 i_51))%Z /\ (((integer_of_int32 i_51) <= (integer_of_int32 m_2))%Z /\ ((all_star_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 ((integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift x1s_2 0%Z))))%Z ((integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift y1s_2 0%Z))))%Z (integer_of_int32 i_51) intM_intP2) <-> (flag11 = true)))))))))) /\ ((~ ((integer_of_int32 i_5) < (integer_of_int32 m_2))%Z) -> (((flag1 = true) -> forall (usObject_tag_table1:(tag_table usObject)), forall (usObject_alloc_table3:(alloc_table usObject)), forall (result2:(pointer usObject)), ((strict_valid_struct_Object result2 0%Z (2%Z - 1%Z)%Z usObject_alloc_table3) /\ ((alloc_extends usObject_alloc_table2 usObject_alloc_table3) /\ ((alloc_fresh usObject_alloc_table2 result2 2%Z) /\ (instanceof usObject_tag_table1 result2 intM_tag)))) -> forall (result3:int32), ((integer_of_int32 result3) = ((integer_of_int32 (select intM_intP2 (shift x2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift x1s_2 0%Z))))%Z) -> forall (result4:int32), ((integer_of_int32 result4) = ((integer_of_int32 (select intM_intP2 (shift y2s_2 (integer_of_int32 k_0)))) - (integer_of_int32 (select intM_intP2 (shift y1s_2 0%Z))))%Z) -> forall (intM_intP3:(memory usObject int32)), ((not_assigns usObject_alloc_table3 intM_intP2 intM_intP3 (pset_range (pset_singleton result2) 0%Z 1%Z)) /\ (((select intM_intP3 (shift result2 0%Z)) = result3) /\ ((select intM_intP3 (shift result2 1%Z)) = result4))) -> forall (return1:(pointer usObject)), (return1 = result2) -> ((usNon_null_intM return1 usObject_alloc_table3) /\ ((((offset_max usObject_alloc_table3 return1) + 1%Z)%Z = 2%Z) /\ (all_star_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 (integer_of_int32 (select intM_intP3 (shift return1 0%Z))) (integer_of_int32 (select intM_intP3 (shift return1 1%Z))) (integer_of_int32 m_2) intM_intP3)))) /\ ((~ (flag1 = true)) -> forall (result2:int32), ((integer_of_int32 result2) = ((integer_of_int32 k_0) + 1%Z)%Z) -> forall (k_01:int32), (k_01 = result2) -> ((0%Z <= (integer_of_int32 k_01))%Z /\ (((integer_of_int32 k_01) <= (integer_of_int32 n_2))%Z /\ (position_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 (integer_of_int32 k_01) intM_intP2))))))))) /\ ((~ ((integer_of_int32 k_0) < (integer_of_int32 n_2))%Z) -> forall (usObject_tag_table1:(tag_table usObject)), forall (usObject_alloc_table3:(alloc_table usObject)), forall (result1:(pointer usObject)), ((strict_valid_struct_Object result1 0%Z (2%Z - 1%Z)%Z usObject_alloc_table3) /\ ((alloc_extends usObject_alloc_table2 usObject_alloc_table3) /\ ((alloc_fresh usObject_alloc_table2 result1 2%Z) /\ (instanceof usObject_tag_table1 result1 intM_tag)))) -> forall (return1:(pointer usObject)), (return1 = result1) -> ((usNon_null_intM return1 usObject_alloc_table3) /\ ((((offset_max usObject_alloc_table3 return1) + 1%Z)%Z = 2%Z) /\ (all_star_exists (integer_of_int32 m_2) x1s_2 y1s_2 (integer_of_int32 n_2) x2s_2 y2s_2 (integer_of_int32 (select intM_intP2 (shift return1 0%Z))) (integer_of_int32 (select intM_intP2 (shift return1 1%Z))) (integer_of_int32 m_2) intM_intP2)))))). (* YOU MAY EDIT THE PROOF BELOW *) Qed. (* DO NOT EDIT BELOW *)
なんだか気が遠くなるような定理だが、これを気が遠くなりながら証明したのが以下である。なんと解説つき。
安全性:
(* 安全性の証明のほとんどは整数不等式なので、ほとんどomega
* ex1: intの足し算がオーバーフローしないこと
* ex2: 配列のインデックスが範囲内であること
* ex3: 無限ループがないこと <== ある整数式が常に非負で単調減少であることを示す
*)
(* omegaの妨げになりそうなものは予め処理しておく *)
unfold left_valid_struct_Object.
unfold position_exists, all_star_exists, corresponding_star_exists.
intros m x1s y1s n x2s y2s intM_intP1 usObject_alloc_table1
(K0,
(K1,
(K2,
(K3,
(K4,
(K5,
(K6,
(K7,
(K8,
(K9,
(K10,
(K11, (K12, (K13, (K14, (K15, (K16, (K17, (K18, (K19, _))))))))))))))))))))
_ _ k intM_intP2 usObject_alloc_table2 (Hrk0, (Hrk1, _)).
split; [ idtac | omega ].
intros Hrk2 _ _ i flag1 (Hri0, (Hri1, _)).
(* 証明できないバグっぽいのでズルして証明回避 *)
replace intM_intP2 with intM_intP1 in * by admit; clear intM_intP2.
replace usObject_alloc_table2 with usObject_alloc_table1 in * by admit;
clear usObject_alloc_table2.
(* omegaに食わせる定理をあらかじめ作っておく *)
pose proof (K16 (integer_of_int32 k) (conj Hrk0 Hrk2)) as K16k.
pose proof (K19 (integer_of_int32 k) (conj Hrk0 Hrk2)) as K19k.
assert (0 <= 0 < integer_of_int32 m) as range0 by complete omega.
pose proof (K10 0 range0) as K10z.
pose proof (K13 0 range0) as K13z.
(* 以下作業 *)
split.
intros Hri2 _ _ j flag2 (Hrj0, (Hrj1, _)).
pose proof (K10 (integer_of_int32 i) (conj Hri0 Hri2)) as K10i.
pose proof (K13 (integer_of_int32 i) (conj Hri0 Hri2)) as K13i.
split.
intros Hrj2.
split; [ omega | idtac ].
split; [ omega | idtac ].
split; [ omega | idtac ].
split; [ omega | idtac ].
intros r rw; rewrite rw; clear r rw.
split; [ omega | idtac ].
intros r rw; rewrite rw; clear r rw.
split; [ omega | idtac ].
split.
intros _.
split; [ omega | idtac ].
split; [ omega | idtac ].
split; [ omega | idtac ].
split; [ omega | idtac ].
intros r rw; rewrite rw; clear r rw.
split; [ omega | idtac ].
intros r rw; rewrite rw; clear r rw.
split; [ omega | idtac ].
split.
intros _ _ _.
split; [ omega | idtac ].
intros r0 rw0 r1 rw1; rewrite rw1, rw0; clear r0 rw0 r1 rw1.
split; omega.
intros _ _ _.
split; [ omega | idtac ].
intros r0 rw0 r1 rw1; rewrite rw1, rw0; clear r0 rw0 r1 rw1.
split; omega.
intros _ _ _.
split; [ omega | idtac ].
intros r0 rw0 r1 rw1; rewrite rw1, rw0; clear r0 rw0 r1 rw1.
split; omega.
intros _.
split.
intros _ _ _.
split; [ omega | idtac ].
intros r0 rw0 r1 rw1; rewrite rw1, rw0; clear r0 rw0 r1 rw1.
split; omega.
intros _ _ _.
split; [ omega | idtac ].
intros r0 rw0 r1 rw1; rewrite rw1, rw0; clear r0 rw0 r1 rw1.
split; omega.
intros _.
split.
intros _.
split; [ omega | idtac ].
intros usObject_tag_table1 usObject_alloc_table3 ret
((T0a, T0b), (T1, (T2, T3))).
repeat
(rewrite <- (alloc_extends_offset_min _ _ _ T1); [ idtac | split; omega ]).
repeat
(rewrite <- (alloc_extends_offset_max _ _ _ T1); [ idtac | split; omega ]).
split; [ omega | idtac ].
split; [ omega | idtac ].
split; [ omega | idtac ].
intros _ _.
split; [ omega | idtac ].
split; [ omega | idtac ].
split; [ omega | idtac ].
intros _ _.
split; omega.
intros _.
split; [ omega | idtac ].
intros r0 rw0 r1 rw1; rewrite rw1, rw0; clear r0 rw0 r1 rw1.
omega.
正当性:
(* 補助的な定理の証明 *)
assert (forall x y, x < y + 1 -> x < y \/ x = y) as PlusOne by complete
(intros; omega).
assert (forall x y, x <= y -> ~ x < y -> x = y) as LtEq by complete
(intros; omega).
(* 全ての定理に共通する前提を取り出す *)
intros m x1s y1s n x2s y2s intM_intP1 usObject_alloc_table1
(K0,
(K1,
(K2,
(K3,
(K4,
(K5,
(K6,
(K7,
(K8,
(K9,
(K10,
(K11,
(K12,
(K13,
(K14,
(K15,
(K16,
(K17,
(K18,
(K19, (kx, (ky, (Hkx0, (Hkx1, (Hky0, (Hky1, K20)))))))))))))))))))))))))).
(* 一時変数はその場で書き換えて破棄 *)
intros r rw; rewrite rw; clear r rw.
split.
(* 1番目のループに最初に入る時に不変条件を満たすことの証明 *)
split; [ omega | idtac ].
split; [ omega | idtac ].
destruct (K20 0) as (k, (Hk0, (Hk1, (Hk2, Hk3)))); [ omega | idtac ].
exists k.
split; [ auto | idtac ].
split; [ auto | idtac ].
replace
(integer_of_int32 (select intM_intP1 (shift x2s k)) -
integer_of_int32 (select intM_intP1 (shift x1s 0))) with kx
by omega.
replace
(integer_of_int32 (select intM_intP1 (shift y2s k)) -
integer_of_int32 (select intM_intP1 (shift y1s 0))) with ky
by omega.
apply K20.
(* 1番目のループの内側に関する諸証明 *)
intros k intM_intP2 usObject_alloc_table2.
(* intM_intP2とusObject_alloc_table2はおそらくバグで証明できないので、少しズルをする *)
replace intM_intP2 with intM_intP1 in * by admit; clear intM_intP2.
replace usObject_alloc_table2 with usObject_alloc_table1 in * by admit;
clear usObject_alloc_table2.
intros (Hrk0, (Hrk1, Hk0)).
split.
(* k < n (ループ継続) の場合の証明 *)
intros Hrk2.
intros r rw; rewrite rw; clear r rw.
split.
(* 2番目のループに最初に入る時に不変条件を満たすことの証明 *)
split; [ omega | idtac ].
split; [ omega | idtac ].
split; [ auto | intros _ ].
intros ii Hii; apply False_ind; omega.
(* 2番目のループの内側に関する諸証明 *)
intros i flag1 (Hri0, (Hri1, Hi)).
split.
(* i < m (ループ継続) の場合の証明 *)
intros Hri2.
intros r rw; rewrite rw; clear r rw.
split.
(* 3番目のループに最初に入る時に不変条件を満たすことの証明 *)
split; [ clear Hi; omega | idtac ].
split; [ clear Hi; omega | idtac ].
split; [ intro H; apply False_ind | congruence ].
destruct H as (jj, (Hjj0, (Hjj1, H))); clear Hi; omega.
(* 3番目のループの内側に関する諸証明 *)
intros j flag2 (Hrj0, (Hrj1, Hj)).
split.
(* j < n (ループ継続) の場合の証明 *)
intros Hrj2.
intros r rw; rewrite rw; clear r rw.
intros r rw; rewrite rw; clear r rw.
(* 3番目のループの継続時に不変条件を満たすことの証明 *)
split.
(* x1s[i] + (x2s[k]-x1s[0]) == x2s[j] のときの証明 *)
intros HH0.
intros r rw; rewrite rw; clear r rw.
intros r rw; rewrite rw; clear r rw.
split.
(* y1s[i] + (y2s[k]-y1s[0]) == y2s[j] のときの証明 *)
intros HH1.
intros r rw; rewrite rw; clear r rw.
intros r0 rw0 r1 rw1; rewrite rw1, rw0; clear r0 rw0 r1 rw1.
split; [ clear Hi Hj; omega | idtac ].
split; [ clear Hi Hj; omega | idtac ].
split; [ auto | intros _ ].
exists (integer_of_int32 j).
split; [ clear Hi Hj; omega | idtac ].
split; [ clear Hi Hj; omega | idtac ].
split; (clear Hi Hj; omega).
(* y1s[i] + (y2s[k]-y1s[0]) != y2s[j] のときの証明 *)
intros HH1.
intros flag2a Hflag2a.
intros r0 rw0 r1 rw1; rewrite rw1, rw0; clear r0 rw0 r1 rw1.
split; [ clear Hi Hj Hflag2a; omega | idtac ].
split; [ clear Hi Hj Hflag2a; omega | idtac ].
rewrite Hflag2a, <- Hj.
(* 条件の同値性を証明するので、必要性と十分性に分割 *)
split.
intros (jj, (Hrjj0, (Hrjj1, (Hjj0, Hjj1)))).
apply PlusOne in Hrjj1.
destruct Hrjj1 as [Hrjj1| Hrjj1].
exists jj.
split; [ clear Hi Hj Hflag2a; omega | idtac ].
split; [ clear Hi Hj Hflag2a; omega | idtac ].
split; (clear Hi Hj Hflag2a; omega).
rewrite Hrjj1 in Hjj1; contradiction .
intros (jj, (Hrjj0, (Hrjj1, (Hjj0, Hjj1)))).
exists jj.
split; [ clear Hi Hj Hflag2a; omega | idtac ].
split; [ clear Hi Hj Hflag2a; omega | idtac ].
split; (clear Hi Hj Hflag2a; omega).
(* x1s[i] + (x2s[k]-x1s[0]) != x2s[j] のときの証明 *)
intros HH0.
intros flag2a Hflag2a.
intros r0 rw0 r1 rw1; rewrite rw1, rw0; clear r0 rw0 r1 rw1.
split; [ clear Hi Hj Hflag2a; omega | idtac ].
split; [ clear Hi Hj Hflag2a; omega | idtac ].
rewrite Hflag2a, <- Hj.
(* 条件の同値性を証明するので、必要性と十分性に分割 *)
split.
intros (jj, (Hrjj0, (Hrjj1, (Hjj0, Hjj1)))).
apply PlusOne in Hrjj1.
destruct Hrjj1 as [Hrjj1| Hrjj1].
exists jj.
split; [ clear Hi Hj Hflag2a; omega | idtac ].
split; [ clear Hi Hj Hflag2a; omega | idtac ].
split; (clear Hi Hj Hflag2a; omega).
rewrite Hrjj1 in Hjj0; contradiction .
intros (jj, (Hrjj0, (Hrjj1, (Hjj0, Hjj1)))).
exists jj.
split; [ clear Hi Hj Hflag2a; omega | idtac ].
split; [ clear Hi Hj Hflag2a; omega | idtac ].
split; (clear Hi Hj Hflag2a; omega).
(* j >= n (ループ終了) の場合の証明 *)
intros Hrj2.
split.
(* flag1 == true の場合の証明 *)
intros Hflag1.
intros flag1a Hflag1a.
intros r0 rw0 r1 rw1; rewrite rw1, rw0; clear r0 rw0 r1 rw1.
split; [ clear Hi Hj Hflag1a; omega | idtac ].
split; [ clear Hi Hj Hflag1a; omega | idtac ].
rewrite Hflag1a, <- Hj, (LtEq _ _ Hrj1 Hrj2).
(* 条件の同値性を証明するので、必要性と十分性に分割 *)
split.
intros H.
destruct (H (integer_of_int32 i))
as (jj, (Hrjj0, (Hrjj1, (Hjj0, Hjj1))));
[ clear Hi Hj Hflag1a; omega | idtac ].
exists jj.
split; [ clear Hi Hj Hflag1a; omega | idtac ].
split; [ clear Hi Hj Hflag1a; omega | idtac ].
split; (clear Hi Hj Hflag1a; omega).
intros H.
rewrite Hflag1 in Hi; destruct Hi as (_, Hi);
specialize (Hi (eq_refl _)).
intros ii (Hrii0, Hrii1).
apply PlusOne in Hrii1.
destruct Hrii1 as [Hrii1| Hrii1].
apply (Hi ii (conj Hrii0 Hrii1)).
rewrite Hrii1; apply H.
(* flag1 != true の場合の証明 *)
intros Hflag1.
intros flag1a Hflag1a.
intros r0 rw0 r1 rw1; rewrite rw1, rw0; clear r0 rw0 r1 rw1.
split; [ clear Hi Hj Hflag1a; omega | idtac ].
split; [ clear Hi Hj Hflag1a; omega | idtac ].
split; [ idtac | contradiction ].
intros H.
rewrite <- Hi in Hflag1.
apply False_ind, Hflag1.
intros ii (Hrii0, Hrii1).
apply H; (clear Hi Hj Hflag1a; omega).
(* i < m (ループ終了) の場合の証明 *)
intros Hri2.
split.
(* flag1 == true の場合 ( return ) の証明 *)
intros Hflag1.
(* 新規配列の生成をするので、新たなメモリ空間が出現する *)
intros usObject_tag_table1 usObject_alloc_table3 ret
(Ht0, (Ht1, (Ht2, Ht3))).
intros r0 rw0 r1 rw1.
intros intM_intP3 (HP0, (HP1, HP2)).
intros r2 rw2.
rewrite rw2, HP1, HP2, rw0, rw1; clear r0 r1 r2 rw0 rw1 rw2 HP1 HP2.
(* メソッドが終了時に満たすべき条件の証明 *)
split.
(* 戻り値はnullではないことの証明 *)
unfold usNon_null_intM.
unfold strict_valid_struct_Object in Ht0.
clear Hi; omega.
split.
(* 戻り値の配列の長さは2であることの証明 *)
unfold strict_valid_struct_Object in Ht0.
clear Hi; omega.
(* 戻り値が条件を満たすことの証明 *)
rewrite Hflag1 in Hi; destruct Hi as (_, Hi);
specialize (Hi (eq_refl _)).
intros ii Hii.
destruct (Hi ii) as (jj, (Hrjj0, (Hrjj1, (Hjj0, Hjj1))));
[ omega | idtac ].
exists jj.
split; [ omega | idtac ].
split; [ omega | idtac ].
unfold left_valid_struct_Object in K0, K1, K2, K3.
(* intM_intP3をintM_intP1にすげ替える作業。 *)
repeat rewrite HP0; [ intuition | idtac | idtac | idtac | idtac ];
(split;
[ unfold valid;
(rewrite <- (alloc_extends_offset_min _ usObject_alloc_table1);
[ idtac
| auto
| unfold valid; rewrite offset_min_shift, offset_max_shift;
omega ]);
(rewrite <- (alloc_extends_offset_max _ usObject_alloc_table1);
[ idtac
| auto
| unfold valid; rewrite offset_min_shift, offset_max_shift;
omega ]); rewrite offset_min_shift, offset_max_shift;
omega; auto
| rewrite in_pset_range; intros (x, (y, (Hx0, (Hx1, (H0, H1)))));
rewrite in_pset_singleton in H0; rewrite H0 in H1;
(apply Ht2 with (i := x); [ omega | idtac ]);
rewrite <- H1;
(unfold valid; rewrite offset_min_shift, offset_max_shift;
omega) ]).
(* flag1 != true の場合 ( returnせずループ継続 ) のとき *)
(* 1番目のループが不変条件を満たすことの証明 *)
intros Hflag1.
intros r0 rw0 r1 rw1; rewrite rw1, rw0; clear r0 rw0 r1 rw1.
split; [ clear Hi; omega | idtac ].
split; [ clear Hi; omega | idtac ].
rewrite (LtEq _ _ Hri1 Hri2) in Hi.
destruct Hk0 as (kk, (Hrkk0, (Hrkk1, Hkk))).
assert (integer_of_int32 k + 1 <= kk \/ integer_of_int32 k = kk)
as Hrkk2 by complete (clear Hkk Hi; omega).
destruct Hrkk2 as [Hrkk2| Hrkk2].
exists kk.
split; [ clear Hkk Hi; omega | idtac ].
split; [ clear Hkk Hi; omega | idtac ].
apply Hkk.
rewrite Hrkk2 in Hi.
rewrite Hi in Hkk.
contradiction .
(* 最後のreturnのときにメソッドが満たすべき条件の証明 *)
(* …だが、この場所には到達しないことを証明すればよい(矛盾を導けば良い) *)
intros Hrk2.
rewrite (LtEq _ _ Hrk1 Hrk2) in Hk0.
destruct Hk0 as (kk, (Hrkk0, (Hrkk1, Hkk))).
exfalso; omega.
FAQ
- Q1. お疲れ様でした。
- A1. ……(無言)
- Q2. なんでこんなに難しいんですか？
- A2. 理由は2つ考えられます。1つは、形式的定理証明そのものの難しさ。Coqも非常に良いサポートをしているとはいえ、人間の感覚に近い証明ができるとはとても言い難いです。これは進歩を待つのみです。もう1つは、手続き型言語の証明をしているという点。状態遷移があったり、リファレンスの扱いが難しかったりと、この手の言語は証明に向かない要素を多数含んでいるといえます。
- Q3. 証明中に「定理生成自体にバグがあり、証明できないから、新たに仮定を導入する」という主旨の内容がありました。証明系自体にバグがあったら証明の意味がないのでは？
- A3. 証明は、あくまでテストの延長上にあると思います。つまり、論理を用いて網羅性の高いテストを行えるというわけです。あくまで我々の直感的な推論中にありがちな見落としを避けるためだと考えれば、証明系自体のバグが必ずしも致命的とは言えないでしょう。
- Q4. というかぶっちゃけ、これって意味あるんですか？
- A4. 今のところは、ハッキリいって、ほとんど無いです。anarchy proofだって、遊びの一種でしょう。ただ、我々(少なくとも筆者)は形式的定理証明の黎明期の時代にいるのだと、信じています。
