I try to use Frama-C to prove the invariant below. With the precondition that the array clean has at least one "true" in the first half, the loop should terminate before the last iteration and hence i will never be increased to BLOCK_NUM (=1000). However, Frama-C seems to ignore the content of clean and failed to establish the loop invariant. Does anyone know how to fix this proof?
#include <stdio.h>
#include <stdlib.h>
#include <stdbool.h>
#include <assert.h>
#define BLOCK_NUM 1000
bool clean[BLOCK_NUM] ; // clean bit for physical block; phy block ID -> bool
/*@
requires \exists integer j; 0 <= j < BLOCK_NUM/2 ==> clean[j] == true;
*/
void test(){
int i = 0;
/*@
loop assigns i;
loop invariant 0 <= i < BLOCK_NUM;
*/
while( i < BLOCK_NUM && clean[i] == false ){
i += 1;
}
}
I also tried a different version adding more information to the invariant
void test(){
int i = 0;
/*@
loop assigns i;
loop invariant 0 <= i < BLOCK_NUM &&
\exists integer j; i <= j < BLOCK_NUM/2 ==> clean[j] == true;
*/
while( i < BLOCK_NUM && clean[i] == false ){
i += 1;
}
//@ assert 0 <= i < BLOCK_NUM;
}
This translates to the following proof condition.
Goal Invariant (preserved):
Assume {
Type: is_sint32(i@L4) /\ is_sint32(1 + i@L4).
[...]
Stmt { L4: }
(* Invariant *)
Have: (0 <= i@L4) /\ (i@L4 <= 999) /\
(((i@L4 <= i_3) -> ((i_3 <= 499) -> (clean@L1[i_3] = 1)))).
(* Then *)
Have: clean@L1[i@L4] = 0.
}
Prove: ((-1) <= i@L4) /\ (i@L4 <= 998) /\
(exists i_4 : Z. ((i@L4 < i_4) -> ((i_4 <= 499) -> (clean@L1[i_4] = 1)))).
--------------------------------------------------------------------------------
Prover Alt-Ergo 2.4.1: Timeout (Qed:101ms) (10s) (cached).
But still all solvers (including Z3 and CVC4) fail to show it.
There are two issues in your specification. First, your precondition is incorrect. What you want to say is that there exists a j such that j is between appropriate bounds and clean[j] == true, i.e.
requires \exists integer j; 0 <= j < BLOCK_NUM/2 && clean[j] == true;
More generally, and this can indeed be quite confusing at first, while a universal quantification generally goes along the lines of \forall x; P(x) ==> Q(x) (For any x such that P(x) holds, then Q(x) holds as well), existential quantification is usually something like \exists x, P(x) && Q(x): if you use implication instead of conjunction in that case, then any x that does not satisfy P will be a witness for the existential formula.
The second point is that your loop invariant is too weak: you don't say anything about the values you've examined so far: with just the bounds on i, it is impossible to deduce that we will eventually check the value of the cell containing true. By adding as an invariant that we have examined all the cells before i (and found false, since otherwise we wouldn't be in the loop anymore), all the proofs can be completed automatically:
loop invariant all_false: \forall integer j; 0 <= j < i ==> clean[j] == false;
Note that I've also added a name all_false to the new loop invariant. As your number of clauses grows, it is useful to give them explicit names, that will be used in Frama-C's output, so that you can quickly spot which proof obligation failed.
For what it's worth, here is the complete file (I removed the unnecessary includes)
#include <stdbool.h>
#define BLOCK_NUM 1000
bool clean[BLOCK_NUM] ; // clean bit for physical block; phy block ID -> bool
/*@
requires \exists integer j; 0 <= j < BLOCK_NUM/2 && clean[j] == true;
*/
void test(){
int i = 0;
/*@
loop assigns i;
loop invariant all_false: \forall integer j; 0 <= j < i ==> clean[j] == false;
loop invariant 0 <= i < BLOCK_NUM;
*/
while( i < BLOCK_NUM && clean[i] == false ){
i += 1;
}
}