I tried to use Frama-c to prove the occurrence of true value in an array that is the same as a integer which used to record the number of true values. But the prove failed if I want to change some values false to true. Is there any method to solve this problem? (Frama-c 25.0 / Alt-Ergo 2.4.2 / CVC4 1.8 / Z3 4.8.6)
#include <stdio.h>
#include <stdlib.h>
#include <stdbool.h>
#define SIZE 150
bool table[SIZE] = {true};
int true_counter;
/*@
logic integer count_true(integer idx) =
idx<=0 ? 0 :
(table[idx-1]==true ? count_true(idx-1) + 1 : count_true(idx-1));
*/
/*@
requires table[0] == false;
requires true_counter == count_true(SIZE);
assigns table[0], true_counter;
ensures table[0] == true;
ensures true_counter == \old(true_counter) + 1;
*/
void ATEST(void) {
int countBF = 0;
int countAF = 0;
/*@
loop invariant 0 <= idx <= SIZE;
loop invariant 0 <= countBF == count_true(idx) <= idx;
loop assigns idx, countBF;
loop variant SIZE - idx;
*/
for(int idx=0; idx<SIZE; idx++) {
if(table[idx] == true) countBF += 1;
}
//@ assert true_counter == countBF;
table[0] = true;
true_counter += 1;
/*@
loop invariant 0 <= idx <= SIZE;
loop invariant 0 <= countAF == count_true(idx) <= idx;
loop assigns idx, countAF;
loop variant SIZE - idx;
*/
for(int idx=0; idx<SIZE; idx++) {
if(table[idx] == true) countAF += 1;
}
//@ assert true_counter == countAF;
//@ assert countAF == countBF + 1;
}
[kernel] Parsing test.c (with preprocessing)
[rte:annot] annotating function ATEST
[wp] 33 goals scheduled
[wp] [Failed] Goal typed_ATEST_assert_2
Z3 4.8.6: Unknown (Qed:8ms) (cached)
CVC4 1.8: Timeout (Qed:8ms) (10s) (cached)
Alt-Ergo 2.4.2: Timeout (Qed:8ms) (10s) (cached)
[wp] [Cache] found:17
[wp] Proved goals: 32 / 33
Qed: 26 (0.84ms-7ms-24ms)
Alt-Ergo 2.4.2: 6 (7ms-13ms-27ms) (629) (interrupted: 1) (cached: 7)
CVC4 1.8: 4 (20ms-28ms-30ms) (11375) (interrupted: 1) (cached: 5)
Z3 4.8.6: 4 (10ms-20ms) (46252) (unknown: 1) (cached: 5)
The problem is that such a reasoning is not that direct. Here is what happen: when we write cell 0, WP creates a new memory whose properties are directly related to the old memory. The loop invariant of the first loop gives to the solver some information about the original memory, the loop invariant of the second loop gives information about the new memory. But for establishing the link between the two we need to learn something like "since only on value has changed, the remaining part has the same number of occurrences". Which is not possible with most SMT solvers.
For this particular example, we can be brutal and directly push the information in the invariant of the second loop:
/*@
loop invariant 0 <= idx <= SIZE;
loop invariant 0 <= countAF == count_true(idx) <= idx;
// added:
loop invariant idx >= 1 ==> countAF == 1 + count_true{Pre}(idx) <= idx;
loop assigns idx, countAF;
loop variant SIZE - idx;
*/
for(int idx=0; idx<SIZE; idx++) {
if(table[idx] == true) countAF += 1;
}
Which allows to create the link between the number of occurrences in the pre-state with the current number of occurrences. A more elegant solution is to dedicate a bit of ghost code so that it applies to any location:
/*@
requires 0 <= loc < SIZE ;
requires table[loc] == false;
requires true_counter == count_true(SIZE);
assigns table[loc], true_counter;
ensures table[loc] == true;
ensures true_counter == \old(true_counter) + 1;
*/
void ATEST(int loc) {
int countBF = 0;
int countAF = 0;
/*@
loop invariant 0 <= idx <= SIZE;
loop invariant 0 <= countBF == count_true(idx) <= idx;
loop assigns idx, countBF;
loop variant SIZE - idx;
*/
for(int idx=0; idx<SIZE; idx++) {
if(table[idx] == true) countBF += 1;
}
//@ assert true_counter == countBF;
table[loc] = true;
true_counter += 1;
/*@ ghost
/@ loop invariant 0 <= i <= loc ;
loop invariant count_true(i) == count_true{Pre}(i);
loop assigns i;
loop variant loc - i ;
@/
for(int i = 0 ; i < loc ; i++);
/@ loop invariant loc < i <= SIZE ;
loop invariant count_true(i) == 1 + count_true{Pre}(i);
loop assigns i;
loop variant SIZE - i ;
@/
for(int i = loc+1 ; i < SIZE ; i++);
*/
/*@
loop invariant 0 <= idx <= SIZE;
loop invariant 0 <= countAF == count_true(idx) <= idx;
loop assigns idx, countAF;
loop variant SIZE - idx;
*/
for(int idx=0; idx<SIZE; idx++) {
if(table[idx] == true) countAF += 1;
}
}
On can also express lemmas to handle the problem. For example the following lemmas can provide enough information to solvers so that they can finish the proof:
/*@ lemma same_count{L1,L2}:
\forall integer size; 0<= size < SIZE ==>
(\forall integer i; 0 <= i < size ==> \at(table[i], L1) == \at(table[i],L2)) ==>
count_true{L1}(size) == count_true{L2}(size);
*/
/*@ lemma same_but_one{L1,L2}:
\forall integer size; 0 <= size < SIZE ==>
\forall integer i_diff; 0 <= i_diff < size ==>
(\forall integer i; 0 <= i < size && i != i_diff ==> \at(table[i],L1) == \at(table[i],L2))
&& \at(table[i_diff],L1) == false && \at(table[i_diff],L2) == true
==>
count_true{L1}(size) + 1 == count_true{L2}(size);
*/
The first lemma states that an unchanged memory region keeps the same number of occurrences as before. The second states that when in a state a cell has true while in another it is false and all remaining cells are the same, the number of occurrences changes by one. These two lemmas can be verified via the induction tactic (see for example https://stackoverflow.com/a/73796135/4628125).
These two lemmas can be used directly by the solvers to get a proof for any location.