Imperative Language¶

Type Reference¶

A type reference refers to an existing non-generic type declaration or constant.

typeType Reference¶

«dot identifier list»

Consider the following example of type reference representations:

val size : Int = 4
var result : Array<Bool, size>

In the variable declaration of size, Int is an example of a type reference, and in the variable declaration of result, size is an example of a type reference to an integer constant.

Instantiated Type¶

An instantiated type defines an instantiation of a generic type.

typeInstantiated¶

«dot identifier list»<«types»>

where there must be at least one type specified in the list of types between the angle brackets.

Consider the following variable declarations:

    var a : Array<Bool, 3>
    var b : Bounded<0, 4>
    var c : Slot<Int>
    var d : NonVerified<Int>

The variables a, b, c, and d are declared with the instantiated types Array<Bool, 3>, Bounded<0, 4>, Slot<Int>, and NonVerified<Int> respectively.

Reference Type¶

A reference type is a reference (or pointer) to a value of that type, and is denoted using: & for an immutable reference; &mut for a mutable reference, or &out to a reference that must be written to before being read. Reference types can be used to implement out and inout parameters for functions, such as:

function swap<T>(left : &mut T, right : &mut T) : Nil = {
  val t = left;
  left = right;
  right = t;
}

See Functions for further details on out parameters.

typeReference¶

[& | &mut | &out] «type»

Reference types can only be used in conjunction with function types or when declaring the type of a function parameter. Usage of reference types outside of these contexts will result in an static error.

Function Type¶

A function type denotes the type of a function in terms of the types of its parameters, and its return type.

typeFunction¶

(«types») -> «type»

Function types are not comparable for equality, and are not defaultable, but they are verifiable.

Consider the following example:

(Int, Int) -> Bool

This function type describes a function that takes two parameters of type Int, and returns a value of type Bool. As an example, the following two function declarations are of this type:

function isEqual(a : Int, b : Int) : Bool = a == b
function notEqual(a : Int, b : Int) : Bool = a != b

Function types that do not have any parameters are simply denoted with empty parentheses. For example:

() -> Nil

This function type describes a function that does not have any parameters, and has the return type Nil.

Function types can be used as any other type, for example, in a variable declaration:

var x : (Int, Int) -> Bool = isEqual

In this example, variable x is declared to be of type (Int, Int) -> Bool, and is initialised with a reference to the function isEqual (declared above). The function contained in x can be called in the usual way, for example:

var y : Bool
y = x(2, 5)

Function types describing functions that have out or inout parameters are written in the same way, where their corresponding types capture this information. For example, consider the following function declaration:

function square(a : Int, b : &out Int) : Nil = {
  b = a * a;
}

In this case, the function type for square is:

(Int, &out Int) -> Nil

In this example, the second parameter of this function type is of an out reference type.

Function types can only be made to represent the types of static (i.e. non-member) functions. This means that it is not possible (currently) to write the type of a function that is defined within a state machine in Coco.

The following example illustrates how function types can be used in combination with the builtin Optional and Signal types in a port state machine:

port P {
  function check() : Nil
  outgoing signal ok(x : Bool)
  outgoing signal fail(x : Bool)

  machine {
    var x : Bool
    var response : Optional<(Bool) -> Signal>

    function setResponse() : Nil = {
      x = nondet {
        true,
        false,
      };
      response = Optional.Some(nondet {
        P.ok,
        P.fail,
      });
    }

    check() = {
      setResponse();
      send(response.value()(x));
    }
  }
}

In the above, the expressions P.ok and P.fail are both references to functions of type (Bool) -> P.Signal that construct the corresponding signal (of type P.Signal) without sending it.

Binary Type¶

A binary type refers to a type that is defined using a binary operator.

typeBinary¶

«type» «operator» «type»

Consider the following example of a binary type, which uses the addition operator:

val kLimit : Int = 7
var counter : Bounded<0, kLimit + 1>

In the instantiated type Bounded<0, kLimit + 1>, kLimit + 1 is an example of a binary type.

Coco currently supports integer operators in binary types only.

Unary Type¶

A unary type refers to a type that is defined using a unary operator.

typeUnary¶

«operator» «type»

Consider the following example of a unary type, which uses the integer negation operator:

var counter : Bounded<-5, 5>

In the instantiated type Bounded<-5, 5>, -5 is an example of a unary type.

Coco currently supports the integer negation operator in unary types only.

Dependent Member Type¶

typeDependent Member¶

«dot identifier list»<«types»>.«identifier»

where there must be at least one type specified in the list of types between the angle brackets.

Fields¶

Many declarations in Coco consist of one or more field declarations of the form id : T, where id is a name being declared of type T. For example, components and ports are declared through lists of fields that give their constituent parts.

declarationField¶

(val | var) «identifier» : «type»

For example, a port declaration could have the following field declarations:

val oneControlPort : ControlPort
val manyControlPorts : Array<ControlPort, 5>

This declares two ports called oneControlPort of type ControlPort, and manyControlPorts of type Array<ControlPort, 5>.

Variables¶

A variable is a named value, which can be referenced in the code. In Coco, there are two types of variables: a mutable variable, declared with the keyword var, where the value of the variable can be modified; and a constant variable, declared with the keyword val, where the value of the variable cannot be modified.

declarationVariable¶

