frama-c - ACSL の PreCondition または PostCondtion

Question

ACSL では、さまざまな前提条件と事後条件を区別できません。私が知っているように、require、terminate、および想定は前提条件であり、post-condition で保証および割り当てます。しかし、減少などの休憩はどのセットにありますか??

理解するのを手伝ってくれる体はありますか?? 前もって感謝します

Answer 1

これはひっかけ問題です。基本的に、decreasesは再帰呼び出しの前提条件として機能します。 を使用する関数fがある場合、それ自体を呼び出す場合は、この呼び出しサイトでdecreases x;それを証明する必要があります。さらに、呼び出すときx<\at(x,Pre)の前提条件があります(再帰呼び出しかどうか)。その他の節について ( ACSL 1.7での出現順序に基づく:x>=0f

• completeanddisjoint節は、基本的に契約の節の論理プロパティでありassumes、実装に対して何も意味しませんが、仕様自体の健全性チェックとして機能します。
• allocatesおよびfrees事後条件です（assigns動的割り当てに関するものと同様）
• exits(and returns、breaksand continues) は事後条件です (関数またはステートメントを終了するときに評価されます)。
• 依存関係 ( \from) は事後条件 ( などassigns) です。