할당 절 입증 할 수 없습니다 - FRAMA-C

내가 FRAMA-C에 새로 온 사람과 나는이 간단한 예제와 문제가 무엇인지 이해하고 싶습니다 :이 예에서할당 절 입증 할 수 없습니다 - FRAMA-C

/*@ requires \valid(array+(0..length-1)) 
@ ensures \forall integer k; 0 <= k < length ==> array[k] == 0; 
@ assigns array[0..length-1]; 
*/ 
void fill(int array[], int length){ 
    /*@ loop invariant 0 <= i <= length; 
    @ loop invariant \forall integer k; 0 <= k < i ==> array[k] == 0; 
    @ loop assigns i, array[0..i-1]; 
    @ loop variant length - i; 
    */ 
    for(int i = 0; i < length; i++){ 
     array[i] = 0; 
    } 
}

, FRAMA-C를 (WP + Value)는 함수 계약에서 assign 절을 증명할 수 없으며 이유를 이해할 수 없습니다. 어떤 도움을 주시면 감사하겠습니다 =)

출처

2013-05-23 roo

왜? 괜찮지 않니? 난 그냥 int 배열을 (정적으로 선언 된) 0으로 채우기 싶습니다 ... int * array [] int 포인터 배열이 아닙니다 ?? 어쨌든 트릭을하지 않습니다./ – roo

무슨 뜻인지 모르겠군요. 이 서명 채우기 (int * 배열, int 길이)를 사용하더라도 문제는 여전히 여기에 있습니다 ... – roo

@EliasVanOotegem C에서 배열은 참조로 전달됩니다. 기능이 좋으며 사양이 좋습니다. Value 플러그인은 정보 소스로서 "assigns"절만 사용하고 소스 코드가없는 라이브러리 함수에 대해서만 사용하는 것을 목표로하지 않으므로 "할당"을 증명하지 않습니다. 나는 WP가 그것을 증명할 것이라고 생각했다. Roo, 자동 프로 버는 무엇을 설치 했습니까? –

루프 할당을 약화 시키면 (alt-ergo 0.95.1로) 입증 될 수 있습니다.

@ 루프는 i, array [0..length-1]; 이 \valid(array+(0..length-1) 암시 하지 때문에

전제 조건 i >= 0도 필요하다. array+(0..length-1)은 유효한 위치 세트이지만 length <= 0입니다. 빈 장소는 있습니다.

원래 루프 지정이 귀하의 전제 조건을 의미하지 않는다는 사실은 WP 플러그인의 현재 버전에 대한 제한 사항임을 의미합니다.

출처

2013-05-24 09:24:08 byako

안녕하세요, Boris, 답변 해 주셔서 감사합니다. 나는 루프 지정을 약화시킴으로써 그것을 증명할 수 있다는 것을 알았지 만, 왜 그것이 더 강하고 정확한 절로 작동하지 않는지 알고 싶었다. 설명해 주셔서 감사합니다. – roo

Boris의 답변이 마음에 들면 승인 된 것으로 표시해야합니다 (투표 버튼 아래의 체크 표시). –

할당 절 입증 할 수 없습니다 - FRAMA-C

답변

관련 문제