if_succeeds {:msg "P0"} y == x + 1;
is the property. Note the semicolon at the end - it is required for all properties.if_succeeds
properties are usually specified before functions. They specify conditions that must hold if the function returns successfully. (if_succeeds
can also be specified on contracts. For more details on their semantics see this section).invariant
properties are specified only before contracts. They specify conditions that must hold whenever we are NOT executing code in the contract (more info in this section).if_updated
properties are specified only before state variables. They specify conditions that must be checked whenever we are updating the value of a state variable (or some of part of the state variable in the case of complex data structures such as arrays, structs and maps). More info in this section.assert
properties are specified before a statement in the body of the function. They specify a condition that must be checked inline before the target statement, and can refer to any local variable in scope for the target statement. For more details see this section.{:msg "message"}
. This is helpful when mapping the properties to their description in other documents, or just as a reminder about the intent of a complex property.{:msg "some message"}
you can also just write "some message" as shorthand. So for example the below is a valid annotation:#if_succeeds
annotation.inc
increments the value of the state variable x
by 1. The property x == old(x) + 1
captures exactly this behavior.x == old(x + 1)
since the value of the constant 1
doesn't change before and after the function.x >= 1
as shown below:P
and post-condition Q
as: P ==> Q
. So for example for the sillyDiv
function below, we can express a pre-condition (y != 0
) and post-condition (z == x/y
) as y!=0 ==> z == x/y
.y == 0
. We can make it complete by adding another property:if_succeeds
annotations for the same functions are conjoined together. The same holds for multiple invariant
annotations for a contract.