无法证明 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;
}

但是post条件无法自动证明（循环不变量证明很好）：

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

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

我用SMT2格式重写了目标，Alt-Ergo 2.2、CVC4 1.5和Z3 4.6.0的none可以证明：

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

如果你像这样改变你的post条件，Alt-Ergo

证明了这一点

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

Answer 2

如 , 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 所示以获取更多信息），或使用 coq（双击 GUI 的 WP 目标选项卡的相应单元格以在相应目标上启动 coqide）。

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

/*@

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

而 post 条件只需要用适当的参数实例化引理。

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

Cannot prove euclidean division in frama-c

frama-c

alt-ergo