Proving simple property of a function over array

Question

Suppose we have the following annotated C-code:

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;
}

Neither Z3 nor Alt-ergo are able to prove assert final_a and post condition; Z3 is not able to prove loop invariant also;

Output for 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)

Output for 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)

What is missing?

score 0 · Accepted Answer · answered Jul 19 '15 at 23:59

0

If you change the inv2 loop invariant to:

        loop invariant inv2:
        \forall int k; 0 <= k < i ==> a[k] == k;

.. then Alt-Ergo is able to prove the final_a assertion and main() postconditions.

answered Jul 19 '15 at 23:59

Daniel Trebbien

38,421
18
121
193

Thanks! Do you have any ideas why the previous invariant isnt working? – Evgeniy Jul 20 '15 at 06:14
Do you mind to take a look at this issue also: http://stackoverflow.com/questions/31426510/the-exact-mechanism-of-mapping-whyml-into-smt-logic – Evgeniy Jul 20 '15 at 06:15
1

@Evgeniy: I am not sure why it has trouble automatically proving the final_a assertion using your original loop invariant. It has no trouble asserting `\forall ℤ k; 0 <= k-1 < 3 ==> a[k-1] == k-1` and `\forall ℤ l, k; l == k-1 ==> (0 <= l < 3 ==> a[l] == l)` after the loop. However, making that final jump to `\forall ℤ k; 0 <= k < 3 ==> a[k] == k` is not happening. – Daniel Trebbien Jul 20 '15 at 11:44
This might be also interesting issue http://stackoverflow.com/questions/31510974/smt-prover-yields-unknown-despite-strong-proven-assertions – Evgeniy Jul 20 '15 at 13:55

Proving simple property of a function over array

1 Answers1