[var|val] «identifier» [: «type» | = «expression» | : «type» = «expression»]

In a declaration statement, a variable can be declared without its type, and with an initial value only. Coco will then infer the type of the variable from the initial value.

If a variable is declared to be of a type T without an initial value, and there is an instance of Default declared for T, then it will be assigned the default value of T. For example:

var x : Int
val y : Bool = true

Variable x is declared as a mutable variable of type Int. Although x is not explicitly assigned an initial value, there is an instance of Default declared for Int with the default value 0, and therefore x will be assigned the value 0. Variable y is a constant of type Bool, and is explicitly initialised with the value true.

Variables must be initialised in order. For example, the following variables declared at the top-level of a module is not valid:

val x : Int = y
val y : Int = 5

Instead, the valid ordering in Coco is:

val y : Int = 5
val x : Int = y

If a variable is declared to be of a type T that does not have an instance of Default, then the variable declaration must either assign an initial value as part of its declaration, or it can be declared as being of type Slot<T>, which means that the verification will check whether the variable is being accessed correctly or not. For example:

var z : Slot<Int>

The variable z is declared to be of type Slot parameterised with type Int, which means that although the actual value of z is not verified, the verification will check whether z is accessed correctly.

See Slot in the Standard Library section for further details on slots, and the description of a state machine declaration in the State Machines section regarding the restrictions of their use in port state machines.

A variable is local to the scope in which it is declared. For example, a variable declared inside a function is local to that function, and a new variable is created every time the function is called. Variables declared inside a state machine are created when the state machine is initialised, and destroyed when the state machine terminates.

Functions¶

A function defines a reusable block of code that can be called from different places. It has a function name, which is used to call the function when required elsewhere in the code. A function can have parameters, each declared with a parameter name and type, and specifies its return type.

declarationFunction¶

function «identifier»(«parameters») : «type» = «expression»

«parameter» := [var] «identifier» : «type»

A function will either return the value given by an explicit return statement (like other imperative programming languages), or it will return the value computed by its expression (like expression-orientated languages such as Haskell or Rust). For example:

function id(argument : Int) : Int = {
  return argument;
}

function id2(argument : Int) : Int = argument

The functions above give two equivalent definitions of the identity function, where both versions return their argument unaltered. The first version uses an explicit return statement, whereas the return value of the second version is computed by evaluating the expression argument.

Function parameters can either be passed by value or passed by reference. If a function parameter is passed by value, then by default is is immutable in the body of the function; that is, they can be read but not written to. To allow the parameter to be mutated, it must be prefixed by the keyword var. Assignments to a var parameter within the called function are local to the called function only, and have no effect on the calling function.

The value of a parameter passed by reference, namely what it is referencing, is immutable; it is not valid to declare a parameter of type var v : T, where T is a reference type. For a parameter of type v : T, where T is a reference type, the assignment expression v = x means the value that v refers to is assigned the value of x; it does not change what v is referring to. The values that are being referred to may be mutable depending upon the parameter’s reference type. If a parameter is of type &T for some type T, then the values being referenced are immutable, whereas if it is of type &mut T or &out T, then they are mutable. The difference between the types &mut T or &out T is that for a parameter of type &out T, the value being referenced must be assigned a valid value within the called function before it returns, and before the value can be read. Any changes made by the function to the values in either case will persist after the function returns.

Consider the following example:

function square(x : Int) : Int = x * x

function testSquare(x : Int, y : &out Int) : Nil = {
  var v : Int;
  y = square(x);
  v = x + 1;
  y = square(v);
}

The function square(x : Int) takes an immutable parameter passed by value called x of type Int, and returns the result of evaluating x * x. The function testSquare(x : Int, y : &out Int) takes two parameters, the second of which is a parameter of reference type &out Int. This function modifies the value of y twice before it returns.

Member functions (for example, declared in a struct or enum) cannot be called on &out parameters, unless they have been written to first. Consider the following example:

function f1(x : &out Optional<Int>) : Nil = {
  x.reset();
  x = Optional.Some(5);
}

The function f1(…) is invalid Coco, because the member function reset() of the enum Optional<Int> is being called on the &out parameter x, which has not been written to yet.

The same applies to non-mutating member functions, since they still need to be able to read the value they are being called upon. For example, the following function f2(…) is also invalid Coco:

function f2(x : &out Optional<Int>) : Bool = {
  var y : Bool;
  y = x.hasValue();
  return y;
}

The following function f3(…) extends f2(…) by assigning a value to x before the member function hasValue() is called on it, and is therefore valid Coco:

function f3(x : &out Optional<Int>) : Bool = {
  var y : Bool;
  x = Optional.Some(5);
  y = x.hasValue();
  return y;
}

In the previous example of the function testSquare(…) above, the local variable v can be removed by changing the parameter x to be mutable using the keyword var as follows:

function square(x : Int) : Int = x * x

function testSquare2(var x : Int, y : &out Int) : Nil = {
  y = square(x);
  x = x + 1;
  y = square(x);
}

In this case, all references to x are references to the automatically created local variable with the same name, initialised with the value passed in the function call. In contrast, consider the following example:

function InvalidFn(x : Int, y : &out Int) : Nil = {
  var z : Int = y;
}

This function is invalid for two reasons: the parameter y is being read before a value has been assigned to it, and the function returns without having assigned a value to y.

