Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Function Attributes

Ursus uses attributes to control function behavior, visibility, code generation, and verification. Attributes are specified using the #[...] syntax before function definitions.

Syntax

#[attribute1, attribute2, ...]
Ursus Definition functionName (args): UExpression RetType panicFlag.

Visibility Attributes

#[public]

Makes function callable from outside the contract.

Example:

#[public]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

Generated code:

function transfer(address to, uint256 amount) public returns (bool) {
    ...
}

#[external]

Function can only be called externally (not internally).

Example:

#[external]
Ursus Definition deposit: UExpression unit false.

Generated code:

function deposit() external {
    ...
}

#[internal]

Function can only be called internally.

Example:

#[internal]
Ursus Definition _validateAmount (amount: uint256): UExpression boolean false.

Generated code:

function _validateAmount(uint256 amount) internal returns (bool) {
    ...
}

#[private]

Function is private to the contract.

Example:

#[private]
Ursus Definition _calculateFee (amount: uint256): UExpression uint256 false.

Generated code:

function _calculateFee(uint256 amount) private returns (uint256) {
    ...
}

State Mutability Attributes

#[pure]

Function doesn't read or modify state.

Example:

#[pure]
Ursus Definition add (a b: uint256): UExpression uint256 false.
{
    ::// _result := a + b |.
}
return.
Defined.

Generated code:

function add(uint256 a, uint256 b) public pure returns (uint256) {
    return a + b;
}

#[view]

Function reads but doesn't modify state.

Example:

#[view]
Ursus Definition balanceOf (account: address): UExpression uint256 false.
{
    ::// _result := balances[[account]] |.
}
return.
Defined.

Generated code:

function balanceOf(address account) public view returns (uint256) {
    return balances[account];
}

#[payable]

Function can receive Ether/tokens.

Example:

#[payable]
Ursus Definition deposit: UExpression unit false.
{
    ::// balance := balance + msg->value |.
}
return.
Defined.

Generated code:

function deposit() public payable {
    balance += msg.value;
}

#[nonpayable]

Function cannot receive Ether/tokens (default).

Example:

#[nonpayable]
Ursus Definition withdraw (amount: uint256): UExpression unit false.

Code Generation Attributes

#[translation = on]

Enable code generation for this function.

Example:

#[translation = on]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

#[translation = off]

Disable code generation (proof-only function).

Example:

#[translation = off]
Ursus Definition helper_lemma: UExpression unit false.

#[language = solidity]

Generate Solidity code.

Example:

#[language = solidity]
Contract ERC20 ;

#[language = cpp]

Generate C++ code for TON.

Example:

#[language = cpp]
Contract TONToken ;

#[language = rust]

Generate Rust code.

Example:

#[language = rust]
Contract RustToken ;

Return Value Attributes

#[returns = varName]

Use named return variable.

Example:

#[returns = result]
Ursus Definition calculate (x: uint256): UExpression uint256 false.
{
    ::// result := x * {2} |.
}
return.
Defined.

Generated code:

function calculate(uint256 x) public returns (uint256 result) {
    result = x * 2;
}

Parameter Attributes

#[write = arg]

Parameter is mutable (passed by reference).

Example:

#[write = balance]
Ursus Definition updateBalance (balance: uint256) (delta: uint256):
  UExpression unit false.
{
    ::// balance := balance + delta |.
}
return.
Defined.

Interface Attributes

#[no_body]

Function declaration without implementation (interface).

Example:

#[no_body]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

Generated code:

function transfer(address to, uint256 amount) external returns (bool);

Inheritance Attributes

#[override]

Function overrides parent implementation.

Example:

#[override]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

Generated code:

function transfer(address to, uint256 amount) public override returns (bool) {
    ...
}

#[virtual]

Function can be overridden by children.

Example:

#[virtual]
Ursus Definition _beforeTransfer (from to: address) (amount: uint256):
  UExpression unit false.

Generated code:

function _beforeTransfer(address from, address to, uint256 amount)
    internal virtual {
    ...
}

Verification Attributes

#[quickchick = on]

Enable QuickChick testing for this function.

Example:

#[quickchick = on]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

#[verified]

Mark function as formally verified.

Example:

#[verified]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

Combining Attributes

Multiple attributes can be combined:

Example:

#[public, view, translation = on]
Ursus Definition balanceOf (account: address): UExpression uint256 false.
{
    ::// _result := balances[[account]] |.
}
return.
Defined.

Generated code:

function balanceOf(address account) public view returns (uint256) {
    return balances[account];
}

Common Attribute Combinations

Public View Function

#[public, view]
Ursus Definition getBalance: UExpression uint256 false.

Payable External Function

#[external, payable]
Ursus Definition receive: UExpression unit false.

Internal Pure Helper

#[internal, pure]
Ursus Definition _min (a b: uint256): UExpression uint256 false.

Override Virtual Function

#[public, override, virtual]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

See Also