I'd like to prove this loop implementation of Euclidean division in Frama-C :
/*@
requires a >= 0 && 0 < b;
ensures \result == a / b;
*/
int euclid_div(const int a, const int b)
{
int q = 0;
int r = a;
/*@
loop invariant a == b*q+r && r>=0;
loop assigns q,r;
loop variant r;
*/
while (b <= r)
{
q++;
r -= b;
}
return q;
}
But the post condition fails to prove automatically (the loop invariant proved fine) :
Goal Post-condition:
Let x = r + (b * euclid_div_0).
Assume {
(* Pre-condition *)
Have: (0 < b) /\ (0 <= x).
(* Invariant *)
Have: 0 <= r.
(* Else *)
Have: r < b.
}
Prove: (x / b) = euclid_div_0.
--------------------------------------------------------------------------------
Prover Alt-Ergo: Unknown (250ms).
It does have all the hypotheses of Euclidean division, does anyone know why it cannot conclude ?
As indicated by Mohamed Iguernlala's answer, automated provers are not very comfortable with non-linear arithmetic. It is possible to do interactive proofs with WP, either directly within the GUI (see section 2.3 of WP Manual for more information), or by using coq (double click on the appropriate cell of the WP Goals tab of the GUI for launching coqide on the corresponding goal).
It is usually better to use coq on ACSL lemmas, as you can focus on the exact formula you want to prove manually, without being bothered by the logical model of the code you're trying to prove. Using this tactic, I've been able to prove your post-condition with the following intermediate lemma:
More precisely, the lemma itself is proved with the following Coq script:
While the post-condition only requires to instantiate the lemma with the appropriate arguments.