frama-c - 无法证明 frama-c 中的欧氏除法

Question

我想证明 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;
}

但是后置条件无法自动证明(循环不变量证明很好):

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).

它确实有欧几里德除法的所有假设，有谁知道为什么它不能得出结论？

Answer 1

如 Mohamed Iguernlala's answer 所示, 自动证明器不太适应非线性算法。可以使用 WP 直接在 GUI 中进行交互式证明(有关更多信息，请参见 section 2.3 of WP Manual)，或者使用 coq(双击 GUI 的 WP 目标选项卡的适当单元格以在相应的位置上启动 coqide目标)。

在 ACSL 引理上使用 coq 通常更好，因为您可以专注于您想要手动证明​​的确切公式，而不会被您试图证明的代码的逻辑模型所困扰。使用这种策略，我已经能够使用以下中间引理证明您的后置条件:

/*@

// WP's interactive prover select lemmas based on the predicate and
// function names which appear in it, but does not take arithmetic operators
// into account 😭. Hence the DIV definition.

logic integer DIV(integer a,integer b) = a / b ;

lemma div_rem:
  \forall integer a,b,q,r; a >=0 ==> 0 < b ==>  0 <= r < b ==>
  a == b*q+r ==> q == DIV(a, b);
*/

/*@
  requires a >= 0 && 0 < b;
  ensures \result == DIV(a, b);
*/
int euclid_div(const int a, const int b)
{
  int q = 0;
  int r = a;

  /*@
    loop invariant a == b*q+r;
    loop invariant r>=0;
    loop assigns q,r;
    loop variant r;
   */
  while (b <= r)
    {
      q++;
      r -= b;
    }
  /*@ assert 0<=r<b; */
  /*@ assert a == b*q+r; */
  return q;
}

更准确地说，引理本身用以下 Coq 脚本证明:

intros a b q prod Hb Ha Hle Hge.
unfold L_DIV.
generalize (Cdiv_cases a b).
intros Hcdiv; destruct Hcdiv.
clear H0.
rewrite H; auto with zarith.
clear H.

symmetry; apply (Zdiv_unique a b q (a-prod)); auto with zarith.
unfold prod; simpl.
assert (b*q = q*b); auto with zarith.

虽然后置条件只需要用适当的参数实例化引理。