c - 在 ACSL/Frama-C 中使用实数类型声明

Question

我对最新 Frama-C 版本的 ACSL 规范有一些疑问。
我尝试了很多方法来声明一对实数，但没有一个起作用。这是一个按问题说明的小例子:

/*@ 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 文档在类型声明上非常含糊...

非常感谢您的回答。

最好的问候，

尼勒克斯。

Answer 1

关于 ACSL 手册，您所写的内容是正确的。但是，正如您在 ACSL Implementation 手册中看到的那样( http://frama-c.com/download/frama-c-acsl-implementation.pdf )，当前 Frama-C 中的 ACSL 实现不支持对。事实上，在 ACSL 的这个领域中唯一受部分支持的是求和类型。更准确地说，您可以定义和类型，但 Frama-C 不支持 \match 构造，这意味着您必须求助于公理。在目前的情况下，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;
 */