PreCondition or PostCondtion in ACSL

Question

I am not able to distinguish between various precondition and post-condition in ACSL. As I know that requires, terminates and assume comes in precondition and ensures and assigns in post-condition. But in which set rest like decrease etc are??

Can any body is able to help me in figuring out?? thanks in advance

Answer 1

This is a trick question. Basically, decreases would serve as a pre-condition of a recursive call: if you have a function f with decreases x;, if it happens to make a call to itself, you have to prove that x<\at(x,Pre) at this call site. Additionally, you have a pre-condition that x>=0 when you call f (recursive call or not). Regarding other clauses (based on their order of apperance in ACSL 1.7:

• complete and disjoint clause are basically a logical property of the assumes clause of the contract, they do not imply anything for the implementation, but act as a sanity check of the specification itself.
• allocates and frees are post-conditions (like for assigns but regarding dynamic allocation)
• exits (and returns, breaks and continues) are post-conditions (they are evaluated when we exit the function -or the statement).
• dependencies (\from) are post-conditions (like assigns).

Answer 2

decrease clause of ACSL is basically used for recursive function calls. if you have specified decrease clause with a pointer variable x like: decrease *x; then what it means is, every time when control enters the function related to this decrease clause, it checks whether the value pointed to by the pointer x is 1 less as compared to the value pointed to by x during the pre-state of the function. For the very first time when the function is called, pre-condition checked is: (*x) >= 0 as the function is in its pre-state so there is no pre-state value to compare to.