Pre- and Post-Conditions
Pre-conditions
Transaction pre-conditions are just like 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.
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.
Using pre-conditions and post-conditions
Another function of the pre-conditions and post-conditions is to describe the effects of a transaction on the involved accounts. They are essential for users to verify what a transaction does before submitting it. The conditions are an easy way to introspect transactions before they are executed.
For example, the software that a user uses to sign and send a transaction could analyze and interpret the transaction into a human-readable description, such as "This transaction will transfer 30 tokens from A to B. The balance of A will decrease by 30 tokens and the balance of B will increase by 30 tokens."
Function pre-conditions and post-conditions
Functions may have pre-conditions and may have post-conditions. Pre-conditions and post-conditions 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. Pre-conditions 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. Post-conditions may only occur after pre-conditions, if any.
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.
Interface declaration
Interfaces are declared using the struct, resource, or contract keyword, followed by the interface keyword, the name of the interface, and the requirements, which must be enclosed in opening and closing braces.
Field requirements can be annotated to require the implementation to be a variable field, by using the var keyword; to require the implementation to be a constant field, use the let keyword; or, the field requirement may specify nothing, in which case the implementation may either be a variable or a constant field.
Field requirements and function requirements must specify the required level of access. The access must be at least public, so the access(all) keyword must be provided.
Interfaces can be used in types. This is explained in detail in the Interfaces in types section. For now, the syntax {I} can be read as the type of any value that implements the interface I:
_81// Declare a resource interface for a fungible token._81// Only resources can implement this resource interface._81//_81access(all)_81resource interface FungibleToken {_81_81 // Require the implementing type to provide a field for the balance_81 // that is readable in all scopes (`access(all)`)._81 //_81 // Neither the `var` keyword, nor the `let` keyword is used,_81 // so the field may be implemented as either a variable_81 // or as a constant field._81 //_81 access(all)_81 balance: Int_81_81 // Require the implementing type to provide an initializer that_81 // given the initial balance, must initialize the balance field._81 //_81 init(balance: Int) {_81 pre {_81 balance >= 0:_81 "Balances are always non-negative"_81 }_81 post {_81 self.balance == balance:_81 "the balance must be initialized to the initial balance"_81 }_81_81 // NOTE: The declaration contains no implementation code._81 }_81_81 // Require the implementing type to provide a function that is_81 // callable in all scopes, which withdraws an amount from_81 // this fungible token and returns the withdrawn amount as_81 // a new fungible token._81 //_81 // The given amount must be positive and the function implementation_81 // must add the amount to the balance._81 //_81 // The function must return a new fungible token._81 // The type `{FungibleToken}` is the type of any resource_81 // that implements the resource interface `FungibleToken`._81 //_81 access(all)_81 fun withdraw(amount: Int): @{FungibleToken} {_81 pre {_81 amount > 0:_81 "the amount must be positive"_81 amount <= self.balance:_81 "insufficient funds: the amount must be smaller or equal to the balance"_81 }_81 post {_81 self.balance == before(self.balance) - amount:_81 "the amount must be deducted from the balance"_81 }_81_81 // NOTE: The declaration contains no implementation code._81 }_81_81 // Require the implementing type to provide a function that is_81 // callable in all scopes, which deposits a fungible token_81 // into this fungible token._81 //_81 // No pre-condition is required to check the given token's balance_81 // is positive, as this condition is already ensured by_81 // the field requirement._81 //_81 // The parameter type `{FungibleToken}` is the type of any resource_81 // that implements the resource interface `FungibleToken`._81 //_81 access(all)_81 fun deposit(_ token: @{FungibleToken}) {_81 post {_81 self.balance == before(self.balance) + token.balance:_81 "the amount must be added to the balance"_81 }_81_81 // NOTE: The declaration contains no implementation code._81 }_81}
The required initializer and functions do not have any executable code.
Struct and resource interfaces can only be declared directly inside contracts (i.e., not inside of functions). Contract interfaces can only be declared globally and not inside contracts.
See Interfaces for more information.