Функция проверки длины для подсчета номера элемента массива символов

Question

Я пытаюсь доказать функцию типа strlen в C, но frama-c не доказывает состояние сообщения и предложение loop variant len. Я не понимаю, почему!

Что я пробовал:

/*@ 
    axiomatic elementNumber_axioms 
    { 
     logic unsigned elementNumber{L}(char *a); 

     axiom elementNumber_base{L}: 
      elementNumber(\null) == 0; 

     axiom elementNumber_step{L}: 
      \forall char *a; 
      \valid(a) ==> elementNumber(a) == elementNumber(a+1) + 1; 
    } 
*/ 

/*@ 
    assigns \nothing; 
    ensures \result == elementNumber(\old(s)); 
*/ 
unsigned stringlen(const char *s) 
{ 
    unsigned len = 0; 

/*@ 
    loop assigns len; 
    loop assigns s; 
    loop variant len; 
*/ 
    while(*s) 
    { 
     ++s; 
     ++len; 
    } 

    return len; 
} 

Что я делаю неправильно?

Answer 1

Существует несколько проблем с тем, что вы написали. Неполный список:

• Ваш StringLen() не обрабатывает случай, когда s является NULL.

  Если аннотировать стандартную функцию C strlen(), вам не нужно будет обрабатывать этот случай, потому что стандартная функция C strlen() не позволяет параметру быть NULL. Однако аксиоматическое определение вашей логической функции elementNumber() определяет elementNumber(\null) как 0, а постусловие stringlen() заключается в том, что результат равен elementNumber(s). Таким образом, вам нужно будет обработать этот случай.

• Цикл while в stringlen() завершается, когда встречается нулевой байт. Однако определение вашей логической функции elementNumber() зависит только от того, действителен ли указатель.

• Нет никаких предварительных условий для stringlen() относительно того, являются ли s, s + 1 и т. Д. Действительными.

• Логическая функция elementNumber() не определяет значение для недопустимого указателя.

• Вам нужно будет указать инварианты цикла.

---

Я рекомендую взглянуть на то, как Frama-C аннотирует StrLen():

/*@ requires valid_string_src: valid_string(s); 
    @ assigns \result \from s[0..]; 
    @ ensures \result == strlen(s); 
    @*/ 
extern size_t strlen (const char *s); 

В StrLen() логическая функция и valid_string() предикат определены в share/libc/__fc_string_axiomatic.h источника дистрибутив, который на момент написания этой статьи - натрий-20150201.