💡 We discuss this example in greater detail below
if_updatedspecification enables properties that will be checked at any point where a variable is updated. These properties follow the following structure and are placed above state variable declarations
The value of
ownermay only be set at contract creation, OR changed by the current owner by calling
Ownable. You can do this by adding an
if_succeedsannotation on all functions OTHER than
transferOwnership. However, this is fragile; what if we miss one?
old()and don't (yet) support temporal predicates. Even if we specified this as a contract invariant, a function inside the contract can temporarily re-assign
onlyOwnerand then restore it before returning.
owneris modified, which is precisely what you can do with the new
if_updatedannotation appears right above the declaration of the
ownervariable. This property will ensure that the condition following
if_updatedwill be checked on every write to the owner variable. This condition has two clauses that describe the conditions where the owner variable is allowed to be updated.
msg.sig == 0x0 && owner == msg.senderdescribes the case when we are in the constructor (in that case
msg.sig == 0x0), and states that in that case, after the assignment
ownermust equal to the
msg.sender(i.e., the contract creator).
transferOwnership(which is specified by
msg.sig == <signature-of-transferOwnership>) b) The caller must be the current owner (
msg.sender == old(owner)). Note the use, of
old()to refer to the value of
ownerbefore the assignment c) The new value of
ownermust be what was passed in to
owner == newOwner).
if_updatedannotations are docstrings right before a variable declaration
if_updatedannotation you can use
old()to refer to the value of an expression before the assignment.
deleteoperations, unary increment/decrement operations (
arris aliased, and cannot be annotated: