斷言上指針陣列

我已經定義下面的函數，其是公由郵資-C證明：斷言上指針陣列

//ensures array <= \result < array+length && *\result == element; 
/*@ 
    requires 0 < length; 
    requires \valid_read(array + (0 .. length-1)); 

    assigns \nothing; 

    behavior in: 
    assumes \exists int off ; 0 <= off < length && array[off] == element; 
    ensures *\result == element; 

    behavior notin: 
    assumes \forall int off ; 0 <= off < length ==> array[off] != element; 
    ensures \result == 0; 

    disjoint behaviors; 
    complete behaviors; 
*/ 
int* search(int* array, int length, int element){ 
    int *tmp; 
    /*@ 
    loop invariant 0 <= i <= length; 
    loop invariant \forall int j; 0 <= j < i ==> array[j] != element; 
    loop assigns i; 
    loop variant length-i; 
    */ 
    for(int i = 0; i < length; i++) 
    { 
    if(array[i] == element) 
    { 
     tmp = &array[i]; 
     //@ assert *tmp==element; 
    } 
    else 
    { 
     tmp = 0;  
    } 
    } 
    return tmp; 
}

我用它在以下主要條目：

int main(){ 
    int arr[5]={1,2,3,4,5}; 
    int *p_arr; 

    p_arr = search(arr,5,4); 
    //@ assert *p_arr==30; 

    return 0 
}

我想知道爲什麼frama-c給出斷言「// @ assert * p_arr == 30;」真的，我不明白。

感謝

來源

2017-09-06 Laurent Guillaume

哪個版本的frama-c？哪些選項？誰說斷言是有效的：WP？ – Anne

謝謝您的回覆，版本爲磷，選項爲：frama-c-gui -wp -rte -val ，GUI上的子彈爲橙色。這對你來說有足夠的信息嗎？ –

我會說斷言線上的子彈是綠色的，對不起 –

只使用命令行，我看到在你的代碼的一些問題：

tmp缺少的循環分配;
您需要：
- 無論是在seach功能的then分支中加入一個break（那麼你將返回指針相匹配的第一個元素）
- 或在的開始初始化tmp = 0函數並刪除循環中的else分支（然後您將返回最後一次出現的指針）。

我沒有嘗試的圖形用戶界面，但它似乎很奇怪，你說你的例子是：

通過郵資-C很好的驗證

我建議你使用命令行來開始。

來源

2017-09-07 09:43:47 Anne

謝謝你，同時我得到了和你相同的結論！問題是我在代碼的其他地方定義了一些令WP混淆的錯誤公理，所以一切都被定義爲有效。所以現在我要糾正你的建議中的代碼並再次嘗試，非常感謝你的支持，我會在這裏發佈最終結果。 –

如果你確定，你可以考慮接受我的答案。謝謝。 – Anne

好了，現在我糾正我的代碼如下：

//ensures array <= \result < array+length && *\result == element; 
/*@ 
    requires 0 < length; 
    requires \valid_read(array + (0 .. length-1)); 

    assigns \nothing; 

    behavior in: 
    assumes \exists int off ; 0 <= off < length && array[off] == element; 
    ensures *\result == element; 

    behavior notin: 
    assumes \forall int off ; 0 <= off < length ==> array[off] != element; 
    ensures \result == 0; 

    disjoint behaviors; 
    complete behaviors; 
*/ 
int* search(int* array, int length, int element){ 

    /*@ 
    loop invariant 0 <= i <= length; 
    loop invariant \forall int j; 0 <= j < i ==> array[j] != element; 
    loop assigns i; 
    loop variant length-i; 
    */ 
    for(int i = 0; i < length ; i++) 
    { 
    if(array[i] == element) 
    { 
     return &array[i]; 
    } 
    } 
    return 0; 
}

，並添加以下斷言：

int main() 
{ 
    int arr[5] = {1,2,3,4,5}; 
    int *ptr; 

    ptr = search(arr,5,3); 
    //@ assert *ptr==3; 

}

然後運行：郵資-C -wp -rte myfile.c文件，並得到了結果：

[wp] Proved goals: 65/65 
    Qed:   35 (1.00ms-6ms-24ms) 
    Alt-Ergo:  30 (16ms-30ms-94ms) (132)

如果我把另一個斷言：

int main() 
    { 
     int arr[5] = {1,2,3,4,5}; 
     int *ptr; 

     ptr = search(arr,5,3); 
     //@ assert *ptr==5; 

    }

然後我得到的輸出：

[wp] [Alt-Ergo] Goal typed_main_assert_2 : Timeout (Qed:4ms) (10s) 
[wp] Proved goals: 64/65 
    Qed:   35 (1.00ms-4ms-10ms) 
    Alt-Ergo:  29 (16ms-28ms-109ms) (132) (interrupted: 1)

因此斷言是「未知」正如我們預期，如果我們運行郵資-C-GUI子彈爲橙色。

所以這工作正常，照顧錯誤的公理的東西！謝謝安妮的幫助。

來源

2017-09-07 12:51:00

斷言上指針陣列

回答

相關問題