Невозможно доказать евклидово деление в 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

Как указывается в ответе Мохамеда Игуернлала, автоматизированные испытатели не очень удобны с нелинейной арифметикой. Интерактивные доказательства можно сделать с помощью WP, либо непосредственно в графическом интерфейсе (для получения дополнительной информации см. Раздел 2.3 Руководства WP), либо с помощью команды coq (дважды щелкните соответствующую ячейку на вкладке WP Goals в графическом интерфейсе пользователя для запуска команды на соответствующая цель).

Обычно лучше использовать coq в леммах ACSL, поскольку вы можете сосредоточиться на точной формуле, которую вы хотите доказать вручную, не беспокоясь о логической модели кода, который вы пытаетесь доказать. Используя эту тактику, я смог доказать ваше постусловие со следующей промежуточной леммой:

/*@

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