Specifications

The application specifications the CEC tool takes as input are formatted in a way similar to a Boogie specification.

Examples of application specifications can be found in the specifications/applications directory present in the Git Hub repository.

Example

System Description

Consider as an example a distributed banking application.

The application has the following interface:

• withdraw(client, amount)
• deposit(client, amount)
• applyInterest(client)

The withdraw operation withdraws money from a client's bank account. The deposit operation deposits money in a client's bank account. The applyInterest operation multiplies the amount that all clients have in their bank accounts by a constant.

The invariant of the system states that no bank account may have a credit below zero.

System Specification

@import Map1K;

@init
type Client;
var INTEREST :int where INTEREST > 0;

@variables
var balances : [Client]int;

@equals [Client]int @as map1KEquals(@this, @other);

@invariant
forall c: Client :: balances[c] >= 0;


@operations

procedure deposit(c1: Client, a1: int)
    modifies balances;
    requires a1 >= 0;
    ensures map1KSet(c1, old(balances)[c1] + a1, balances, old(balances));

procedure withdraw(c1: Client, a1: int)
    modifies balances;
    requires balances[c1] - a1 >= 0;
    ensures map1KSet(c1, old(balances)[c1] - a1, balances, old(balances));

procedure applyInterest()
    modifies balances;
    ensures forall c : Client :: balances[c] == old(balances[c]) * INTEREST;

The Specification Format

The specifications are composed by six separate sections: imports, initializer, variables, equals expressions, invariant and operations. All sections have to be defined in order. Additionally all sections, besides the operations section, are optional.

• @import defines the beginning of the import section. This section is composed by a list of names of libraries that will be imported into the specification when the tool executes. The names of the libraries must be separated by comas and the list must be terminated by a semicolon.

• @init defines the beginning of the initializer section, where the user can specify, in Boogie, auxiliary data types, axioms variables, constants, functions, etc., that can then be used in the rest of the specification.

• @equals defines the beginning of a new equals expression. These are composed by two parts: type and expression written as @equals <type> @as <expression>. Each defines a Boogie expression (in the expression part) that denotes the equality criteria between two instances of the data type being specified in the type part. In the expression @this and @other are used to denote the two different instances that are being compared. More on which data types need to have an equality expression defined, can be found in the Notes section bellow.

• @variables defines de beginning of the variables section where the user should specify, in Boogie, the variables that describe the state of the application.

• @invariant defines the invariant section, where the user should specify the invariant of the application, through a Boogie expression, terminated by a semicolon.

• @operations defines the beginning of the operations section where the operations supported by the application are defined. Each operation is defined as a Boogie procedure, by a header and modifies clause, containing the variables defined in the variables field, whose values are modified after the execution of the operation. This list of identifiers should be separated by comas and terminated by a semicolon. Finally the procedure can also have a requires and ensures clause, defining the operation's pre conditions and effects, respectively, in a manner similar to Boogie.

Step by Step System Specification

Lets start by looking at the initializer section of this specification.

@init
type Client;
var INTEREST :int where INTEREST > 0;

The second line declares a new type, the type Client. The third line declares that there is a constant that is bigger then zero, named INTEREST. This is the multiplication factor that is applied in the operation applyInterest.

Now we define the variables that represents the state of the system.

@variables
var balances : [Client]int;

In this case we only use one variable, balances, that is defined as a map of Client to the amount the client has in its bank account.

Next, we define the equality expression for the variable we defined. We could define it using by writing an expression from scratch but the unit named Map1K, specified in specifications/libraries/map1k_utils.spec, already provides a default equality function for a 1 key 1 value Boogie map. To use it, we first need to import it.

@import Map1K;

Having imported the unit we can now use its functions. In this case we are using the map1KEquals function.

@equals [Client]int @as map1KEquals(@this, @other);

Now we can define the invariant.

@invariant
forall c: Client :: balances[c] >= 0;

Finally, we specify each of the three operations.

@operations

procedure deposit(c1: Client, a1: int)
    modifies balances;
    requires a1 >= 0;
    ensures map1KSet(c1, old(balances)[c1] + a1, balances, old(balances));

procedure withdraw(c1: Client, a1: int)
    modifies balances;
    requires balances[c1] - a1 >= 0;
    ensures map1KSet(c1, old(balances)[c1] - a1, balances, old(balances));

procedure applyInterest()
    modifies balances;
    ensures forall c : Client :: balances[c] == old(balances[c]) * INTEREST;

This specification can be found can be found in specifications/applications/basic_bank.json in the Git Hub repository.

Notes

• The procedures defined in the operations section cannot have return statements.
• In application specifications, the "equals" section must contain an equality expression for each of the types defined in the "variables" field, that are not data types imported from a library and are not types for which Boogie already defines equality (i.e. basic types like "type Player"). For instance, if you use a map you must specify an "equals" expression for that map.
• The CEC Tool currently does not support the use of operation parameters defined in the operations field, that are not types for which Boogie already defines equality (for instance the tool does not support using a Boogie map as a parameter of an operation).