ACSL/Frama-C中使用reals的类型声明

Question

我对上一个Frama版本的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);  

} */ 

有人看到错误在哪里了吗？我发现ACSL文档对类型声明非常模糊..。

非常感谢你的回答。

诚挚的问候,

尼莱克斯。

Answer 1

你所写的对ACSL手册是正确的。但是，正如您在ACSL Implementation手册(http://frama-c.com/download/frama-c-acsl-implementation.pdf)中所看到的那样，在Frama中ACSL的当前实现中不支持对。事实上，在ACSL的这个区域中唯一部分支持的是sum类型。更准确地说，您可以定义和类型，但是Frama不支持\match构造，这意味着您必须求助于公理。在目前的情况下，以下内容应被Frama所接受(尽管没有测试)：

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