Pre- and Post-Conditions

Pre-conditions and post-conditions are a unique and powerful feature of Cadence that allow you to specify conditions for execution that must be met for transactions and functions. If they're not met, execution stops and the transaction is reverted. One use is to define specific inputs and outputs for a transaction that make it easy to see what will be transferred, regardless of how complex the transaction execution becomes. This property is particularly useful in using code written by an AI.

To mock out an example:

Pre-condition: The user has 50 Flow.

Execution: Massively complex operation involving swaps between three different currencies, two dexes, and an NFT marketplace.

Post-condition: The user has at least 30 Flow remaining, and owns SuperCoolCollection NFT #54.

Function pre-conditions and post-conditions

Functions may have pre-conditions and may have post-conditions. They can be used to restrict the inputs (values for parameters) and output (return value) of a function.

Pre-conditions must be true right before the execution of the function. They are part of the function and introduced by the pre keyword, followed by the condition block.
Post-conditions must be true right after the execution of the function. Post-conditions are part of the function and introduced by the post keyword, followed by the condition block.
A conditions block consists of one or more conditions. Conditions are expressions evaluating to a boolean.
Conditions may be written on separate lines, or multiple conditions can be written on the same line, separated by a semicolon. This syntax follows the syntax for statements.
Following each condition, an optional description can be provided after a colon. The condition description is used as an error message when the condition fails.

In post-conditions, the special constant result refers to the result of the function:


_27fun factorial(_ n: Int): Int {
_27    pre {
_27        // Require the parameter `n` to be greater than or equal to zero.
_27        //
_27        n >= 0:
_27            "factorial is only defined for integers greater than or equal to zero"
_27    }
_27    post {
_27        // Ensure the result will be greater than or equal to 1.
_27        //
_27        result >= 1:
_27            "the result must be greater than or equal to 1"
_27    }
_27
_27    if n < 1 {
_27       return 1
_27    }
_27
_27    return n * factorial(n - 1)
_27}
_27
_27factorial(5)  // is `120`
_27
_27// Run-time error: The given argument does not satisfy
_27// the pre-condition `n >= 0` of the function, the program aborts.
_27//
_27factorial(-2)

In post-conditions, the special function before can be used to get the value of an expression just before the function is called:


_12var n = 0
_12
_12fun incrementN() {
_12    post {
_12        // Require the new value of `n` to be the old value of `n`, plus one.
_12        //
_12        n == before(n) + 1:
_12            "n must be incremented by 1"
_12    }
_12
_12    n = n + 1
_12}

Both pre-conditions and post-conditions are considered view contexts; any operations that are not legal in functions with view annotations are also not allowed in conditions. In particular, this means that if you wish to call a function in a condition, that function must be view.

Transaction pre-conditions

Transaction pre-conditions function in the same way as pre-conditions of functions.

Pre-conditions are optional and are declared in a pre block. They are executed after the prepare phase, and are used for checking if explicit conditions hold before executing the remainder of the transaction. The block can have zero or more conditions.

For example, a pre-condition might check the balance before transferring tokens between accounts:


_10pre {
_10    sendingAccount.balance > 0
_10}

If any of the pre-conditions fail, then the remainder of the transaction is not executed and it is completely reverted.

Transaction post-conditions

Transaction post-conditions are just like post-conditions of functions.

Post-conditions are optional and are declared in a post block. They are executed after the execution phase, and are used to verify that the transaction logic has been executed properly. The block can have zero or more conditions.

For example, a token transfer transaction can ensure that the final balance has a certain value:


_10post {
_10    signer.balance == 30.0: "Balance after transaction is incorrect!"
_10}

If any of the post-conditions fail, then the transaction fails and is completely reverted.