次の注釈付き C コードがあるとします。
int a[3] = {0};
/*@ requires \valid(a+(0..2));
assigns a[0..2];
ensures \forall int j; 0 <= j < 3 ==> (a[j] == j); */
int main() {
int i = 0;
/*@ loop assigns i, a[0..(i-1)];
loop invariant inv1: 0 <= i <= 3;
loop invariant inv2:
\forall int k; 0 < k <= i ==> a[k-1] == k-1; */
while (i < L) {
a[i] = i;
i++;
}
//@ assert final_i: i == 3;
//@ assert final_a: a[1] == 1;
}
Z3 も Alt-ergo も、アサート final_a と事後条件を証明できません。Z3 はループ不変式も証明できません。
Alt-Ergo の出力:
# ~/queue $ frama-c -wp -wp-prover alt-ergo test2.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing test2.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 14 goals scheduled
[wp] [Qed] Goal typed_main_pre : Valid
[wp] [Qed] Goal typed_main_loop_inv_inv1_established : Valid
[wp] [Qed] Goal typed_main_loop_inv_inv2_established : Valid
[wp] [Qed] Goal typed_main_assert_final_i : Valid
[wp] [Alt-Ergo] Goal typed_main_loop_inv_inv1_preserved : Valid (Qed:1ms) (14ms) (15)
[wp] [Qed] Goal typed_main_loop_assign_part1 : Valid
[wp] [Alt-Ergo] Goal typed_main_loop_inv_inv2_preserved : Valid (45ms) (51)
[wp] [Qed] Goal typed_main_loop_assign_part2 : Valid
[wp] [Qed] Goal typed_main_loop_assign_part3 : Valid
[wp] [Qed] Goal typed_main_assign_part1 : Valid
[wp] [Qed] Goal typed_main_assign_part3 : Valid
[wp] [Alt-Ergo] Goal typed_main_assign_part2 : Valid (20ms) (12)
[wp] [Alt-Ergo] Goal typed_main_assert_final_a : Unknown (3.5s)
[wp] [Alt-Ergo] Goal typed_main_post : Timeout (Qed:1ms)
[wp] Proved goals: 12 / 14
Qed: 9 (0ms-1ms)
Alt-Ergo: 3 (14ms-45ms) (51) (interrupted: 1) (unknown: 1)
Z3 の出力:
$ frama-c -wp -wp-prover z3 test2.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing test2.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 14 goals scheduled
[wp] [Qed] Goal typed_main_pre : Valid
[wp] [Qed] Goal typed_main_loop_inv_inv1_established : Valid
[wp] [Qed] Goal typed_main_loop_inv_inv2_established : Valid
[wp] [Qed] Goal typed_main_assert_final_i : Valid
[wp] [z3] Goal typed_main_loop_inv_inv1_preserved : Valid (20ms)
[wp] [Qed] Goal typed_main_loop_assign_part1 : Valid
[wp] [Qed] Goal typed_main_loop_assign_part2 : Valid
[wp] [Qed] Goal typed_main_loop_assign_part3 : Valid
[wp] [Qed] Goal typed_main_assign_part1 : Valid
[wp] [z3] Goal typed_main_assert_final_a : Unknown (356ms)
[wp] [Qed] Goal typed_main_assign_part3 : Valid
[wp] [z3] Goal typed_main_post : Unknown (911ms)
[wp] [z3] Goal typed_main_assign_part2 : Valid (10ms)
[wp] [z3] Goal typed_main_loop_inv_inv2_preserved : Unknown (1.3s)
[wp] Proved goals: 11 / 14
Qed: 9
z3: 2 (10ms-20ms) (unknown: 3)
何が欠けている？