When a function is called, the arguments corresponding to parameters of a reference type must be prefixed with &, with the exception of when references are forwarded as the arguments in a function call:

function increment(x : Int, y : &out Int) : Nil = {
  y = x + 1;
}

function testIncrement() : Nil = {
  var z : Int = 1;
  increment(z, &z);
  assert(z == 2);
}

& must be applied directly to a variable, and cannot be applied to arbitrary expressions.

The following example illustrates the case where a function is called, and is passed a reference as its argument:

function f(x : &out Bool) : Nil = g(x)

function g(x : &out Bool) : Nil = {
  x = true;
}

In this example, function f is calling g, and passing on the reference to its &out parameter. In this case, it is not necessary to prefix the argument x with & when calling g, because x is declared to be of the same type &out in f. It is therefore valid to simply write g(x) instead.

Functions can take functions as parameters, and return functions. For example:

function compute(x : Int, y : (Int) -> Int) : Int = y(x)

The function compute takes two parameters, the second of which is function of type (Int) -> Int, and returns the value of calling y(x). The following example illustrate how this function can be called passing a function reference as its argument:

function square(x : Int) : Int = x * x

function cube(x : Int) : Int = x * x * x

function testCompute(a : Int) : Int = {
  val x : Int = compute(a, cube);
  val y : Int = compute(a, square);
  return x + y;
}

The following example illustrates how a function can take functions as arguments, and have a function type as its return type:

function f1() : (&out Bool) -> Nil = f2

function f2(b : &out Bool) : Nil = {
  b = true;
}

function f3() : Bool = {
  val vF1 : () -> (&out Bool) -> Nil = f1;
  val vF2 : (&out Bool) -> Nil = vF1();

  var b : Bool;
  vF2(&b);
  return b;
}

In this example, the function f1 has the return type (&out Bool) -> Nil, and returns a reference to the function f2 in its function body. The function f2 takes a parameter of type &out Bool, which is assigned the value true in its function body, and has a return type Nil. The function f3 does not have any parameters, and returns a value of type Bool. In its body, it declares two variables, vF1, which is initialised with a reference to the function f1, and vF2, which is initialised with the function stored in vF1. The function f3() then calls vF2(&b), and returns the value of b, which in this case will be the value true.

Functions which are directly or indirectly called recursively cannot call functions on required ports, emit signals, or use nondet expressions.

Function Interfaces¶

A function interface declaration is used to declare a function in a port declaration.

declarationFunction Interface¶

function «identifier»(«parameters») : «type»

«parameter» := «identifier» : «type»

For example:

function start() : Nil
function check(v : Int) : Bool

Signals¶

A signal declaration is used to declare a signal in a port declaration.

declarationSignal¶

outgoing signal «identifier»(«parameters»)

«parameter» := «identifier» : «type»

For example:

outgoing signal ok()
outgoing signal error(status : Bool)

Enumerations¶

An enumeration, also called an enum, defines a type with a finite number of named values, referred to as enum cases. In Coco, enum cases can also have data values associated with them. These are referred to as tagged enums, and are effectively a type safe union.

declarationEnum¶

enum «identifier» {
  «enum elements»
}

«enum element» := «enum case» | [mut] «function»

«enum case» := case «identifier»[(«parameters»)] [= «expression»]

«parameter» := «identifier» : «type»

where if an enum case has parentheses, then it must have at least one parameter inside them.

The name of an enum becomes the name of its type. An enum case is referenced elsewhere by using a dot (.) between the enum type name and its case name, as illustrated in the examples below. An enum can also have member functions, which can be called on an instance x of the enum by using a dot (.), for example, x.fn(). If a member function is preceded by the keyword mut, then it means that the function is permitted to modify the value of the enum.

An enum where none of its cases have parameters is called a simple enum, whereas an enum that has at least one enum case with parameters is called a tagged enum.

Simple enums are always comparable for equality, and defaultable with the default value being the first enum case listed in the declaration. Coco will automatically generate instances of Eq and Default without having to label them with the @derive attribute. For example:

enum SimpleColour {
  case Red
  case Blue
  case Green
}

function isDefaultColour() : Bool = {
  val v : SimpleColour;
  return v == .Red;
}

The function isDefaultColour() will return true, since the variable v is assigned the default value Colour.Red when it is declared.

By default, tagged enums are not comparable for equality, but they can be labelled with @derive(Eq) so that Coco automatically derives an instance of Equality when every parameter type in every enum case has an instance of Eq. Likewise, by default tagged enums are not defaultable, but derive(Default) can be used to automatically derive an instance of Default when all of the parameters of the default enum case are defaultable, where the default enum case is the first enum case listed in the declaration.

The following example is of a tagged enum, where one of the enum cases has parameters to represent different colours:

@derive(Default, Eq)
enum Colour {
  case RGB(red : Int, green : Int, blue : Int)
  case None
}

function isEqualColour() : Bool = {
  val v : Colour;
  return v == .RGB(0, 0, 0);
}

In this example, Colour is a tagged enum where the first enum case RGB has three parameters of type Int representing the decimal colour codes, and the second enum case None does not have any parameters, representing the case where no colour is specified. Colour is defaultable with the default value .RGB(0, 0, 0), and is comparable for equality since every parameter is of type Int, which in turn is comparable for equality.

