# Syntax of the Act language

A specification of a contract written in `act` consists of a `constructor` and a set of `behaviours`.

The `constructor` specification defines the structure of the contract state, the initial value for the state, and a list of invariants that the contract should satisfy.

Each `behaviour` specification determines how a contract method updates the state, and its return value, and the conditions that must be satisfied in order for it to be applied.

Alternatively, they can be thought of an initial state and a set of state transitions, determining an inductively defined state transition system.

The specifications can be exported to different backends in order to prove that the claims that are being made hold with respect to an implementation.

This document is a high level description of the syntax of act specifications. For a more formal treatment of the syntax, study the definitions of RefinedAst.hs.

## Types

The types of Act consist of three basic primitives: Integers, Booleans and ByteStrings. Integers are unbounded, with true integer operations. However, as our integer expressions will often represent words in the EVM, we allow ourselves a slight abuse of notation and denote by `uintN/intN` integers together with the constraint that the value fits into a `uintN/intN`.

Using conventional ABI types for typing also allows us to specify function signatures in a concise way.

As an example consider the specification of overflow safe addition:

``````behaviour add of SafeMath

iff in range uint

x + y

returns x + y
``````

In more verbose terms, this specification would read:

Given any pair of integers `x` and `y`, s.t. `0 <= x < 2^256` and `0 <= y < 2^256`, an ABI encoded call to the contract `SafeMath` with the signature `add(uint256,uint256)`, and `x` and `y`, will:

• return `x + y` if `0 <= x + y < 2^256`
• revert otherwise

## Contructor

A `constructor` specification is indicated by the `constructor of <contractName>` header, as in:

``````constructor of A
``````

A constructor section consists of the following fields:

### interface

Specifying the arguments the constructor takes. Example:

``````interface constructor(address _owner)
``````

### iff (optional)

The conditions that must be satisfied in order for the contract to be created. These must be necessary and sufficient conditions, in the sense that if any condition isn't met, the contract cannot be created.

Example:

``````iff

CALLER == _owner
``````

### creates

Defines the storage layout of the contract.

Example:

``````
creates

uint256 totalSupply := _totalSupply
mapping(address => uint) balanceOf :=  [CALLER := _totalSupply]
``````

### External storage changes (optional)

If the contract creation updates the state of other contracts, they should be specified as:

``````contract B
x => x + 1

contract C
y => y - 1
``````

### Ensures (optional)

A list of predicates that should hold over the poststate. All references to storage variables in `ensures` sections need to specify whether they talk about the variable's value in the pre- or the poststate, by using `pre(x)` or `post(x)`. Example:

``````
ensures

(post(x) == _x) or (pre(x) == _x)
``````

### Invariants (optional)

A list of predicates over the state of the contract that should hold before and after every contract invocation:

``````invariants

totalSupply = initialSupply
_k = x * y
``````

## Behaviour

A `behaviour` specification is indicated by the `behaviour of <contractName>` header, as in:

``````behaviour of A
``````

and consists of the following fields:

### interface

Specifying which method the behaviour refers to. Example:

``````interface transfer(address to, uint value)
``````

### iff (optional)

The conditions that must be satisfied in order for the transition to apply. These must be necessary and sufficient conditions, in the sense that if any condition isn't met, a call to the given method must revert.

Example:

``````iff

balanceOf[CALLER] >= value
CALLVALUE == 0
``````

Each behaviour must specify the state changes that happens a result of a valid call to the method, and its return argument, if any. All references to storage variables in `returns` arguments need to specify whether they talk about the variable's value in the pre- or the poststate, by using `pre(x)` or `post(x)`.

This can be specified in two ways. Either directly, as in:

``````
storage

balanceOf[CALLER] => balanceOf[CALLER] - value
balanceOf[to] => balanceOf[to] + value

returns post(balanceOf[CALLER])
``````

or split between a number of cases, as in:

``````case to == CALLER:

returns -1

case to =/= CALLER:

storage
balanceOf[CALLER] => balanceOf[CALLER] - value
balanceOf[to] => balanceOf[to] + value

returns post(balanceOf[CALLER])
``````

Note that currently, either a `storage` or `returns` section, or both is required in every spec.

### External storage changes (optional)

If the contract method updates the state of other contracts, they should be specified as:

``````contract B
x => x + 1

contract C
y => y - 1
``````

### Ensures (optional)

A list of predicates that should hold over the poststate. Example:

``````
ensures

x == _x
``````

## Referencing Storage Variables

Storage locations that are read and used in other expressions must be declared in a storage block.

Some examples:

``````storage
x => y
y
``````
``````storage
x
y

returns x + y
``
``````