Scribble
Search…
Language
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
1
/// #if_succeeds $result > 0;
2
function positiveNumber() external returns (uint) {
3
...
4
}
Copied!
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
1
contract Example {
2
// #if_updated msg.sender == owner || owner == address(0);
3
address owner;
4
}
Copied!
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
1
/// #invariant sum(balances) == totalSupply;
2
contract Token {
3
...
4
}
Copied!
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
1
/// #define add10(uint x) uint = x + 10;
2
contract Example {
3
/// #if_succeeds add10(1) == 11;
4
function example() public {}
5
}
Copied!
Read more about Scribble functions here:
Last modified 4mo ago