瞭解如何正確使用post-condition和loop-invariant與Frama-c

Question

我試圖在此示例中證明返回值將爲0（如果8不在數組中）或1（如果在數組中爲8 ）。

---

int fi8(int *array, int size) { 
    int fi8 = 0; 
    int i = 0; 
    for(i = 0; i < length; ++i) 
    { 
    if(array[i] == 8) 
    fi8 = 1; 
    } 
    return fi8; 
} 

我開了前置和後置條件：

/*@ requires 0 <= size <= 100; 
@ requires \valid(array+(0..size-1)); 
@ assigns \nothing; 
@ ensures (\forall integer i; 0<= i < size && array[i] != 8) ==> (\result == 0); 
@ ensures (\exists integer i; (0<= i < size && array[i] == 8)) && (\result == 1); 
@*/ 

和循環不變，因爲郵資-C是基於霍爾邏輯：

/*@ loop invariant 0 <= i <= length; 
    @ loop invariant fi8 == 0 || fi8 == 1; 
    @ loop invariant (\forall integer i; 0<= i < size && array[i] != 8) 
     ==> (fi8 == 0); 
    @ loop invariant (\exists integer i; (0<= i < size && array[i] == 8)) 
     && (fi8 == 1); 
    @ loop assigns i, fi8; 
    @*/ 

我相當肯定，我錯過了一些線路上，我試圖使用所有 和存在。 我花了數小時試圖理解，如何正確檢查，如果任何值分配給數組或不，但我覺得我卡在這裏。 我真的很感謝你的幫助:)

Answer 1

你的代碼有幾個問題。首先，你似乎混合了size和length。我冒昧地在各處使用size，否則這個代碼甚至不會被C編譯器接受，更不用說Frama-C。其次，\forall integer i; 0<= i < size && array[i] != 8（和相應的循環不變量）不正確。從字面上看，這意味着任何整數i驗證既即i是0和和array[i]之間size不是8。以101爲i給出了這個命題的一個微不足道的例子。你想表達的是什麼，對於任何整數i，如果i是0和size之間，然後array[i]不8，其表示爲\forall integer i; 0<= i < size ==> array[i] != 8。另一方面，當在\exists下使用時，&&連接器是正確的：這次我們確實想要找到i，使得i在該數組的範圍內，並且爲array[i]==8。然而，在你上確保了第二&&是不正確的：你想說那是什麼如果有這樣的i，然後\result == 1，因此你必須在這裏的含義：(\exists integer i; 0<= i < size && array[i] == 8) ==> (fi8 == 1)

的最後一個問題是你的循環不變量。你已經重新用作量化變量，而它已經是一個C變量，這通常不是一個好主意。事實上，這是一個真正的問題，因爲你想表達的屬性，只要我們還沒有看到0和i，fi8==0（和雙重如果如果看到一個8，fi8==1），i作爲之間的8 C變量。如果您在量化中使用j，如

​​

所有證明義務已解除。