證明長度函數來計算字符數組元素數

Question

我試圖證明函數像C中的strlen，但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)。因此，您需要處理這種情況。

• stringlen（）中的while循環在遇到nul字節時終止。但是，elementNumber（）邏輯函數的定義僅取決於指針是否有效。

• 對於stringlen（），沒有關於s，s + 1等是否有效的先決條件。

• 您的elementNumber（）邏輯函數未定義無效指針的值。

• 您將需要指定循環不變量。

---

我建議採取看看如何郵資-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定義分發，截至撰寫本文時爲Sodium-20150201。