存在量化斷言失敗

Question

我想證明數組的量化斷言並遇到一些問題。請看下面的小程序：

int a[4] = {1,2,3,4}; 

/*@ requires p == a; 
    assigns \nothing; 
*/ 
void test(int *p) 
{ 
    p++; 
    //@ assert \forall int i; 0 <= i < 3 ==> p[i] < 10; 
    //@ assert \exists int i; p[i] == 3; 
} 

我使用的是 '類型化' 的內存模型：

郵資-C-GUI -wp -wp-QED -wp-byreference -wp模型 '類型化' - 主要測試Test.c

由於某些原因，「requires」不成立，因此所有斷言都可以證明，即使是1 == 2。爲了克服這一點，我直接分配函數體中的全局變量：

int a[4] = {1,2,3,4}; 

/*@ assigns \nothing; 
*/ 
void test(int *p) 
{ 
    p = a; 

    p++; 
    //@ assert \forall int i; 0 <= i < 3 ==> p[i] < 10; 
    //@ assert \exists int i; p[i] == 3; 
} 

這裏FORALL持有，但存在沒有。只有當我在它之前添加斷言「p [1] == 3」時，該存在才成立。什麼是缺少證明這種存在性數組屬性？我需要這個表達循環不變的數組條目的搜索循環。

謝謝，哈拉爾德

Answer 1

的「要求」是由一個不正確的簡化轉化成假。它將在下一個版本中得到糾正。感謝您發現錯誤。

隨着修復，最後的斷言仍然沒有被Alt-ergo證明，因爲它無法找到我使用其通常啓發式的見證。當你添加斷言「p [1] == 3」時，你給了證人，這就是證明更容易的原因。其他一些證明者（Z3，CVC4）將能夠直接證明這個特定的斷言。請繼續關注下一個版本。