3

外部関数の動作、より正確にはそれらの終了を指定しようとしています。ACSLのドキュメントによると、\terminates p;プロパティでは、述語が保持されている場合pは関数が終了することが保証されていますが、保持されていない場合は何も指定されpていません。また、決して返されない関数は次のように指定できることも説明しています。

//@ ensures \false ; terminates \false ;

さらに、ACSLは\exits p;、突然終了した場合の事後条件を指定するプロパティを提供します。だから私は疑問に思っています：

//@ ensures \false ; exits \false; terminates \false ;

関数が常に無限ループになるように指定しますか？

さらに、仕様は何ですか：

//@ ensures p ; exits q; terminates \false ;

可能な無限ループに関する手段？

4

1 に答える 1

1

あなたの仕様は、関数が永遠にループしていると言うことができる最も近いものですが、それでも2つのコーナーケースが残っています:

  1. 実行時エラー: 他の場所で処理されているといつでも言えます ( WP+genassignsまたはValue)
  2. longjmp : 残念ながら現在、ACSL にはそのようなものを指定するものは何もありません。
于 2013-02-23T14:36:48.560 に答える