Объявление типа с использованием вещественных чисел в ACSL/Frama-C

У меня есть некоторые проблемы со спецификацией ACSL для последней версии Frama-C.
Я много раз пытался объявить пару вещественных чисел, но ни один из них не работал. Вот крошечный пример, иллюстрирующий проблему:

/*@ 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);  

} */

Кто-нибудь видит, где ошибка? Я нашел документацию ACSL очень расплывчатой ​​в объявлениях типов...

Большое спасибо за ваши ответы.

С наилучшими пожеланиями,

Нилексис.


c frama-c
person Nilexys    schedule 20.06.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

То, что вы написали, верно в отношении руководства ACSL. Однако, как видно из руководства по реализации ACSL (http://frama-c.com/download/frama-c-acsl-implementation.pdf), пары не поддерживаются в текущей реализации ACSL в Frama-C. Фактически, единственное, что частично поддерживается в этой области ACSL, — это типы суммы. Точнее, можно определить типы сумм, но конструкция \match не поддерживается Frama-C, а значит, приходится прибегать к аксиоматике. В текущем состоянии Frama-C должен принять следующее (хотя и не тестировалось):

/*@ type real_pair = RPCons(real, real); */
/*@ axiomatic Real_pair {
     logic real rp_fst(real_pair p);
     logic real rp_snd(real_pair p);
     axiom rp_fst_def: \forall real x, y; rp_fst(RPCons(x,y)) == x;
     axiom rp_snd_def: \forall real x,y; rp_snd(RPCons(x,y)) == y;
 */
person Virgile    schedule 23.06.2014