Skip to main content

contract

A named block whose last statement is an assert. The assertion states a property that should hold. Nothing calls a contract, and no interface includes one.

contract bearing_wraps {
    let bearing_deg: int32 = 350;
    let turn_deg: int32 = 20;
    assert (bearing_deg + turn_deg) % 360 == 10;
}

Bodies​

A contract's name is unique among the file's declarations, and no other module can name it as an element of an import.

  • The body is a block whose last statement is an assert. A body that ends any other way is a parse error.
  • Intermediate assert statements are allowed.
  • The final assert's condition has type bit.
  • The body type-checks as an ordinary block, so it may hold let and statement if.
  • The body may reference any in-scope declaration, including a function and a const.
struct SearchSector { start_deg: uint16; end_deg: uint16; }

function span_deg(sector: SearchSector) -> uint16 = sector.end_deg - sector.start_deg;

const forward: SearchSector = SearchSector { start_deg = 350; end_deg = 360; };

contract forward_span_is_ten {
    let span: uint16 = span_deg(forward);
    assert span == 10;
}

Parameters​

A parameterized contract states its property for all values of its parameters. An unparameterized one states it for the single computation its body spells out.

  • Parameters are optional, and a contract with none is written with no parentheses at all. An empty () is a parse error.
  • Parameter names are unique.
  • A parameter type may be any type.
  • Parameters are in scope in the body and nowhere else.
contract average_within_bounds(low_deg: int32, high_deg: int32) {
    let mid_deg: int32 = (low_deg + high_deg) / 2;
    assert (low_deg <= mid_deg && mid_deg <= high_deg)
        || (high_deg <= mid_deg && mid_deg <= low_deg);
}

Errors​

Declaring the same parameter twice​

contract span_is_positive(start_deg: int32, start_deg: int32) {   // error: duplicate-contract-param
    assert start_deg > 0;
}

An assert condition that is not bit​

contract callsign_is_set {
    assert "Viper-1";   // error: assert-condition-type
}
  • block, let, assert — the statements a contract body holds, and what assert does inside a function.
  • function — the named body that is called and returns a value.
  • struct — the assertions that guard a value instead of stating a property.