The following example illustrates how member functions can be declared in an enum declaration:

@derive(Default)
enum ErrorStatus {
  case None
  case Error(id : Int)

  mut function reset() : Nil = {
    self = None;
  }

  function status() : Bool = {
    match (self) {
      None => false,
      Error(_) => true,
    }
  }
}

The following simple functions illustrate how a variable can be declared to be of type ErrorStatus, and its member functions called:

function hasError1() : Bool = {
  var error : ErrorStatus;
  error = .Error(3);
  return error.status();
}

function hasError2() : Bool = {
  var error : ErrorStatus;
  error = .Error(3);
  error.reset();
  return error.status();
}

The function hasError1() always returns true, because the variable error is assigned the value .Error(3), and therefore the member function error.status() returns true. In contrast, the function hasError2() always returns false, because after the variable error is assigned an error value, and before the function returns, error is reset to .None as a result of calling error.reset().

Structures¶

A structure, also called a struct, combines several types into a larger compound type, giving each value within the structure a name.

declarationStruct¶

struct «identifier» {
  «struct elements»
}

«struct element» := «field» | [mut] «function»

The name of the struct becomes the name of its type. If x is a variable of a struct type S, where S has a field f with type T, then x.f can be read from, and assigned a value of type T. A struct S can also have member functions, which can be called on an instance x of the struct by using a dot (.), for example, x.fn(). If a member function is preceded by the keyword mut, then it means that the function can modify the values assigned to fields in the struct.

By default, structs are not defaultable, but they can be labelled with @derive(Default) so that Coco automatically derives an instance of Default when the type of every field has an instance of the class Default. Likewise, by default structs are not comparable for equality, but derive(Eq) can be used to automatically derive an instance of Eq when the type of every field has an instance of the class Eq. See @derive for further details regarding which traits can be derived for structs.

Consider the following example of a struct called Message, which implements a simple buffer, together with member functions to read from, write to, and reset it:

val size : Int = 2

type Buffer = Array<Int, size>

@derive(Eq)
struct Message {
  var store : Buffer
  var index : Int

  mut function reset() : Nil = {
    for index in range(0, size) {
      store[index] = Int();
    }
    index = 0;
  }

  mut function write(data : Int) : Bool = {
    if (index < size) {
      store[index] = data;
      index = index + 1;
      return true;
    }
    return false;
  }

  function read() : Optional<Buffer> = {
    if (index == size) {
      return Optional.Some(store);
    }
    return Optional.None<Buffer>;
  }
}

The function reset() is an example of a mutating member function, as it resets all of the array elements to the default value of Int. In contrast, the function read() is not, as it simply returns the value of store in the case where it has been written to, or Optional.None<Buffer> otherwise.

Message is labelled with @derive(Eq), which means that Coco will try to automatically derive the instance of the trait Eq for this struct. This is necessary to compare instances of Message for equality, for example as illustrated in the following function isEqual(…), which returns .Ok(nil) if the two arguments of type Message are equal, and .Error(y) otherwise, where y is the value of the second argument:

function isEqual(x : Message, y : Message) : Result<Nil, Message> =
  if (x == y) {
    return .Ok(nil);
  } else {
    return .Error(y);
  }

function run(x : Message, y : Message, z : Message) : Result<Bool, Message> = {
  isEqual(x, y)?;
  isEqual(x, z)?;
  return .Ok(true);
}

The function run(…) returns the value .Ok(true) if all of its arguments are equal. If either of the expressions of the form isEqual(a, b)? evaluates to .Error(b), then run(…) will immediately return with the value .Error(b).

Type Aliases¶

A program may give new names to existing types by using type aliases.

declarationType Alias¶

type «identifier» = «type»

The newly named type behaves identically to the type for which it is an alias. However, it may have different attributes attached to it, so two otherwise identical types with different names may be treated differently by the code generation or verification tools.

The following example illustrates how a type alias can be defined and used:

type TemperatureDegrees = Int

function warm(t : TemperatureDegrees) : TemperatureDegrees = if (t < 40) t + 1 else t

External Functions¶

Coco provides a range of language constructs to support the integration of the generated code into the rest of the system. One of these is an external function declaration, which allows Coco programs to reference functions that are defined by some other implementation outside the scope of the Coco program, but that the Coco generated code will be able to use.

declarationExternal Function¶

external function «identifier»(«parameters») : «type» = «expression»

«parameter» := [var] «identifier» : «type»

The body of an external function is an expression, which cannot use any non-verified types, or instances of the Abstracted type.

An external function is similar to a port in the sense that it provides the specification of the function, not its implementation. The body of an external function is only used during the verification; no code is generated from it.

Consider the following simple example:

enum Command {
  case Start
  case Stop
}

external function getCommand() : Command =
  nondet {
    .Start,
    .Stop,
  }

The external function getCommand() returns a value of type Command. The return value is chosen nondeterministically, and the possible return values will be taken into account when verifying calls to the function.

The following function declaration calls the external getCommand() function in a match:

function convertToBool() : Bool = {
  var command : Bool;

  command = match (getCommand()) {
    .Start => false,
    .Stop => true,
  };
  return command;
}

If the return type of an external function is a non-verified type, then the undefined expression (_) must be used as the return value:

