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

Question

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

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

Что дает:

[kernel] user error: unexpected token '('

В конце концов, я хочу, чтобы иметь код рядом с:

/*@ axiomatic RealPairs { 

type real_pair = (real, real); 

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

} */ 

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

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

С уважением,

Nilexys.

Answer 1

Что вы написали правильно в отношении руководства 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; 
*/