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) {
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.
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.
Scribble functions are a utility feature which enables you to reduce code duplication between annotations. They also make annotations much easier to read!