external function errorMessage() : String = _

In this example above, the external function errorMessage() returns a value of type String, which is a non-verified type, and therefore the body of the function must be _.

When an external function is declared with an &out parameter, Coco requires the &out parameter to be written to, and therefore assumes the code implementing this function will write a valid value. This has to be specified in the body of the external function. For example:

external function writeBool(v : &out Bool) : Nil = {
  v = nondet {
    true,
    false,
  };
}

If an &out parameter is of a non-verified type, then it must be assigned the undefined expression (_) in the external function’s body, as illustrated in the following example:

external type Data

external function getData(v : &out Data) : Nil = {
  v = _;
}

In this example, getData(...) has an &out parameter v of external type Data, and is therefore a non-verified type. The assignment v = _ in the function body means that the function will write an arbitrary but valid value to its &out parameter before it returns.

The assumption that &out parameters are always written to is particularly useful when passing a reference to a Slot<T> to a function that has an &out parameter of type T, since it means that the slot can be assumed to be valid by the time the function returns. To illustrate this, consider the following example:

external function getTimeoutValue(v : &out NonVerified<Int>) : Nil = {
  v = _;
}

function getDuration() : Duration = {
  var timeout : Slot<Int>;
  getTimeoutValue(&timeout);
  return seconds(timeout);
}

In this example, the function getDuration() converts an Int into a Duration, which can then be used in timer transitions in a component state machine. When the local variable timeout is declared as a Slot<Int>, its default value is SlotStatus.Invalid, indicating that the slot does not contain a valid value at this stage. However, it is guaranteed to be assigned a valid value upon return of getTimeoutValue(&timeout).

If an external function has a parameter that is passed by value, mutable, and of a non-verified type, then it should be assigned the undefined expression (_) in the function body, as illustrated in the following example:

external function f1(var d : NonVerified<Int>) : Nil = {
  d = _;
}

External Types¶

An external type declaration allows users to refer to a type that is not defined within their Coco program, but is defined somewhere else in the code. External types help integration of the generated code into the rest of the system.

declarationExternal Type¶

external type «type» [{
  «external type elements»
}]

«external type element» :=
  static val «identifier» : «type» = «expression»
  | «variable declaration»
  | [mut] «external function»

where variable declarations must be of a type that has an instance of Verified.

Like external functions, the body of an external type is only used during the verification; no code is generated from it.

A user-defined external type T is not verifiable, and not defaultable. Users can specify that a custom external type T is defaultable by declaring an instance of Default for T.

A variable can be declared to be of some external type T. If there is no instance of Default declared for T, then the variable declaration must either be given an explicit initialisation, or it must be declared to be of type Slot of type T instead.

External Constants¶

Constants defined outside of Coco can be declared as an external constant in Coco.

declarationExternal Constant¶

external val «identifier» : «type» = «expression»

External constants must be declared with a value, which is used for verification purposes only. For example:

external val kLimit : Int = 4

This declares the external constant kLimit of type Int with value 4. During verification, Coco will assume that it has the value 4.

Variable Reference¶

One of the basic building blocks in Coco is a variable expression, which allows existing declarations to be referenced.

expressionVariable Reference¶

«dot identifier list»

Member Reference¶

A member reference expression is used to reference the value of a field within an instance of some type.

expressionMember Reference¶

«expression» . «identifier»

For example, consider the following struct declaration:

struct Date {
  var day : Int
  var month : Int
  var year : Int
}

Given a variable declaration called date of type Date, date.day refers to the value of the field day within the instance of the variable date.

Implicit Member¶

An implicit member expression is an abbreviated way of accessing a member of a type, without having to explicitly specify the type. This can be used in contexts where the type can be automatically inferred.

expressionImplicit Member¶

.«identifier»

For example, consider the following simple enum:

enum SimpleColour {
  case Red
  case Blue
  case Green
}

function isDefaultColour() : Bool = {
  val v : SimpleColour;
  return v == .Red;
}

In the function isDefaultColour(), the implicit member expression .Red can be used as an abbreviation for SimpleColour.Red, since its type can be inferred from the type of v.

Implicit member expressions can also be used in other contexts, such as:

• Builtin attributes, for example @runtime(.MultiThreaded, .SingleThreaded), @queue(.Unbounded(1)), and @ignoreWarning(.DeadState);
• Queue control functions, for example setAllow(r, .sigA) and setUnique(r, .sigA);
• setAccess functions, for example setAccess(r, .Shared).

Struct Literal¶

An struct literal expression is used to assign values to fields in a struct.

expressionStruct Literal¶

«expression» {
  «field assignments»
}

«field assignment» := «identifier» = «expression»,

The following example illustrates the use of a struct literal:

struct ColourCode<T> {
  var red : T
  var green : T
  var blue : T
}

function red() : ColourCode<Int> = ColourCode{ red = 255, green = 0, blue = 0 }

Operators¶

Coco provides a range of operators, which are commonly found in other programming languages. These include binary and unary operators for integer and boolean types, each described in turn below. All of the operators in Coco have the same precedence as in C.

1 + 2

6 + 2 is equal to 8
6 - 2 is equal to 4
6 * 2 is equal to 12
6 / 2 is equal to 3
6 % 2 is equal to 0

x = (y * m) + r

13 = (4 * 3) + 1

