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 assigned references to static (i.e. non-member) functions and external functions that are deterministic. This means that it is not possible to assign a reference to a function that is defined within a state machine, or an external function with a body that includes the nondet expression.

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¶

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

where the expression is a simple expression, and can only be used as a field initialiser in components.

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¶

[«visibility»] [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.

For variable declarations at the top-level of a Coco module, the expressions must be simple ones.

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.

Private variables (denoted by the keyword private) can only be declared in component declarations, and can only be of non-verified types.

Static Constants¶

A static constant belongs to the declaration within which it is defined. Since these definitions are static, it is not necessary to create an instance of the enclosing type to access its value. In all cases, the static constant x can be referenced as C.x, where C is the enclosing type.

declarationStatic Constant¶

[«visibility»] static val «identifier» : «type» = «expression»

Static constants can be declared in enum, struct, port, component, state machine, and event state declarations. The following example illustrates the use of a static constant in a struct called Table:

enum Style {
  case Painted(red : Int, green : Int, blue : Int)
  case Oak
}

struct Table {
  static val kBase : Style = .Oak
  var size : Int
  var tableTop : Style
}

The static constant kBase in Table can simply be referenced as Table.kBase in other contexts, as illustrated in the following port example:

port P {
  function getTableBase() : Style

  machine {
    getTableBase() = Table.kBase
  }
}

The function getTableBase() will return the value Style.Oak.

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¶

[«visibility»] 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¶

[«visibility»] function «identifier»(«parameters») : «type»

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

For example:

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

Signals¶

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

declarationSignal¶

[«visibility»] 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¶

[«visibility»] enum «identifier» {
  «enum elements»
}

[«visibility»] «enum element» :=
  «enum case»
  | [mut | static] «function»
  | [mut | static] «external function»
  | «static constant»

«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. Member functions, including external ones, can be static, which means they are defined on the type, as opposed to an instance of the type. An example of a static function can be found in struct.

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¶

[«visibility»] struct «identifier» {
  «struct elements»
}

[«visibility»] «struct element» :=
  «field»
  | [mut | static] «function»
  | [mut | static] «external function»
  | «static constant»

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. Member functions, including external ones, can be static, which means they are defined on the type, as opposed to an instance of the type.

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

  static function initial() : Message = Message{ store = [0, 0], index = 0 }

  mut function reset() : Nil = {
    for i in range(0, size) {
      store[i] = 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.

The function initial() is an example of a static function, as it is defined on the type Message, as opposed to an instance of it. The following example illustrates how this function can be used to set the default value for a variable declaration:

var m : Message = Message.initial()

The struct 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¶

[«visibility»] 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¶

[«visibility»] 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.

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, and also allow users to provide information about these types for the purposes of verification.

declarationExternal Type¶

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

[«visibility»] «external type element» :=
  «static constant»
  | «variable declaration»
  | [mut | static] «external function»
  | [mut | static] «function»

where variable declarations must be of a type that has an instance of Verified, and can only be accessed by member functions.

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

By default, a user-defined external type is not defaultable. However, if the real implementation of the type in the target language is defaultable (for example, in C++, if the type is default-constructible), then its declaration can be labelled with with the @derive attribute, written as follows:

@derive(Default)
external type Data

Users can also specify that a custom external type is defaultable by declaring an instance of Default for that type. However, this approach is more restrictive as the trait instance can only use external functions, and the body of those functions must be simple.

A variable can be declared to be of some external type T. If the external type is not defaultable, then Slot or Optional of type T can be used instead.

By default, external types are not verified, and therefore no data about them is stored during verification.. However, users can some information about an external type in body of its declaration, in order to enable some verification to be carried out. This is an abstract specification, since it is only used for verification purposes, and no code is generated from it. For example:

@derive(Default)
external type Vector<T, val max : Int where 0 <= max> {
  var size_ : Bounded<0, max>

  mut external function clear() : Nil = {
    size_ = 0;
  }

  external function size() : Bounded<0, max> = size_

  mut external function pushBack(x : T) : Nil = {
    size_ = size_ + 1;
  }
}

This is an example of a Coco external type declaration for a vector. Although the contents of the vector are not verifiable, the size of the vector is and can therefore be used during verification. The variable size_ stores the current size of the vector, and is implicitly initialised with the value 0. It can be accessed via calls on the external type’s member functions, for example, the function clear() resets the value of size_ to 0. The following function testVector() illustrates how a variable of type Vector can be declared, and its member functions called:

function testVector() : Nil = {
  var store : Vector<Bool, 5>;
  assert(0 == store.size());
  store.pushBack(false);
  store.pushBack(false);
  assert(2 == store.size());
  store.clear();
  assert(0 == store.size());
}

This passes verification, which means that all assertions pass.

External types can be mapped to existing definitions elsewhere in the code using the @mapToType attribute, for example:

@CPP.mapToType("std::vector<{0}>", .ConstReference, .System("vector"))
external type Vector<T, val max : Int where 0 <= max> {

This is an example illustrating how Vector can be mapped to an existing definition in C++.

Member functions can also be mapped to their implementations using the @mapToMember attribute, as illustrated in the following example where the target language is C++:

  @CPP.mapToMember("clear")
  mut external function clear() : Nil = {
    size_ = 0;
  }

In addition to making it easier to integrate the generated code into the rest of the system, Coco’s external type is a powerful tool for allowing partial verification involving variables of external types that are not verifiable by default.

External Constants¶

Constants defined outside of Coco can be referenced in Coco by declaring them as external constants.

declarationExternal Constant¶

[«visibility»] external val «identifier» : «type» = «expression»

External constants must be declared with a value, and are 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.

External constants can be declared to be of an external type. For example:

external type DataPacketSize
external val packetSize : DataPacketSize = _

External constants of an external type must be initialised with the undefined expression (_) as illustrated above, unless the external type has a body, in which case it must be initialised with a value of the variable type declared in the external type’s body. For example:

external type BlockSize {
  var size_ : Bounded<0, 128>
}

external val defaultBlockSize : BlockSize = BlockSize{ size_ = 16 }

External constants can be labelled with the @mapToValue attribute in order to map them to their corresponding definition in the generated target language, as illustrated by the following example:

@CPP.mapToValue("cocotec::project::kTimeoutPeriod", .User("cocotec/constants.h"))
external val kTimeoutPeriod : Duration = _

In this example, the external constant kTimeoutPeriod is mapped to a constant value declared in C++.

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.

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. Coco supports two types of arrays called Array and SymmetricArray, each described in turn below.

The Array type is the standard and most commonly used one, where the size of the array is the actual size used for the verification and runtime. 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.

In contrast, SymmetricArray is a special array type that can only be used in implementation components to declare an array of provided ports, where the component treats each index of the array identically. They are written as follows:

  val client : SymmetricArray<Provided<P>, 100>

The variable client is a symmetric array of provided ports of type P. The size of the array (in this case, 100) is only relevant at runtime. For verification, Coco will automatically compute the minimum array size it needs to verify in order to guarantee that the component will work correctly for an array of any size greater than this minimum threshold. This allows the verification of components with a large number of provided ports that are treated symmetrically to be optimized. See Components with Symmetric Provided Ports for further details and examples.

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 used for an Array must evaluate to a value of a type that has an instance of Integer. In contrast, the subscript expression used for a SymmetricArray must of type SymmetricArrayIndex. This imposes certain restrictions on how values of this type are used, which are required to ensure soundness of the verification. See SymmetricArrayIndex for further details and examples.

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.

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>)
  case DataWithId(id : Int, msg : Int)
}

function unpackMessage(m : Message) : Int = {
  match (m) {
    .None => -1,
    .Data(d) => d,
    .DataWithId(id, d) if (id < 3) => d,
    _ => -1,
  }
}

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;
    },
  };
}