💡 We discuss this example in greater detail below
if_updated
specification 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 declarationsOwnable
contract below:The value ofowner
may only be set at contract creation, OR changed by the current owner by callingtransfer
Ownable
. You can do this by adding an if_succeeds
annotation 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 onlyOwner
and then restore it before returning.owner
is modified, which is precisely what you can do with the new if_updated
annotation:if_updated
annotation appears right above the declaration of the owner
variable. This property will ensure that the condition following if_updated
will 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.sender
describes the case when we are in the constructor (in that case msg.sig == 0x0
), and states that in that case, after the assignment owner
must 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 owner
before the assignment c) The new value of owner
must be what was passed in to transferOwnership
(owner == newOwner
).owner
is modifiedif_updated
annotations appaer in docstrings right before a variable declarationif_updated
annotation you can use old()
to refer to the value of an expression before the assignment.delete
operations, unary increment/decrement operations (++
/--
), etc.arr
is aliased, and cannot be annotated: