這個問題中的示例似乎僅適用于固定長度的陣列，但是下面來自https://frama-c.com/html/acsl.html的類似代碼似乎沒有通過。一旦我將代碼更改為包含要求&& n == 42（或任何其他正整數），它就會通過。
當它失敗時，它說[wp] [Alt-Ergo 2.4.1] Goal typed_set_to_0_loop_invariant_established : Timeout (Qed:1ms) (1') (cached)
/*@
requires \valid(a (0..n-1));
assigns a[0..n-1];
ensures
\forall integer i;
0 <= i < n ==> a[i] == 0;
*/
void set_to_0(int* a, int n){
int i;
/*@
loop invariant 0 <= i <= n;
loop invariant
\forall integer j;
0 <= j < i ==> a[j] == 0;
loop assigns i, a[0..n-1];
loop variant n-i;
*/
for(i = 0; i < n; i)
a[i] = 0;
}
關于如何進行的任何提示/預期的行為/標志是什么？
uj5u.com熱心網友回復：
實際上，如果嚴格否定，loop invariant 0 <= i <= n則不正確。n回圈不變數必須在您第一次到達回圈時保持（這是“已建立”部分的含義，而不是“保留”部分，您必須在“保留”部分檢查它是否在任何回圈步驟結束時保持，假設它是true 在所述步驟的開頭），即使您根本沒有進入回圈（這顯然是 if 的情況n<0）。因此，您必須requires n >=0;在函式的合同中添加 a。
編輯
我忘了提到另一種解決方案當然是制作n和i unsigned（甚至更好地#include <stddef.h>使用和使用size_t）：這樣，您可以保證一個正數而無需撰寫額外的requires）
轉載請註明出處，本文鏈接：https://www.uj5u.com/qita/424456.html
上一篇：VBA：遍歷作業表和字典