-13 = (4 * -3) + -1

Try Operator¶

The try operator, written as ?, can be used to simplify error handling by reducing the amount of code used to propagate errors in the case of functions that return either the Result or Optional type.

expressionTry Operator¶

«expression»?

where the expression must evaluate to a value of type Result or Optional.

Given an expression x?, where x evaluates to a value of type Result<T, E>, if x evaluates to .Ok(v) for some value v of type T, then x? will evaluate to v. Otherwise, if x evaluates to .Error(e) for some error value e of type E, then x? will cause the calling function to immediately return with the value .Error(e).

For an expression of the form e : Result<T, E>, a function of the form f(e?) is equivalent to the following expanded version using match:

f(match (e) {
  .Error(x) => { return .Error(x); },
  .Ok(v) => v,
})

This illustrates why a function that evaluates an expression of the form e?, where e is of type Result<T, E>, must also have return type Result<S, E>. Note that although the parameter types T and S may differ, the parameter type E for the error case must be the same in both cases in order to handle the early return of the enclosing function. This is illustrated in the following examples below.

The following function is an example of one that takes an argument x of type Int, and returns a value of type Result<Int, Nil>:

function check(x : Int) : Result<Int, Nil> =
  match (x) {
    0 => .Error(nil),
    _ => .Ok(x),
  }

When check(v) is called, it returns .Error(nil) if v is equal to 0, and .Ok(v) otherwise.

The following example illustrates how a function can use the try operator when calling check:

function sum(x : Int, y : Int, z : &mut Int) : Result<Bool, Nil> = {
  z = check(x)? +check(y)?;
  return .Ok(true);
}

When evaluating check(x)? and check(y)?, if either of them evaluates to .Error(nil), then the function sum will immediately return .Error(nil). Otherwise, it will assign the value resulting from x + y to z, and return .Ok(true).

The builtin enum Result is labelled with the attribute @mustUse. This means that when a function evaluates an expression e of type Result, it must also use a corresponding value of e, as illustrated with the following modified version of the example above:

function sum2(x : Int, y : Int, z : &mut Int) : Result<Bool, Nil> = {
  check(x)?;
  check(y)?;
  z = x + y;
  return .Ok(true);
}

If either check(x) or check(y) was accidentally called without ?, then Coco would give an error pointing out that the value is of type Result<Int, Nil>, and must be used due to the attribute @mustUse on Result.

The try operator can also be applied to expressions that evaluate to a value of type Optional. For an expression of the form e : Optional<T>, a function of the form f(e?) is equivalent to the following expanded version using match:

f(match (e) {
  .None => { return .None; },
  .Some(v) => v,
})

A function that evaluates an expression of the form e?, where e is of type Optional<T>, must also have return type Optional<S>. As is the case for Result, T and S may differ. Unlike Result, the error case resulting in the early return of .None does not have a parameter, and therefore can always be handled by an enclosing function that has return type Optional<S> for any type S.

The following functions illustrate the use of ? and Optional together:

function step(x : Int) : Optional<Int> =
  match (x) {
    0 => .None,
    _ => .Some(x),
  }

function multipleSteps(x : Int, y : Int, z : Int) : Optional<Int> = {
  step(x)?;
  step(y)?;
  step(z)?;
  return .Some(x + y + z);
}

In this example, if any of the calls to step result in .None, then the enclosing function multipleSteps will immediately return with the value .None. Otherwise, it will return with the value .Some(v), where v is the sum of arguments given for x, y, and z.

Block¶

A block expression comprises a sequence of semicolon-separated statements, and optionally an expression that describes a block of code. When the block gets evaluated it will either give the value nil, or the value of the expression at the end of the block.

expressionBlock¶

{
  «statements»
  [«expression»]
}

The final expression, if present, has no trailing semicolon. The value and type of the block are those of the final expression. If the final expression is absent, the value of the block expression is nil.

The following function is an example of one where the value of the block expression is given by the final expression y:

function quad1(x : Int) : Int = {
  var y = x + x;
  y = y + y;
  y
}

In contrast, the following function is an example of one with a block expression that does not end with an expression:

function ignore(x : Int) : Nil = {
  var y = x + x;
  y = y + y;
  y;
}

In this case, the value of the block expression, and hence the function is nil.

The following example is of a function with a block expression that also does not end with an expression, but instead has an explicit return statement:

function quad2(x : Int) : Int = {
  var y = x + x;
  y = y + y;
  return y;
}

In this example, the result of the function is returned explicitly and is of type Int.

Assignment¶

An assignment expression is used to assign values to variables.

expressionAssignment¶

«expression» = «expression»

The value of a mutable variable can be modified using an assignment expression, for example:

function modifyVar() : Nil = {
  var x : Int = 5;
  x = x + 1;
  assert(x == 6);
}

Arrays¶

An Array is a container type in Coco, and stores values of the same type in an ordered list. For example:

  var x : Array<Bool, 2>;
  var y : Array<Int, 4>;

Variable y is declared as an array of length 4, and contains values of type Int. It has not been provided with an initial value as part of its declaration, and therefore all of the elements in the array will be given the default value 0 of their type Int.

There are two expressions used to access the elements in an array, namely an array literal, and an array subscript.

expressionArray Literal¶

'['«expressions»']'

