如何在frama-c中調試ACSL？

Question

我在努力學習ACSL，但是試圖編寫一個完整的規範時磕磕絆絆。我的代碼

#include <stdint.h> 
#include <stddef.h> 

#define NUM_ELEMS (8) 

/*@ requires expected != test; 
    @ requires \let n = NUM_ELEMS; 
    @   \valid_read(expected + (0.. n-1)) && \valid_read(test + (0.. n-1)); 
    @ assigns \nothing; 
    @ behavior matches: 
    @ assumes \let n = NUM_ELEMS; 
    @   \forall integer i; 0 <= i < n ==> expected[i] == test[i]; 
    @ ensures \result == 1; 
    @ behavior not_matches: 
    @ assumes \let n = NUM_ELEMS; 
    @   \exists integer i; 0 <= i < n && expected[i] != test[i]; 
    @ ensures \result == 0; 
    @ complete behaviors; 
    @ disjoint behaviors; 
    @*/ 
int array_equals(const uint32_t expected[static NUM_ELEMS], const uint32_t test[static NUM_ELEMS]) { 
    for (size_t i = 0; i < NUM_ELEMS; i++) { 
    if (expected[i] != test[i]) { 
     return 0; 
    } 
    } 
    return 1; 
} 

我與運行

郵資-C -wp -wp即食test.c的

，我看到下面的日誌

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) 
[kernel] Parsing test.c (with preprocessing) 
[rte] annotating function array_equals 
test.c:22:[wp] warning: Missing assigns clause (assigns 'everything' instead) 
[wp] 9 goals scheduled 
[wp] [Alt-Ergo] Goal typed_array_equals_assign_part1 : Unknown (Qed:2ms) (67ms) 
[wp] [Alt-Ergo] Goal typed_array_equals_assert_rte_mem_access_2 : Unknown (Qed:2ms) (128ms) 
[wp] [Alt-Ergo] Goal typed_array_equals_assert_rte_mem_access : Unknown (Qed:2ms) (125ms) 
[wp] [Alt-Ergo] Goal typed_array_equals_matches_post : Unknown (Qed:10ms) (175ms) 
[wp] [Alt-Ergo] Goal typed_array_equals_not_matches_post : Unknown (Qed:7ms) (109ms) 
[wp] Proved goals: 4/9 
    Qed:    4 (0.56ms-4ms) 
    Alt-Ergo:  0 (unknown: 5) 

所以看起來好像我的兩種行爲和「分配\沒有」無法證明。那麼我怎麼從這裏開始呢？

編輯：所以我想通了問題。我沒有註釋我的循環：

/*@ loop invariant \let n = NUM_ELEMS; 0 <= i <= n; 
    @ loop invariant \forall integer k; 0 <= k < i ==> expected[k] == test[k]; 
    @ loop assigns i; 
    @ loop variant \let n = NUM_ELEMS; n-i; 
    @*/ 

我的更大的問題仍然是：什麼是調試問題的好方法？我通過更改和刪除代碼並查看證明/未證實的內容來解決此問題。

Answer 1

恐怕這個問題不能有明確的答案（說實話，我認爲投票結果是「太寬泛」）。這裏有一個但是一些指導原則，可能會幫助你在你的證明嘗試：

識別單個條款

ACSL規範正在迅速由許多條款（requires，ensures，loop invariant，assert，...）。能夠輕鬆區分它們是非常重要的。爲此，您有兩個主要成分：

1. 使用GUI。它可以更容易地看到哪些註釋被證明（綠色子彈），但是在假設其他未經證實的子句是真實的（綠色/黃色）或未證實的（黃色）的假設下更容易。
2. 爲您的子句命名：任何ACSL謂詞都可以附上一個名稱，其語法爲name: pred。當一個條款配備一個名稱時，WP將使用它來引用該條款。

秋後算賬

這是很容易錯過一個規範的一些非常重要的組成部分。這裏是一個快速檢查表：

1. 所有循環必須配備loop invariant和loop assigns
2. 所有功能通過分析下的一個叫做必須有一個合同（至少有一個assigns條款）
3. 如果loop assigns中提到的內存位置不是 對應的loop invariant的對象，那麼對於在該位置以外的位置存儲的值，您一無所知。這可能是一個問題。

調試個別條款

一旦你確信你有沒有錯過什麼明顯的，現在是時候 開始調查的具體條款。

1. 通常，（實現首次循環時，即真），而不是保留（停留跨環步驟的真）這是很容易驗證一個loop invariant建立 。如果無法建立loop invariant，則它可能是錯誤的，或者您忘記了某些requires來限制該函數的輸入（對於陣列上的算法，典型情況是loop invariant 0<=i<=n;，如果您不是requires n>=0;，則不能證明）
2. 類似地，assigns和loop assigns應該比實際的功能特性更容易驗證。只要他們沒有被證明，你應該專注於他們（一個常見的錯誤是忘記把 它的loop assigns，或提及，它分配a[i]而不是a[0..i]）循環的索引。 不要忘記assigns必須包括所有可能的任務，包括 在被調用者中完成的任務。
3. 不要猶豫，使用assert來檢查WP是否可以證明一個屬性在給定的點上有效。這將幫助您瞭解問題出現的位置。 [根據@DavidMENTRÉ的評論編輯]請注意，在這種情況下，您應該注意以下事實：初始證明義務可能成功，假設assert擁有而assert本身未經過驗證。在GUI中，這通過綠色/黃色子彈反映出來，當然還有一個黃色子彈在assert前面。在這種情況下，證明還沒有結束，你必須明白爲什麼斷言沒有被證明，可能使用與上面相同的策略，直到你明確地知道問題出在哪裏。