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 のこの領域で部分的にサポートされているのは合計型だけです。より正確には、和の型を定義できますが、\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;
 */
于 2014-06-23T07:02:26.440 に答える