Проверка линейного поиска с помощью Frama-C

Question

Я еще раз озадачен простым проверочным упражнением, на этот раз в Frama-C (Sodium), используя плагин WP, так как я не мог заставить Джесси работать на универе рабочие станции (в процессе установки администратором/командой). Я читал «ACSL на примере» и руководство. Хотя я бы подумал, что этот пример достаточно прост, чтобы быстро справиться. После использования Dafny и Whiley для проверки того же алгоритма, возможно, я немного испортился.

#include <stdio.h> 
// A linear search over a sorted array looking for a given element. 

/*@ requires len > 0; 
    @ requires \valid(ls+ (0..(len - 1))); 
    @ requires \forall size_t k; 0 <= k < (len - 1) ==> ls[k] <= ls[k + 1]; 
    @ assigns \nothing; 
    @ behavior found: 
    @ assumes \exists size_t k; 0 <= k < len && ls[k] == item; 
    @ ensures \result >= 0; 
    @ behavior nfound: 
    @ assumes \forall size_t k; 0 <= k < len ==> ls[k] != item; 
    @ ensures \result == -1; 
    @ complete behaviors found, nfound; 
    @ disjoint behaviors found, nfound; 
    */ 
int search(int ls[], const size_t len, int item) 
{ 
    size_t i = 0; 

    /*@ loop invariant 0 <= i <= len; 
    @ loop invariant \forall size_t k; 0 <= k < i ==> ls[k] != item; 
    @ loop assigns i; 
    @ loop variant len - i; 
    */ 
    while (i < len) 
    { 
    if (ls[i] == item) 
     return i; 
    ++i; 
    } 
    return -1; 
} 

int main() 
{ 
    int src[] = { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 }; 
    if (search(src, 10, 5) >= 0) printf("found item"); 
    else printf("no item found"); 
} 

и выход я получаю при попытке проверить это:

$ frama-c -pp-annot -wp -wp-rte -wp-timeout 100 search.c  
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) 
[kernel] Parsing search.c (with preprocessing) 
/tmp/ppannot97a491.c:1:0: warning: "__STDC_VERSION__" redefined 
#define __STDC_VERSION__ 201112L 
^ 
<built-in>: note: this is the location of the previous definition 
/tmp/ppannot97a491.c:2:0: warning: "__STDC_UTF_16__" redefined 
#define __STDC_UTF_16__ 1 
^ 
<built-in>: note: this is the location of the previous definition 
/tmp/ppannot97a491.c:3:0: warning: "__STDC_UTF_32__" redefined 
#define __STDC_UTF_32__ 1 
^ 
<built-in>: note: this is the location of the previous definition 
[wp] Running WP plugin... 
[wp] Collecting axiomatic usage 
[rte] annotating function main 
[rte] annotating function search 
[wp] 20 goals scheduled 
[wp] [Qed] Goal typed_main_call_search_pre : Valid 
[wp] [Qed] Goal typed_main_call_search_pre_2 : Valid 
[wp] [Alt-Ergo] Goal typed_search_complete_found_nfound : Valid (10ms) (19) 
[wp] [Alt-Ergo] Goal typed_search_loop_inv_preserved : Valid (17ms) (21) 
[wp] [Alt-Ergo] Goal typed_search_disjoint_found_nfound : Valid (13ms) (19) 
[wp] [Qed] Goal typed_search_loop_inv_established : Valid 
[wp] [Qed] Goal typed_search_loop_inv_2_established : Valid 
[wp] [Alt-Ergo] Goal typed_main_call_search_pre_3 : Valid (383ms) (93) 
[wp] [Alt-Ergo] Goal typed_search_loop_inv_2_preserved : Valid (17ms) (33) 
[wp] [Qed] Goal typed_search_loop_assign : Valid 
[wp] [Alt-Ergo] Goal typed_search_assert_rte_mem_access : Valid (50ms) (89) 
[wp] [Alt-Ergo] Goal typed_search_assert_rte_unsigned_overflow : Valid (13ms) (30) 
[wp] [Qed] Goal typed_search_assign_part1 : Valid 
[wp] [Qed] Goal typed_search_assign_part2 : Valid 
[wp] [Qed] Goal typed_search_assign_part3 : Valid 
[wp] [Qed] Goal typed_search_assign_part4 : Valid 
[wp] [Qed] Goal typed_search_loop_term_decrease : Valid (3ms) 
[wp] [Qed] Goal typed_search_loop_term_positive : Valid 
[wp] [Alt-Ergo] Goal typed_search_nfound_post : Valid (17ms) (33) 
[wp] [Alt-Ergo] Goal typed_search_found_post : Unknown (54.3s) 
[wp] Proved goals: 19/20 
    Qed:   11 (3ms-3ms) 
    Alt-Ergo:  8 (10ms-383ms) (93) (unknown: 1) 

Answer 1

Это озадачило меня на некоторое время, но после того, как попытка доказательства Coq, я понял, что причина, почему ты не может доказать, что поведение found просто так ... это не правильно. А именно, для len > INT_MAX и item, который не найден в INT_MAX первых ячейках массива, но появляется где-то позже, результат в виде int будет отрицательным.

Ну, технически, это реализация определяется, как указано в C99, 6.3.1.3§3:

В противном случае новый тип подписан и значение не может быть представлено в его; либо результат определяется реализацией, либо генерируется сигнал, определяемый реализацией .

Если добавить опцию -warn-signed-downcast в командной строке, вы увидите новый RTE-генерируемый утверждение, которое не доказано:

 /*@ assert rte: signed_downcast: i ≤ 2147483647; */ 

Тогда пост-состояние found поведения становится доказано, при условии, что это утверждение имеет место.