존재 한정된 어설 션이 실패했습니다.

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; 
} 

:

FRAMA-C-GUI를 -wp -wp-QED -wp-byreference -wp 모델 '형식화'- main test Test.c

"요구"는 유지되지 않으므로 모든 주장이 입증 될 수 있습니다. 1 == 2조차도. (가)하지 않는 존재하지만, FORALL 보유 여기

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; 
} 

:이 문제를 극복하기 위해 내가 직접 함수 본문에서 전역 변수를 할당합니다. 존재는 어설 션 "p [1] == 3"을 추가 할 때만 유지됩니다. 그러한 실존 배열 속성을 증명하기 위해 누락 된 것은 무엇입니까? 배열 항목에 대한 검색 루프에 대한 루프 불변 식을 표현할 때이 함수가 필요합니다.

감사합니다, 하 랄드

Answer 1

는 "필요"잘못된 단순화으로 false로 변환됩니다. 다음 릴리스에서 수정 될 것입니다. 오류를 발견해 주셔서 감사합니다.

이 수정 사항을 사용하면 Alt-ergo에서 마지막 어설 션을 증명할 수 없습니다. 일반적인 어설 션을 사용하여 i의 증인을 찾을 수 없기 때문입니다. "p [1] == 3"이라는 어설 션을 추가하면 증인이되므로 증명하기가 쉽습니다. 일부 다른 프로 버 (Z3, CVC4)는이 특정 어설 션을 직접 증명할 수 있습니다. 다음 출시를 위해 계속 지켜봐주십시오.