гарантирует, что код неисправен?

Question

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

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

Контекст: Я использую Frama-C-Boron, Jessie и через gWhy Alt-Ergo, чтобы научиться писать спецификации и доказывать, что функции встречаются с ними. Также приветствуются любые cluebatting, RTFMing и т. Д. О стратегиях разработки, инструментах и ​​т. Д. До сих пор я читаю как руководство по внедрению ACSL 1.7 (это последнее, что -Boron's), так и учебник 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; 
} 

Вот цель gWhy первый постусловии:

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

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

Что касается вашего вопроса, я повторил ваш результат (BTW, вам не хватает #include <stdint.h>" в вашем коде) с фтором Frama-C, а 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, если некоторые обязательства по доказательству остаются непроверенными, даже если они не вытекают непосредственно из этой аннотации.