1

我对最后一个 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);  

} */

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

非常感谢您的回答。

此致，

尼莱克斯。

4

1 回答 1

2

关于 ACSL 手册，您所写的内容是正确的。但是，正如您在 ACSL实施手册 ( http://frama-c.com/download/frama-c-acsl-implementation.pdf ) 中看到的那样，在 Frama-C 中当前的 ACSL 实施中不支持对。事实上，在 ACSL 的这个领域中，唯一部分支持的是 sum 类型。更准确地说，您可以定义 sum 类型，但\matchFrama-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;
 */
于 2014-06-23T07:02:26.440 回答