if_succeeds. Using if_succeeds, annotations you can assert properties that you expect to hold if (and only if) the annotated function succesfully terminates.
if_succeedsallows you to write postconditions.
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
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).