where the expressions in the square brackets is a comma-separated list of expressions each of which must evaluate to a value of the same type.

When an array literal is used to initialise an array, the type of the expressions in the array literal must match the type of the array being declared. For example:

  var a : Array<Int, 4> = [2, 4, 6, 8];

expressionArray Subscript¶

«expression»'['«expression»']'

In Coco, array subscripting starts with 0, and therefore the first location in an array a is a[0]. The subscript expression must evaluate to a value of a type that has an instance of Integer.

The array subscript expression is used to access the values stored in an array. For example, using variable x in the example above, we can access the values of its elements using an array subscript expression:

  val c : Bool = x[0];

c is declared to be a constant variable of type Bool, and is initialised with the value stored in location 0 of the array x as its initial value (i.e. true).

Coco also supports multi-dimentional arrays. For example:

  var m : Array<Array<Bool, 2>, 3>;

The value of m[0] is [false, false], and the value of m[0][0] is false.

Array subscript expressions can also be used in assignment expressions to modify the values in an array. For example:

  x[0] = Bool();
  y[3] = 5;
  m[0][1] = true;

where x, y, and m are declared in the previous examples above. In these assignment expressions, x[0] is assigned the default value of Bool, y[3] is assigned the value 5, and m[0][1] is assigned the value true.

Function Calls¶

A program can use a function by making a function call. A function call comprises the function’s name and arguments that match the order and types of the parameters in the function declaration. The arguments are evaluated from left to right before being passed to the function.

expressionFunction Call¶

«expression»(«expressions»)

A function call expression evaluates the result returned by the function, and the type of the expression is the return type of the function.

The following example is of a simple function, which returns the sum of two integers, and a function testSum(), which calls sum(2, 3):

function sum(x : Int, y : Int) : Int = x + y

function testSum() : Nil = {
  val x : Int = sum(2, 3);
  assert(x == 5);
}

Sending Signals¶

A program can send a signal to other parts of the system. The syntax for sending a signal is the same as for a function call expression.

expressionSignal Send¶

«expression»(«expressions»)

where the type of the signal send expression is Nil.

A signal send expression is used in state machines to describe the communication between components. For example:

port P {
  function checkStatus() : Nil
  outgoing signal ok()

  machine {
    checkStatus() = ok()
  }
}

This simple port P declares a function called checkStatus(), and an outgoing signal called ok(). Its state machine specifies that when checkStatus() is called, it will send the signal ok().

Conditionals¶

Coco has two types of conditional expressions, if and match, which enable different branches of code to be executed depending on certain conditions.

function toggle1(x : Int) : Int = {
  if (x == 0) {
    return 1;
  } else {
    return 0;
  }
}

function toggle2(x : Int) : Int = {
  if (x == 0) {
    return 1;
  }
  return 0;
}

function toggle3(x : Int) : Int = if (x == 0) 1 else 0

function safeToggle(x : Int) : Int = {
  match (x) {
    0 => 1,
    1 => 0,
    _ => x,
  }
}

function squareUnlessRootOf(x : Int, y : Int) : Int = {
  match (x * x) {
    y => x,
    val z => z,
  }
}

val Max : Int = 5

enum Message {
  case None
  case Data(msg : Bounded<0, Max - 1>)
}

function unpackMessage(m : Message) : Int = {
  match (m) {
    .None => -1,
    .Data(d) => d,
  }
}

function f1(y : Int, z : &out Int) : Nil = {
  L1: match (y) {
    0 => {
      z = 5;
    },
    _ => {
      L2: match (y * 2) {
        10 => {
          z = 15;
        },
        20 => {
          z = 30;
          break;
        },
        30 => {
          z = 40;
          break L2;
        },
        _ => {
          z = 0;
          break L1;
        },
      };
      break;
    },
  };
}

Nondeterministic Choice¶

Coco has a nondet expression, which enables different branches of a program to be executed, the choice of which is decided nondeterministically. This type of expression is essential for expressing port state machines, which describe partial views of behaviour that are visible across a component (e.g. software) boundary.

expressionNondet¶

nondet {
  «nondet clauses»
  [otherwise «expression»]
}

«nondet clause» := [if («expression»)] «expression»,

where the guard expression in the nondet clause must evaluate to a value of type Bool, and strictly side-effect free. If the expression in the nondet clause is a block expression, then the semicolon at the end of the clause is omitted. A nondet must have at least one nondet clause.

A nondet expression will execute one of the nondet clauses that either has a guard that evaluates to true, or no guard. The choice of which clause is chosen is made nondeterministically. If there are no such clauses, then the fallback expression, denoted by the keyword otherwise, will be evaluated.

Consider the following example of a simple port:

port P {
  function checkStatus() : Bool

  machine {
    checkStatus() = nondet {
      true,
      false,
    }
  }
}

Port P declares a single function checkStatus(), which returns a value of type Bool. Its state machine specifies that when checkStatus() is called, it will return true or false nondeterministically.

It is a dynamic error for a nondet expression to have no nondet clauses available, and no otherwise expression.

Optional¶

An optional expression is one that nondeterministically decides either to perform a given expression, or do nothing. A common use of optional is in a transition’s event handler in a port state machine, for example to specify that upon receiving a function call, either a signal is sent or no action is taken, the decision of which is nondeterministic. Expressing this choice as an optional expression is more efficient than using a nondet expression, as the latter would require the explicit addition of the nondet clause to represent the no action option (i.e. {}).

