Types

• boolean
• int
• double
• $proc : The process type.
• $scope : The scope type.

Expressions

• +, - , * , / , %
• =
• ==, <=. >=, <, >
• ++, --
• $true, $false
• $self : The process invoking the expression (constant of type $proc).
• $spawn f(e1, ..., e_n) : Spawn a process executing f on (e1, ..., e_n), return a reference to the process.
• function calls

Statements

• Expression statement : Use an expression as a statement (e.g. i++;).
• if-then-else statements : Same syntax as C.
• while, for loops
• return statement
• { <blockItem>* } : A blockItem can be a variable declaration, function definition, or statement.
• $assert <expr> : Check that <expr> holds.
• $assume <expr> : Add <expr> to the path condition.
• $wait <expr> : For <expr> of type $proc, block until <expr> terminates.
• $when (<expr>) S; : Guarded statement. Block until <expr> is true, then execute S.
• $choose : A $choose statement has the form

    $choose {
    stmt1;
    stmt2;
    ...
    default: stmt
  }
  

The "default" clause is optional. The guards of the statements are evaluated and among those that are true, one is chosen nondeterministically and executed. If none are true and the default clause is present, it is chosen. The default clause will only be selected if all guards are false. If no default clause is present and all guards are false, the statement blocks. Hence the implicit guard of the $choose statement without a default clause is the disjunction of the guards of its sub-statements. The implicit guard of the $choose statement with a default clause is "true".

Declarations

• Variable : Can optionally be specified as an input or output of the program. Have optional initialization.

[$input | $output] <type> v [= <expr>]

• Typedef : Assign an alternate name to a type.

typedef <type> <name>

• Function : Gives the name, return type, and parameters. Each function may have 0 or more declarations.

<type> f(<type> e1, ..., <type> e_n)

• Function definition: Gives the name, return type, parameters, and body. Each function must have exactly one definition.

<type> f(<type> e1, ..., <type> e_n) {...}

Program

A program is a sequence of external definitions. The external definitions are

• Variable declaration
• Function declaration
• Function definition
• $assume

A program must have a function called main which takes no arguments. Execution of the program begins in the body of main.

Example

This program calls a function that sums the numbers from 1 to n and checks that the result is equal to the closed form.

#include<civlc.h>

$input int n;
$output int s = 0;

int add(int i) {
  int sum = 0;
  for (int i=0; i<n; i++) {
    sum = sum + i;
  }
  return sum;
}

void main() {
  $assume n>0;
  s = add(n);
  $assert s == (n*(n+1))/2;
}