Function Specifications

Function specifications are used to specify the behaviour of a single function.

Successful termination

Scribble currently has a single type of function specification, called if_succeeds. Using if_succeeds, annotations you can assert properties that you expect to hold if (and only if) the annotated function succesfully terminates.

These annotations have the following structure & are placed right above a function declaration:

if_succeeds {:msg "<Description of your property>"} <boolean scribble expression>;
Example 1
Example 1

The following is a simple example property, where we check that the function always returns 0.

contract ExampleContract {
/// if_succeeds {:msg "result is always zero"} result == 0;
function example() public returns (uint result) {
...
}
}

Encoding Pre- and Post- Conditions

Pre- and postconditions are frequently used concepts in verification languages.

  1. A precondition is what should be true before a function is executed.

  2. A postcondition is what should be true after a condition is done executing.

In it's simplest form if_succeedsallows you to write postconditions.

However, if_succeeds is quite versatile and you can use it to check preconditions as well. You'd do so by using the old() function.

Example 1
Example 2
Example 1

We expect that a selfdestruct function only succeeds if the transaction sender is the owner of the contract.

/// if_succeeds {:msg ""} old(msg.sender == owner);
function selfdestruct() public onlyOwner {}
Example 2

We expect that the following function will only succeed if the input variable amount is not zero.

/// if_succeeds {:msg "Amount is not zero"} old(amount) == 0;
function transfer(uint amount, addres receiver) public { ... }

We're using old( ... ) here to make sure that the property is checked with the value of amount at the beginning of the transaction. This is because the value of amount can change during the transaction!

Encoding conditional "behaviors"

Functions can have multiple behaviors depending on the inputs and contract state. Take the following example of a simple calculator function implementing multiplication and addition.

contract Calculator {
enum Op {
PLUS,
TIMES
}
‚Äč
function calc(Op operator, uint left, uint right) public returns (uint result) {
if (operator == Op.TIMES) {
return left * right;
}
if (operator == Op.PLUS) {
return left + right;
}
assert (false);
}
}

In this case, there are two distinct behaviors: multiplication and addition. Writing two separate postconditions wouldn't work, since scribble checks the conjunction of all function annotations.

/// if_succeeds {:msg "result is product of left and right"} result == left * right;
/// if_succeeds {:msg "result is sum of left and right"} result == left + right;
function calc(Op operator, uint left, uint right) public returns (uint result) { ... }

Luckily, you can use the implication operator here to describe the conditions under which each behavior holds:

/// if_succeeds {:msg "result of times operator is product of left and right"} operator == Op.TIMES ==> result == left * right;
/// if_succeeds {:msg "result of plus operator is sum of left and right"} operator == Op.PLUS ==> result == left + right;
function calc(Op operator, uint left, uint right) public returns (uint result) { ... }