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
anddisjoint
clause are basically a logical property of theassumes
clause of the contract, they do not imply anything for the implementation, but act as a sanity check of the specification itself.allocates
andfrees
are post-conditions (like forassigns
but regarding dynamic allocation)exits
(andreturns
,breaks
andcontinues
) are post-conditions (they are evaluated when we exit the function -or the statement).- dependencies (
\from
) are post-conditions (likeassigns
).