expressionOptional¶

optional «expression»

where the expression must evaluate to a value of type Nil.

If the optional argument is not a nondet expression then:

optional «expression»

is semantically equivalent to:

nondet { «expression» , {} }

In contrast, if the optional argument is a nondet expression then:

optional nondet {
  «nondet clauses»
}

is semantically equivalent to:

nondet {
  «nondet clauses» , {}
}

For example, the expression:

optional nondet { e1, e2, e3, }

is semantically equivalent to:

nondet { e1, e2 , e3 , {} }

A nondet expression in an optional argument cannot have an otherwise clause.

Consider the following example of a simple port P1:

port P1 {
  function check() : Nil
  outgoing signal error()

  machine {
    check() = optional error()
  }
}

When the function check() is called, the state machine will either send the error() signal or do nothing; in both cases it will stay in state Main where check() can be called again. The event transition for check() is equivalent to writing the following:

    check() = nondet {
      error(),
      {
      },
    }

Consider the following port P2, where the signal is extended with a boolean parameter, and the expression passed to optional is a nondet expression:

port P2 {
  function check() : Nil
  outgoing signal error(status : Bool)

  machine {
    check() = optional nondet {
      {
        error(true);
        setNextState(Terminated);
      },
      error(false),
    }
  }
}

In P2, when check() is called, the state machine will nondeterministically choose to either: send the signal error(true), and transition to the Terminated state; send the signal error(false), and remain in the same state; or do nothing, and remain in the same state.

Default Constructors¶

A default constructor expression evaluates to the default value of a type T that has an instance of Default declared for it.

expressionDefault Constructor¶

«type»()

The following example illustrates how a simple integer value can be reset using the default constructor for Int:

function resetInt() : Int = {
  var a : Int = 5;
  a = Int();
  return a;
}

This simple function resetInt() declares a local variable a of type Int with initial value 5. Variable a is then reset using the default constructor, resulting in resetInt() returning 0.

Default constructors can also be used for more complex types such as arrays, for example:

function resetArray() : Bool = {
  var store : Array<Int, 2> = [5, 5];
  store = Array<Int, 2>();
  return (store[0] == 0 && store[1] == 0);
}

In this example, resetArray() declares a local variable store as an array of integers of size 2, with initial value [5, 5]. The variable store is then reset using the default constructor for the array type, resulting in resetArray() returning true.

Cast¶

A cast expression converts an expression of one type into an expression of a different type.

expressionCast¶

«expression» as «type»

Undefined¶

An undefined expression can be used when its type does not have an instance of Verified.

expressionUndefined¶

_ [: «type»]

Consider the following example:

external type ErrorCode

port P {
  function start() : Nil
  outgoing signal ok()
  outgoing signal failed(error : ErrorCode)

  machine {
    start() = nondet {
      ok(),
      failed(_),
    }
  }
}

The argument passed to the signal failed(_) is an undefined expression, which is valid because its parameter type ErrorCode is an external type, and therefore not verifiable.

The full form of an undefined expression (i.e. _ : T) only needs to be used when there is ambiguity about which overload of a function or signal would be called.

Side Effects¶

An expression is side-effect free precisely when it does not:

• Mutate any variables.
• Call any functions on a required port that are not labelled with the @noSideEffects attribute.
• Emit any signals in a provided port.

The arguments to the following built-in functions in Coco have to be side-effect free: assert, after, and periodic.

An expression is strictly side-effect free precisely when it is side-effect free, and it does not call any functions on a required port. The following Coco constructs only permit expressions that are strictly side-effect free: state invariants; and guards on transitions, nondet clauses, and offer clauses.

To illustrate this side-effect free property, consider the following examples of components below, which use the following simple port P:

port P {
  @noSideEffects
  function f1() : Bool
  function f2() : Bool

  machine {
    // ...
  }
}

P declares two functions, f1() and f2(), where f1() is labelled with the @noSideEffects attribute.

The first example is of a component has P as its provided port, but fails to comply with the requirement that f1() cannot have side-effects because it mutates the variable x:

@runtime(.MultiThreaded)
component InvalidC1 {
  val client : Provided<P>

  machine {
    var x : Int
    client.f1() = {
      x = 1;
      true
    }
  }
}

The second example is of a component that also fails to comply with the @noSideEffects constraint on f1(), because it calls f2() on its required port P in response to a client.f1() call event, and f2() is not declared as being side-effect free:

@runtime(.MultiThreaded)
component InvalidC2 {
  val client : Provided<P>
  val server : Required<P>

  machine {
    client.f1() = server.f2()
  }
}

Some of the built-in functions in Coco, such as timer expiry events, also require their arguments to be side-effect free. The following component gives two examples of such events that violate this requirement:

@runtime(.MultiThreaded)
component InvalidC3 {
  val client : Provided<P>
  val server : Required<P>

  machine {
    var n : Int
    var d : Duration

    state S0 {
      after((d = milliseconds(20))) = abort()
      periodic(milliseconds(20)) = assert(server.f2())
    }
  }
}

The after timer expiry event has an argument that modifies the variable d, whereas the periodic one results in an assert with a call to f2() (which is not labelled as side-effect free) as its argument.