ACSL/Frama-C에서 reals를 사용하는 유형 선언

Question

마지막 Frama-C 버전에 대한 ACSL 사양과 관련된 몇 가지 문제가 있습니다.
나는 한쌍의 실수를 선언하기 위해 많은 노력을했지만 그 중 누구도 일하지 않았습니다. 제공

/*@ type real_pair = (real, real); */ 

: 여기 이 문제로 설명하는 작은 예입니다

이

/*@ axiomatic RealPairs { 

type real_pair = (real, real); 

logic real Norm (real_pair p) = 
\let (x,y) = p; 
\sqrt(x*x + y*y); 

} */ 

사람이 볼 수 있습니까 :

[kernel] user error: unexpected token '('

을 말에, 나는 근처에 코드를 갖고 싶어 어디서 오류가 발생 했습니까? 형식 선언에 ACSL 문서가 매우 모호하다는 것을 알았습니다 ...

대단히 고맙습니다.

Nilexys.

Answer 1

ACSL 설명서와 관련하여 작성한 내용이 정확합니다. 그러나 ACSL 구현 설명서 (http://frama-c.com/download/frama-c-acsl-implementation.pdf)에서 볼 수 있듯이 Frama-C의 ACSL의 현재 구현에서는 쌍을 지원하지 않습니다. 실제로이 ACSL 영역에서 부분적으로 지원되는 것은 합계 유형뿐입니다. 더 정확하게는 합계 유형을 정의 할 수 있지만 \match 구조는 Frama-C에서 지원하지 않으므로 공리에 의지해야합니다. 현재 상황에서는 다음을 Frama-C에서 받아 들여야합니다 (테스트하지는 않음) :