Annotations

Scribble annotations are at the of the Scribble. You can formalise properties by writing annotations for contracts, state variables and functions.

There are several different kinds of annotations at your disposal.

Function Annotations

Function annotations are what you can use to describe how a function should behave. You'll commonly use it to ensure that the function has the right side-effects, and that the return values are correct.

Example

/// #if_succeeds $result > 0;
function positiveNumber() external returns (uint) {
    ...
}

Read more about function annotations here:

State Variable Annotations

State variable annotations allow you to describe properties that should hold for a particular variable over time. For example, you might specify that a variable can only change under particular circumstances.

Example

contract Example {
    // #if_updated msg.sender == owner || owner == address(0);
    address owner;
}

Read more about state variable annotations here:

Contract Annotations

Contract annotations allow you to describe properties that concern multiple variables and functions. The most common contract annotation will be an invariant, which is used to describe properties that hold before and after each transaction.

Example

/// #invariant sum(balances) == totalSupply;
contract Token {
   ...
}

Read more about contract annotations here:

Scribble Functions

Scribble functions are a utility feature which enables you to reduce code duplication between annotations. They also make annotations much easier to read!

Example

/// #define add10(uint x) uint = x + 10;
contract Example {
    ///  #if_succeeds add10(1) == 11;
    function example() public {}
}

Read more about Scribble functions here:

​