if_succeeds. Using if_succeeds, annotations you can assert properties that you expect to hold if (and only if) the annotated function successfully terminates.
if_succeedsallows you to write postconditions (i.e. properties over the state after the function is done).
amountis not zero.
scribblechecks the conjunction of all function annotations.
if_succeedsannotation at the contract level. A contract-level
if_succeedsis automatically applied to all public and external functions in the annotated contract, and all inheriting contracts. For example, in the below sample the annotation
x > 0will be applied to the functions
B.pubFunB. Note that
viewfunctions are skipped. So in the below example
A.pubViewFunwill not be annotated.
if_succeedsfunction you can only talk about the contract's state vars, and other global transaction state. You cannot refer to function arguments/returns (even if all functions in the contract have the same arguments or returns).