无法证明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 目标选项卡的相应单元格以在相应的目标）。

通常最好在 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.

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

Answer 2

因为它是非线性算术，有时对于自动 (SMT) 求解器来说很难。

我用 SMT2 格式重写了目标，Alt-Ergo 2.2、CVC4 1.5 和 Z3 4.6.0 都无法证明：

(set-logic QF_NIA)

(declare-const i Int)
(declare-const i_1 Int)
(declare-const i_2 Int)

(assert (>= i_1 0))
(assert (>  i_2 0))
(assert (>=  i 0))
(assert (<  i i_2))

; proved by alt-ergo 2.2 and z3 4.6.0 if these two asserts are uncommented
;(assert (<= i_1 10))
;(assert (<= i_2 10))

(assert
 (not
  (= i_1
     (div
      (+ i (* i_1 i_2))
      i_2 )
     )
  )
 )

(check-sat)

如果你像这样改变你的后置条件，它是由 Alt-Ergo 证明的

ensures \exists int r ;
   a == b * \result + r && 0 <= r && r < b;