Обеспечивает доказательство, даже если код неисправен?

Question

Далее, как подтверждаются постусловия для поведения neg_limit, когда соответствующий код C закомментирован?

Как и ожидалось, одно из арифметических переполнений Safety->check не доказуемо, но похоже, что neg_limit также должен быть недоказуемым.

Контекст: я использую Frama-C-Boron, Jessie и, через gWhy, Alt-Ergo, чтобы научиться писать спецификации и доказывать, что функции соответствуют им. Также приветствуются любые подсказки, RTFMing и т. Д., Касающиеся стратегий, инструментов и т. Д. До сих пор я читаю и руководство по внедрению ACSL 1.7 (которое является более новым, чем у Борана), и руководство Jessie & ref. руководство.

Спасибо!

/*@ behavior non_neg:
        assumes v >= 0;
        ensures \result == v;

    behavior neg_in_range:
        assumes INT32_MIN < v < 0;
        ensures \result == -v;

    behavior neg_limit:
        assumes v == INT32_MIN;
        ensures \result == INT32_MAX;

    disjoint behaviors;
    complete behaviors;
*/
int32_t my_abs32(int32_t v)
{
  if (v >= 0)
    return v;

  //if (v == INT32_MIN)
  //  return INT32_MAX;

  return -v;
}

Вот основная цель первого постусловия:

goal my_abs32_ensures_neg_limit_po_1:
  forall v_2:int32.
  (integer_of_int32(v_2) = ((-2147483647) - 1)) ->
  (integer_of_int32(v_2) >= 0) ->
  forall __retres:int32.
  (__retres = v_2) ->
  forall return:int32.
  (return = __retres) ->
  ("JC_13": (integer_of_int32(return) = 2147483647))

и для второго:

goal my_abs32_ensures_neg_limit_po_2:
  forall v_2:int32.
  (integer_of_int32(v_2) = ((-2147483647) - 1)) ->
  (integer_of_int32(v_2) < 0) ->
  forall result:int32.
  (integer_of_int32(result) = (-integer_of_int32(v_2))) ->
  forall __retres:int32.
  (__retres = result) ->
  forall return:int32.
  (return = __retres) ->
  ("JC_13": (integer_of_int32(return) = 2147483647))

Answer 1

Что касается документации, вы можете взглянуть на ACSL Fraunhofer FOKUS By Example: http://www.fokus.fraunhofer.de/de/quest/_download_quest/_projekte/acsl_by_example.pdf

Что касается вашего вопроса, я повторил ваш результат (кстати, вам не хватает #include <stdint.h>" в вашем коде) с Frama-C Fluorine, а Jessie + Alt-ergo все еще удается доказать постусловие. Но помните, что постусловие подтверждается гипотезой о том, что не возникает ошибок времени выполнения, что не относится к вашему коду, как показывает отказавший ПО безопасности.

А именно, второе постусловие содержит гипотезу (integer_of_int32(result) = (-integer_of_int32(v_2))) который можно переписать как (integer_of_int32(result) = 2147483648), Это противоречит аксиоме в прелюдии Джесси, которая говорит, чтоforall v:int32. integer_of_int32(v)<=2147483647,

Я предполагаю, что это еще раз подчеркивает, что вы не можете утверждать, что проверили аннотацию ACSL, пока некоторые обязательства по проверке остаются не проверенными, даже если они не вытекают непосредственно из этой аннотации.