Standard Library

Coco has a small standard library over a number of modules that includes a number of built-in collection types and utility functions. The individual modules are documented below.

Base Module

The Base module is implicitly imported unqualified into every module.

Basic Types

external type Bool

Represents a boolean.

trait instance Default(Bool)

The default value for Bool is false.

trait instance Eq(Bool)
trait instance Verified(Bool)
trait instance Log(Bool)
external constant true : Bool
external constant false : Bool
external type Bounded<val first : T, val last : T, T = Int where Integer<T>, Verified<T>, first <= last>

Represents an integer value in the range first <= value <= last. For example, Bounded<0, 1, Int> is an integer that can be assigned to either 0 or 1. It is a dynamic error to store a value outside of the permitted range.

When first and last are simple literals, then bounded literal initialisers are checked against them, and are rejected as a static error if they out of bounds.

Contrary to the former type BoundedInt (now deprecated), the upper bound last is included in the range of Bounded.

Bounded has the following static constants:

external constant First : Bounded<first, last, T>
external constant Last : Bounded<first, last, T>

The bounds of a Bounded type are accessible by using the static constants First and Last. For example, the following variable declaration is initialised with the upper bound of the Bounded type:

val x : Bounded<0, 5> = Bounded<0, 5>.Last

The static constants can only be accessed via the type name, and not via values of types. For example, the following variable declaration is valid:

type T = Bounded<0, 5>
val y : T = .Last

However, the following use of Last is not valid:

val z : T = y.Last

The recommended approach for declaring and accessing the lower and upper bounds for a Bounded type is to use the static constants First and Last, rather than defining the bounds as independent constants as follows:

val upper : Int = 10
type DeviceId = Bounded<5, upper>

The constant variable upper is of type Int, and will only work in contexts requiring an Int. In contrast, if DeviceId is declared as follows:

type DeviceId = Bounded<5, 10>

then the upper bound can be accessed via .Last. This is not only more succinct, but it also benefits from the fact that .Last can be used in contexts requiring either a DeviceId or an Int type, since Bounded is implicitly convertible to Int.

trait instance Default<val first : T, val last : T, T where Integer<T>, Verified<T>, first <= last>(Bounded<first, last, T>)

The default value of Bounded<first, last, T> is first.

trait instance Eq<val first : T, val last : T, T where Integer<T>, Verified<T>, first <= last>(Bounded<first, last, T>)
trait instance Ord<val first : T, val last : T, T where Integer<T>, Verified<T>, first <= last>(Bounded<first, last, T>)
trait instance Cast<T1, val first : T2, val last : T2, T2 where PrimitiveInteger<T1>, Verified<T1>, PrimitiveInteger<T2>, Verified<T2>, Ord<T2>, Cast<T1, T2>, first <= last>(T1, Bounded<first, last, T2>)

Allows casts from any integer type.

trait instance Cast<val first : T1, val last : T1, T1, T2 where PrimitiveInteger<T1>, Verified<T1>, Ord<T1>, PrimitiveInteger<T2>, Verified<T2>, Cast<T1, T2>, first <= last>(Bounded<first, last, T1>, T2)

Allows casts to any integer type.

trait instance ImplicitCast<val first : T, val last : T, T where Integer<T>, Verified<T>, first <= last>(Bounded<first, last, T>, T)

Allows implicit casts to the underlying integer type.

trait instance Cast<val first : T1, val last : T1, T1, T2 where Cast<T1, T2>, Verified<T1>, PrimitiveInteger<T1>, Ord<T1>, Verified<T2>, PrimitiveInteger<T2>, first <= last>(Bounded<first, last, T1>, NonVerified<T2>)

Allows cast to any non-verified integer type.

trait instance ImplicitCast<val first : T, val last : T, T where PrimitiveInteger<T>, Verified<T>, Ord<T>, first <= last>(Bounded<first, last, T>, NonVerified<T>)

Allows implicit cast to a non-verified version of the underlying type.

trait instance Cast<val first1 : T1, val last1 : T1, T1, val first2 : T2, val last2 : T2, T2 where PrimitiveInteger<T1>, Verified<T1>, Ord<T1>, PrimitiveInteger<T2>, Verified<T2>, Ord<T2>, Cast<T1, T2>, first1 <= last1, first2 <= last2>(Bounded<first1, last1, T1>, Bounded<first2, last2, T2>)

Allows casts to bounded integers of different sizes and different underlying types.

trait instance Num<val first : T, val last : T, T where Integer<T>, Verified<T>, first <= last>(Bounded<first, last, T>)
trait instance Integer<val first : T, val last : T, T where Integer<T>, Verified<T>, first <= last>(Bounded<first, last, T>)
trait instance Negatable<val first : T, val last : T, T where Integer<T>, Verified<T>, first <= last>(Bounded<first, last, T>)
trait instance Verified<val first : T, val last : T, T where Integer<T>, Verified<T>, first <= last, Verified<T>>(Bounded<first, last, T>)
trait instance Log<val first : T, val last : T, T where PrimitiveInteger<T>, Verified<T>, Ord<T>, Log<T>, first <= last>(Bounded<first, last, T>)
type BoundedInt<val lower : Int, val upper : Int where lower <= (upper - 1)> = Bounded<lower, upper - 1, Int>

Represents a bounded integer value in the range lower <= value < upper. For example, BoundedInt<0, 2> is an integer that can be assigned to either 0 or 1. It is a dynamic error to store a value outside of the permitted range.

Note

BoundedInt has been removed in Coco 1, and has been replaced by the type Bounded.

BoundedInt is a type alias of Bounded, where the upper bound is a symbolic binary type expression, namely upper - 1. Since this bound is not a simple literal, Coco does not check whether bounded literal initialisers are out of bounds.

external type Char
trait instance Default(Char)

The default value for Char is ‘0’.

external type Duration

Specifies the time interval used in a timer transition.

trait instance Default(Duration)

The default value for Duration is seconds(0).

trait instance NonVerifiedEq(Duration)
trait instance Log(Duration)

Instances of Duration can be constructed using the following functions:

external function microseconds(t : NonVerified<Int>) : Duration

Creates a Duration of t microseconds.

external function milliseconds(t : NonVerified<Int>) : Duration

Creates a Duration of t milliseconds.

external function seconds(t : NonVerified<Int>) : Duration

Creates a Duration of t seconds.

external function minutes(t : NonVerified<Int>) : Duration

Creates a Duration of t minutes.

external function hours(t : NonVerified<Int>) : Duration

Creates a Duration of t hours.

external type EventuallyAssumption

EventuallyAssumption is a special type specifically used in parameters of @eventually and @satisfiesEventually attributes in order to specify a collection of transitions that are part of a single eventually constraint.

See also

Spanning Multiple Transitions section for further details and examples.

external type Int

A 32-bit signed integer that can express values in the range 2-31 to 231 - 1.

trait instance Cast(Int, Int)
trait instance Cast(Int, UInt)
trait instance Cast(NonVerified<Int>, NonVerified<Int>)
trait instance Cast(NonVerified<Int>, NonVerified<UInt>)
trait instance Default(Int)

The default value for Int is 0.

trait instance Eq(Int)
trait instance Integer(Int)
trait instance Integer(NonVerified<Int>)
trait instance Log(Int)
trait instance Negatable(Int)
trait instance Negatable(NonVerified<Int>)
trait instance Num(Int)
trait instance Num(NonVerified<Int>)
trait instance Ord(Int)
trait instance Verified(Int)
external type UInt

A 32-bit unsigned integer.

trait instance Cast(UInt, Int)
trait instance Cast(UInt, UInt)
trait instance Cast(NonVerified<UInt>, NonVerified<Int>)
trait instance Cast(NonVerified<UInt>, NonVerified<UInt>)
trait instance Default(UInt)
trait instance Eq(UInt)
trait instance Integer(NonVerified<UInt>)
trait instance Integer(UInt)
trait instance Log(UInt)
trait instance Num(UInt)
trait instance Num(NonVerified<UInt>)
trait instance Ord(UInt)
trait instance Verified(UInt)
external type Nil

This is an empty type that is normally used to denote the return value of a function that has no return value (i.e. it is like void in other languages).

external constant nil : Nil
trait instance Log(Nil)
trait instance Verified(Nil)
external type NonVerified<T where Verified<T>>

Requests a non-verified version of a verified type.

trait instance Eq<T where Eq<T>, Verified<T>>(NonVerified<T>)
trait instance Cast<T where Verified<T>>(T, NonVerified<T>)
trait instance Default<T where Default<T>, Verified<T>>(NonVerified<T>)
trait instance ImplicitCast<T where Verified<T>>(T, NonVerified<T>)
trait instance Log<T where Verified<T>, Log<T>>(NonVerified<T>)
trait instance NonVerifiedEq<T where Eq<T>, Verified<T>>(NonVerified<T>)

Non-verified types are comparable for equality if their underlying types are.

trait instance NonVerifiedOrd<T where Ord<T>, Verified<T>>(NonVerified<T>)

Non-verified types are comparable for ordering if their underlying types are.

external type Provided<Port where IsPort<Port>>
external type Required<Port where IsPort<Port>>
external type Range

Represents an integer range so that it can be iterated over within a for loop.

trait instance Iterable(Range)
trait instance Verified(Range)
external function range(lowerBound : Int, upperBound : Int) : Range

This creates a Range object that is suitable for iterating over the integers x such that lowerBound <= x < upperBound. For example, the following sums all the integers between 1 and 10 (including 1 but excluding 10):

var sum = 0
for x : Int in range(1, 10) {
  sum = sum + x;
}
external type String
trait instance Default(String)

The default value of String is “”.

trait instance Log(String)
external type SymmetricArrayIndex
trait instance Eq(SymmetricArrayIndex)
trait instance Log(SymmetricArrayIndex)
trait instance Verified(SymmetricArrayIndex)

SymmetricArrayIndex is specifically used as the type of the index of a SymmetricArray. It can only be used within state machines of implementation components, and cannot be used inside complex types, such as structs. The following example illustrates the use of SymmetricArrayIndex in a component state machine:

component C {
  val client : SymmetricArray<Provided<P>, 100>

  machine {
    state Idle {
      client[val i].begin() = {
        setNextState(Running(i));
        return true;
      }
    }

    state Running(i : SymmetricArrayIndex) {
      client[val j | j != i].begin() = {
        return false;
      }
      after(seconds(1)) = {
        client[i].done();
        setNextState(Idle);
      }
    }
  }
}

Symmetric arrays cannot be indexed by a specific value, for example, client[0] is not valid Coco.

Container Types

external type Array<T, val size : Int where 0 <= size>

Represents a fixed-size array of size size containing items of type T. For example, Array<Int, 5> is an array of five integers.

trait instance Default<T, val size : Int where Default<T>, 0 <= size>(Array<T, size>)

An array is defaultable if its underlying type is also defaultable. If defaultable, then each element of the array is initialised to the default value for its type.

trait instance Eq<T, val size : Int where Eq<T>, 0 <= size>(Array<T, size>)

An array is comparable for equality if the underlying type is also comparable for equality.

trait instance Iterable<T, val size : Int where 0 <= size>(Array<T, size>)
trait instance Log<T, val size : Int where Log<T>, 0 <= size>(Array<T, size>)
trait instance NonVerifiedEq<T, val size : Int where NonVerifiedEq<T>, 0 <= size>(Array<T, size>)
trait instance NonVerifiedOrd<T, val size : Int where NonVerifiedOrd<T>, 0 <= size>(Array<T, size>)
trait instance Ord<T, val size : Int where Ord<T>, 0 <= size>(Array<T, size>)

An array can be ordered if the underlying type can also be ordered.

trait instance Verified<T, val size : Int where 0 <= size>(Array<T, size>)
external type List<T>

This data type in not intended for general use in Coco programs. It is specifically intended to enable the declaration of built-in Coco enum signatures that have variadic parameters, such as the list of header files specified in CPP.mapToType and CPP.mapToValue attributes.

trait instance Cast<T, val size : Int where 0 <= size>(Array<T, size>, List<T>)
trait instance ImplicitCast<T, val size : Int where 0 <= size>(Array<T, size>, List<T>)
enum Optional<T>

Optional<T> can be used in situations where a value may or may not be present, and has the following enum cases:

case None

Represents the case where a value is not present.

case Some(value : T)

Represents the case where a value of type T is present.

The default value is None.

Consider the following example:

external function getData() : Optional<Int> =
  nondet {
    Optional.None<Int>,
    Optional.Some(0),
    Optional.Some(1),
  }

val size : Int = 5

type Message = Array<Int, size>

function update(msg : &out Message) : Bool = {
  var result : Bool = true;
  for index in range(0, size) {
    match (getData()) {
      Optional.None => {
        msg[index] = -1;
        result = false;
      },
      Optional.Some(value) => {
        msg[index] = value;
      },
    }
  }
  return result;
}

The return type of the external function getData() is Optional<Int>, and the function body specifies that it will nondeterministically return either Optional.None, Optional.Some(0), or Optional.Some(1).

The main function update(msg : &out Message) steps through msg, and for each array element, assigns the value returned from calling getData(). In the event that Optional.None is returned, -1 is assigned as the value in the corresponding array element (msg[index]). The function returns true in the case where msg only contains actual values received from getData(), and false otherwise.

The enum Optional<T> also has the following builtin member functions:

function hasValue() : Bool

If the value is of the form Some(v) where v is a value of type T, then this function returns true, otherwise it returns false.

function value() : T

This function assumes that the value is of the form Some(v) where v is a value of type T, and returns v. It is a dynamic error to call this function with the value None.

function valueOr(default : T) : T

If the value is of the form Some(v), then this function returns v, otherwise it returns the value of default.

function reset() : Nil

This is a mutating function that resets the value to None.

Consider the following simple example functions to illustrate the use of these member functions:

function hasData1() : Bool = {
  var data : Optional<Int>;
  data = Optional.Some(3);
  return data.hasValue();
}

function hasData2() : Bool = {
  var data : Optional<Int>;
  data = Optional.Some(8);
  data.reset();
  return data.hasValue();
}

The function hasData1() will always return true, because the variable data is assigned the value Optional.Some(3), and therefore the member function data.hasValue() returns true. In contrast, the function hasData2() will always return false, because after the variable data is assigned a value, and before the function returns, data is reset to having no value as a result of calling data.reset().

See also

Try operator expression.

enum Result<T, E>

Result<T, E> can be used to represent functions that might fail, and if they do fail, return an error. Coupled with the try operator, which enables a function to return early when one of the functions it calls return an error, this is the recommended approach for error handling in Coco.

Result<T, E> has the following enum cases:

case Ok(value : T)

Represents the successful case with a value of type T.

case Error(error : E)

Represents the error case with an error code value error of type T.

Result<T, E> is labelled with the attribute @mustUse, which means that Coco will give an error if the value of an expression e of type Result is ignored. The following example illustrates the importance of this attribute when using Result<T, E> and the try operator for error handling:

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

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

In this example, if check(x)? evaluates to .Error(nil), then the function square() will immediately return early with the value .Error(nil). Since the builtin type Result<T, E> is labelled with @mustUse, Coco ensures that ? is correctly used, and this early return cannot be ignored.

Result<T, E> also has the following builtin member functions:

function discard() : Nil

This function discards the value, and returns nil.

function error() : E

This function assumes that the value is of the form Error(e) where e is a value of type E, and returns e. It is a dynamic error to call this function with a value of the form Ok(v).

function isError() : Bool

If the value is of the form Error(e), then this function returns true, otherwise it returns false.

function isOk() : Bool

If the value is of the form Ok(v), then this function returns true, otherwise it returns false.

function value() : T

This function assumes that the value is of the form Ok(v) where v is a value of type T, and returns v. It is a dynamic error to call this function with a value of the form Error(e).

function valueOr(default : T) : T

If the value is of the form Ok(v), then this function returns v, otherwise it returns the value of default.

See also

Try operator expression.

external type Slot<T>

The type Slot<T> can be used to enable some verification even on non-verified types, such as external types. In particular, if a variable is declared to be of type Slot<T>, then the verification will instead check that the slot is only read when a value has been stored in it. It can therefore be used to check that a non-verified type is accessed correctly by the program, even if the actual value is not available.

Slot<T> has the following static constants:

external constant Valid : Slot<T>

Represents the case where the value is valid, for example because it has been initialised or written to.

external constant Invalid : Slot<T>

Represents the case where the value is not valid, because it has not been written to, or has not been explicitly invalidated. During verification, all variables of type Slot<T> are invalid by default.

Slot also has the following builtin member functions:

external function isValid() : Bool

Returns true if the value is valid, and false otherwise.

external function isInvalid() : Bool

Returns true if the value is invalid, and false otherwise.

external function initialise() : Nil

This is a mutating function that sets the value to being valid.

external function invalidate() : Nil

This is a mutating function that sets the value to being invalid.

During verification, Coco stores whether variables of type Slot<T> hold a valid value or not, without knowing or storing the actual value itself. These variables can be set to being valid or invalid via the static constants .Valid and .Invalid respectively. In the generated code, Slot<T> is replaced by T. By default, all instances of Slot<T> are invalid unless specified otherwise. The verification will find any attempts to read or load an invalid value, and provide a counterexample to highlight the error.

For example, consider the following component state machine:

external type Data

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

  machine {
    val v : Slot<Data>

    client.getData() = v
  }
}

where the return type of getData() is Data, which is declared as an external type. This component fails verification with a runtime error because client.getData() is called and is trying to return v, which has not been initialised or assigned a value. In contrast, consider the following example:

external type Data

external function getUpdate(d : &out Data) : Nil = {
  d = _;
}

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

  machine {
    client.getData() = {
      var v : Slot<Data>;
      getUpdate(&v);
      return v;
    }
  }
}

In this example, when client.getData() is called, it is guaranteed to return a valid value for v, because of the call on the external function getUpdate(&v) before it returns.

The external function getUpdate(_ : &out Data) is guaranteed to write an arbitrary but valid Data into the variable, because Coco requires all out parameters are written to, and therefore assumes the runtime code declaring this function will write a valid value. As a result, when a reference to a Slot<T> is passed to a function taking a T, the slot will be valid by the time the function returns.

In contrast, the following example illustrates the use of slots in an external function that does not guarantee that all &out parameters are written to by the time it returns:

external type Data

external function maybeGetUpdate(data : &out Slot<Data>) : Bool =
  nondet {
    {
      data = .Valid;
      return true;
    },
    {
      data = .Invalid;
      return false;
    },
  }

This function has an &out parameter data of type &out Slot<Data>, which means that, unlike the previous example, the value of data may be valid or invalid. The body of the function defines its interface, and states that it may or may not have written a valid value to data by the time it returns, the decision of which is made nondeterministically. If it has written a valid value, then the function returns true, otherwise it returns false.

See also

Verification section for an example of how slots can used in structs, and how the verification checks that a component does not return values (involving slots) that are not allowed by its provided port.

trait instance Default<T>(Slot<T>)

Slots can be defaulted even if T is not defaulted, since the verification checks that the value can never be used when uninitialised.

trait instance NonVerifiedEq<T where Eq<T>>(Slot<T>)
trait instance NonVerifiedEq<T where NonVerifiedEq<T>>(Slot<T>)

Slots can be compared for equality, but only in the generated code rather than during verification.

trait instance Verified<T>(Slot<T>)
trait instance Cast<T where Verified<T>>(Slot<T>, NonVerified<T>)

Allows conversions of valid slots to non-verified T.

trait instance Cast<T1, T2 where Cast<T1, T2>, PrimitiveInteger<T1>, Verified<T1>, Verified<T2>, PrimitiveInteger<T2>>(Slot<T1>, NonVerified<T2>)

Allows cast to any non-verified integer type.

trait instance ImplicitCast<T where Verified<T>>(Slot<T>, NonVerified<T>)
trait instance Cast<T where !Verified<T>>(Slot<T>, T)

Allows conversions of valid slots to non-verified T.

trait instance ImplicitCast<T where !Verified<T>>(Slot<T>, T)
trait instance Cast<T where Verified<T>>(NonVerified<T>, Slot<T>)

Assumes a value of type NonVerified<T> points to a well-formed value of type T.

trait instance ImplicitCast<T where Verified<T>>(NonVerified<T>, Slot<T>)
trait instance Cast<T1, T2 where Cast<T1, T2>, Verified<T1>, PrimitiveInteger<T1>, PrimitiveInteger<T2>, Verified<T2>>(NonVerified<T1>, Slot<T2>)

Allows conversions of any non-verified integer type to a slot type holding any integer type.

trait instance Cast<T>(T, Slot<T>)

Assumes a value of type T points to a well-formed value of type T.

trait instance ImplicitCast<T>(T, Slot<T>)
trait instance Cast<T where Verified<T>>(T, Slot<NonVerified<T>>)

Assumes a value of type T points to a well-formed value of type T.

trait instance ImplicitCast<T where Verified<T>>(T, Slot<NonVerified<T>>)
trait instance Cast<T1, T2 where Cast<T1, T2>, PrimitiveInteger<T1>, Verified<T1>, PrimitiveInteger<T2>, Verified<T2>>(T1, Slot<NonVerified<T2>>)

Allows conversions of any integer type to a slot type holding any non-verified integer type.

trait instance LValueCast<T where !Verified<T>>(T, Slot<T>)

Assumes that writing to a value of type T just writes a valid value.

trait instance LValueCast<T where Verified<T>>(NonVerified<T>, Slot<T>)

Assumes that writing to a value of type T just writes a valid value.

external type SymmetricArray<T, val size : Int where 0 <= size>

Represents an array of provided ports that will be treated symmetrically by the component, in that the component treats each index of the array identically. The first parameter T is the type of the port, and must be of the form Provided<T>. The second parameter size is the size of the array, which 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.

Unlike normal arrays, SymmetricArray may only be used for provided ports in implementation components. Further, it can only be indexed using the special type SymmetricArrayIndex, as illustrated in the following example:

port LockableResource {
  function lock() : Bool
  function unlock() : Nil
  function action() : Nil
  outgoing signal finished()

  machine {
    state Unlocked {
      lock() = nondet {
        {
          return false;
        },
        {
          setNextState(Locked.Ready);
          return true;
        },
      }
    }

    state Locked {
      unlock() = setNextState(Unlocked)

      state Ready {
        action() = setNextState(Running)
      }

      state Running {
        spontaneous = {
          finished();
          setNextState(Ready);
        }
      }
    }
  }
}
trait instance Verified<T, val size : Int where 0 <= size>(SymmetricArray<T, size>)

See also

Components with Symmetric Provided Ports section for further details and examples.

Traits

trait Cast<From, To>

This trait is used to implement explicit casts between different types. Types that satisfy this trait must implement the following cast function:

function cast(from : From) : To

The cast function could call abort if the cast is not supported at runtime, for example when casting from integers to enums, and passing an integer that is out of range.

trait ImplicitCast<From, To where Cast<From, To>>
trait LValueCast<From, To where Cast<To, From>, !Verified<From>>
function cast(from : From) : To
trait Default<T>

This trait is satisfied by types that have implemented an instance of the default function:

function default() : T

Returns the default value for type T.

This is used in variable declarations without initialisers (for example, var x : T), and when the default constructor is called (e.g. T()).

trait Eq<T>

This trait is satisfied by types that are comparable for equality. There are two functions that instances must implement. This is used internally to implement the == and != operators and takes precedence over NonVerifiedEq. You should not implement both Eq and NonVerifiedEq for the same type.

function equals(first : T, second : T) : Bool

Returns true iff the two arguments are considered equal. Implements the equality comparison operator (i.e. ==).

function notEquals(first : T, second : T) : Bool

Returns true iff the two arguments are considered not equal. Implements the inequality comparison operator (i.e. !=).

trait NonVerifiedEq<T>

This trait is satisfied by types that are comparable for equality only at runtime, not during verification. There are two functions that instances must implement. This is used internally to implement the == and != operators but only if Eq is not also defined. You should not implement both Eq and NonVerifiedEq for the same type.

function equals(first : T, second : T) : NonVerified<Bool>

Returns true iff the two arguments are considered equal. Implements the equality comparison operator (i.e. ==).

function notEquals(first : T, second : T) : NonVerified<Bool>

Returns true iff the two arguments are considered not equal. Implements the inequality comparison operator (i.e. !=).

trait Integer<T where Num<T>>

This trait is for integral numerical types.

trait IsPort<P>
type AnySignal

This is the type of any signal, without its parameters.

type Signal

This is the type of any outgoing signal, with its parameters.

See also

Port declaration.

trait Iterable<ContainerType>

Represents a container of type containerType that contains items that can be iterated over using a for loop.

It is a static error for a user to create instances of Iterable.

type ElementType

The type of each individual element of the container.

trait Log<T>
Standard:1.2

This trait is used to specify how a value can be converted into a string. It is primarily useful when constructing format strings, or when using value-based logging.

function format(value : T, formatter : &mut Formatter) : Nil

Coco has builtin instances of Log for all common types. For Coco-defined types, they can be labelled with the @derive(Log) attribute, which is supported for enums, as illustrated below:

@derive(Log)
enum Colour {
  case Red
  case Yellow
  case Blue
}

function primaryToString(colour : Colour) : String = $"{colour} is a primary colour."

The following example illustrates how the fields in a struct can be referenced in format strings:

@derive(Eq, Log)
struct Order<I, R> {
  var id : I
  var ref : R

  static function create(id : I, ref : R) : Order<I, R> = Order<I, R>{ id = id, ref = ref }
}

function orderToString<I, R where Log<I>, Log<R>>(order : Order<I, R>) : String =
  $"My id is {order.id} and my order reference is {order.ref}."
external type Formatter
Standard:1.2

A Formatter provides methods to write primitive types to a buffer, where the actual buffer is abstracted. For example, the writeBool method could be used to write a single boolean to the Formatter’s buffer.

This type should only be used when defining instances of the Log trait.

external function writeBool(value : Bool) : Nil
external function writeInt(value : Int) : Nil
external function writeString(value : String) : Nil
external function writeUInt(value : UInt) : Nil
external function logWriteBlank() : Nil
external function logBeginArray() : ArrayLogFormatter
external function logEnum(caseName : String) : Nil
external function logBeginEnum(caseName : String, positional : Bool) : EnumLogFormatter
external function logBeginStruct() : StructLogFormatter
external function logExternalValue(value : String) : Nil
external function logBeginExternalValue() : Nil
external function logFinishExternalValue() : Nil

Formatter also utilises several helper types:

external type ArrayLogFormatter
Standard:1.2
external function beginEntry() : Nil
external function finish() : Nil
external type EnumLogFormatter
Standard:1.2
external function beginField(name : String) : Nil
external function finish() : Nil
external type StructLogFormatter
Standard:1.2
external function beginField(name : String) : Nil
external function finish() : Nil

Consider the following example of a simple struct:

struct RGBColour {
  var red : Int
  var green : Int
  var blue : Int
}

This custom type can be labelled with @derive(Log) to tell Coco to automatically derive the trait instance. The following example is an equivalent manually implemented trait instance for RGBColour, to illustrate how the helper functions above can be used in cases where trait instances cannot be automatically derived:

instance Log(RGBColour) {
  function format(value : RGBColour, formatter : &mut Formatter) : Nil = {
    var sf = formatter.logBeginStruct();
    sf.beginField("red");
    Log.format(value.red, formatter);
    sf.beginField("green");
    Log.format(value.green, formatter);
    sf.beginField("blue");
    Log.format(value.blue, formatter);
    sf.finish();
  }
}
trait Ord<T where Eq<T>>

This trait is satisfied by types that can be ordered in some way. There are four functions that instances must implement. This is used internally to implement the <, <= etc operators, and takes precedence over NonVerifiedOrd. You should not implement both Ord and NonVerifiedOrd for the same type.

function lessThan(first : T, second : T) : Bool
function lessThanEquals(first : T, second : T) : Bool
function greaterThan(first : T, second : T) : Bool
function greaterThanEquals(first : T, second : T) : Bool
trait NonVerifiedOrd<T where NonVerifiedEq<T>>

This trait is satisfied by types that can be ordered in some way, but where the ordering is only definable at runtime, not during verification. There are four functions that instances must implement. This is used internally to implement the <, <= etc operators but only if Ord is not also defined. You should not implement both Ord and NonVerifiedOrd for the same type.

function lessThan(first : T, second : T) : NonVerified<Bool>
function lessThanEquals(first : T, second : T) : NonVerified<Bool>
function greaterThan(first : T, second : T) : NonVerified<Bool>
function greaterThanEquals(first : T, second : T) : NonVerified<Bool>
trait Num<T>

This trait is satisfied by numerical types that implement instances of the following functions:

function divide(first : T, second : T) : T
function minus(first : T, second : T) : T
function plus(first : T, second : T) : T
function times(first : T, second : T) : T
trait Negatable<T where Num<T>>

This trait is satisfied by numerical types that implement an instance of the following function:

function negate(arg : T) : T
trait Remainder<T where Num<T>>

This trait is satisfied by numerical types that implement an instance of the following remainder function:

function remainder(first : T, second : T) : T
trait Verified<T>

General Functions

external function abort() : Div

If this function is ever executed then it is a dynamic error. For example:

function f(x : Bool) : Nil = if (x) process(x) else abort()

The above handles x if it evaluates to true, and calls abort() otherwise.

Note

The function abort() differs from illegal: if abort() is ever called, then this is a fatal error. In contrast, declaring that an event is illegal is not an error, providing that the ports and components agree.

See also

The illegal handler.

external function assert(@noSideEffects pred : Bool) : Nil
Parameter pred:a side-effect free predicate that is checked by the assertion.
Type pred:Bool

If the given predicate evaluates to false then this is a dynamic error. This is equivalent to:

if (!pred) { abort(); }
external function assert(@noSideEffects pred : Bool, message : String) : Nil
Parameter pred:a side-effect free predicate that is checked by the assertion.
Type pred:Bool
external function runtimeAbort() : Nil

This appears in the generated code only, and is therefore ignored by the verification. It is equivalent to abort(), and is intended for specifying “can’t happen” situations in the program, which, if they ever occur at runtime, should terminate program execution.

See also

The function abort().

external function runtimeAssert(@noSideEffects pred : NonVerified<Bool>) : Nil
Parameter pred:a side-effect free predicate that is checked by the assertion.
Type pred:Bool

This appears in the generated code equivalent to:

if (!pred) { abort(); }

This statement is ignored by verification and in contrast with the assert() function, it never causes a dynamic error. This is intended for use in specifying “can’t happen” situations in the model, which, if they ever occur at runtime, should terminate program execution.

See also

The function assert(pred : Bool).

Internal Functions

The following are all functions that are internal to the implementation of Coco. Users will not normally need to use these functions unless attempting to customise the code generation process.

Implements &&:

external function logicalAnd(first : Bool, second : Bool) : Bool
external function logicalAnd(first : NonVerified<Bool>, second : NonVerified<Bool>) : NonVerified<Bool>

Implements !:

external function logicalNot(first : Bool) : Bool
external function logicalNot(first : NonVerified<Bool>) : NonVerified<Bool>

Implements ||:

external function logicalOr(first : Bool, second : Bool) : Bool
external function logicalOr(first : NonVerified<Bool>, second : NonVerified<Bool>) : NonVerified<Bool>

Vector Module

Note

The Vector module has been deprecated as of Coco language version 1.2, please use Vector2 instead.

Coco includes a builtin vector module, called Vector.coco, which can be accessed by importing it in the usual way. This module defines the following four vectors, starting from the least to the greatest potential impact on the verification time:

  • NonVerifiedVector, which represents a vector with no verifiable properties, and will therefore have the least impact on verification performance.
  • BoundedVector, which represents a vector with a Bounded verifiable size, but where the contents is not verified.
  • UnboundedVector, which represents a vector with an unbounded verifiable size of type UInt, but where the contents is not verified. If the maximum possible size of the vector is known, then BoundedVector is recommended to be used instead for optimal verification performance.
  • VerifiedVector, which represents a vector where the size and contents are verified. This vector will have the greatest impact on the verification, and should therefore be used with caution.

Each vector type is summarised in more detail below.

external type NonVerifiedVector<T where !Verified<T>>
Standard:1.1

Represents a vector type with no verifiable properties. When defaulted, its initial capacity is implementation dependent. The member function createWithCapacity can be used to specify its initial capacity.

It has the following builtin member functions:

external function createWithCapacity(capacity : NonVerified<UInt>) : NonVerifiedVector<T>

Creates a non-verified vector with a specified initial capacity.

external function reserve(capacity : NonVerified<UInt>) : Nil

Reserves a specified capacity in the vector to make sure it is sufficient for a given number of elements.

external function clear() : Nil

Clears the contents of the vector. The vector is empty after this operation.

external function size() : NonVerified<UInt>

Returns the current size of the vector, namely the number of elements held by the vector.

external function empty() : NonVerified<Bool>

Returns true if the vector is currently empty, and false otherwise.

external function push(element : T) : Nil

Adds element on to the end of the vector, incrementing its size by 1.

external function pop() : Result<T, Nil>

Removes the last element in the vector, decrementing its size by 1.

external function get(pos : NonVerified<UInt>) : Result<T, Nil>

Returns the element stored in the position pos.

external function set(pos : NonVerified<UInt>, element : T) : Result<Nil, Nil>

Sets the value at position pos to element.

external function insert(pos : NonVerified<UInt>, element : T) : Result<Nil, Nil>

Inserts the value element at the given position pos, incrementing the vector’s size by 1. The function insert(size(), element) is equivalent to push(element).

external function remove(pos : NonVerified<UInt>) : Result<Nil, Nil>

Removes the element stored in position pos, decrementing the vector’s size by 1. The function remove(size() - 1) is equivalent to pop().

The NonVerifiedVector type implements the following trait instances:

trait instance Default<T where !Verified<T>>(NonVerifiedVector<T>)

Non-verified vectors can always be defaulted, even if the element type T is not defaultable. The vector’s size defaults to 0.

trait instance NonVerifiedEq<T where !Verified<T>>(NonVerifiedVector<T>)

Non-verified vectors can be compared for equality, but only in the generated code.

external type BoundedVector<T, val maxSize : UInt where !Verified<T>, 0 <= maxSize>
Standard:1.1

Represents a vector with a verifiable size, where a maximum possible size maxSize is specified. The contents of the vector are not verified. When the vector is defaulted, its initial capacity is implementation dependent; the builtin external member function createWithCapacity can be used to specify its initial capacity.

It has the following builtin member functions:

external function createWithCapacity(capacity : Bounded<0, maxSize, UInt>) : BoundedVector<T, maxSize>

Creates a bounded vector with an initial size of capacity.

external function reserve(capacity : Bounded<0, maxSize, UInt>) : Nil

Reserves a specified capacity in the vector to make sure it is sufficient for a given number of elements.

external function clear() : Nil

Clears the contents of the vector. The vector is empty after this operation.

external function size() : Bounded<0, maxSize, UInt>

Returns the current size of the vector, namely the number of elements held by the vector.

external function empty() : Bool

Returns true if the vector is currently empty, and false otherwise.

external function push(element : T) : Nil

Adds element on to the end of the vector, incrementing its size by 1.

external function pop() : T

Removes the last element in the vector, decrementing its size by 1.

external function get(pos : Bounded<0, maxSize - 1, UInt>) : T

Returns the element stored in the position pos.

external function set(pos : Bounded<0, maxSize - 1, UInt>, element : T) : Nil

Sets the value at position pos to element.

external function insert(pos : Bounded<0, maxSize - 1, UInt>, element : T) : Nil

Inserts the value element at the given position pos, incrementing the vector’s size by 1. The function insert(size(), element) is equivalent to push(element).

external function remove(pos : Bounded<0, maxSize - 1, UInt>) : Nil

Removes the element stored in position pos, decrementing the vector’s size by 1. The function remove(size() - 1) is equivalent to pop().

The BoundedVector type implements the following trait instances:

trait instance Default<T, val maxSize : UInt where !Verified<T>, 0 <= maxSize>(BoundedVector<T, maxSize>)

A bounded vector can always be defaulted, even if the element type T is not defaultable. A vector’s size defaults to 0.

trait instance NonVerifiedEq<T, val maxSize : UInt where !Verified<T>, 0 <= maxSize>(BoundedVector<T, maxSize>)

Bounded vectors can be compared for equality, but only in the generated code.

external type UnboundedVector<T where !Verified<T>>
Standard:1.1

Represents a vector type with an unbounded size that is verified. The contents of the vector are not verified. When this vector type is defaulted, its initial capacity is implementation dependent. The member function createWithCapacity can be used to specify its initial capacity. If the maximum possible size of the vector is known, then BoundedVector is recommended to be used instead for optimal verification performance.

It has the following builtin member functions:

external function createWithCapacity(capacity : UInt) : UnboundedVector<T>

Creates an unbounded vector with an initial specified capacity.

external function reserve(capacity : UInt) : Nil

Reserves a specified capacity in the vector to make sure it is sufficient for a given number of elements.

external function clear() : Nil

Clears the contents of the vector. The vector is empty after this operation.

external function size() : Int

Returns the current size of the vector, namely the number of elements held by the vector.

external function empty() : Bool

Returns true if the vector is currently empty, and false otherwise.

external function push(element : T) : Nil

Adds element on to the end of the vector, incrementing its size by 1.

external function pop() : T

Removes the last element in the vector, decrementing its size by 1.

external function get(pos : UInt) : T

Returns the element stored in the position pos.

external function set(pos : UInt, element : T) : Nil

Sets the value at position pos to element.

external function insert(pos : UInt, element : T) : Nil

Inserts the value element at the given position pos, incrementing the vector’s size by 1. The function insert(size(), element) is equivalent to push(element).

external function remove(pos : UInt) : Nil

Removes the element stored in position pos, decrementing the vector’s size by 1. The function remove(size() - 1) is equivalent to pop().

The UnboundedVector type implements the following trait instances:

trait instance Default<T where !Verified<T>>(UnboundedVector<T>)

Unbounded vectors can always be defaulted, even if the element type T is not defaultable. A vector’s size defaults to 0.

trait instance NonVerifiedEq<T where !Verified<T>>(UnboundedVector<T>)

Unbounded vectors can be compared for equality, but only in the generated code and not during verification.

external type VerifiedVector<T, val maxSize : UInt where Verified<T>, 0 <= maxSize>
Standard:1.1

Represents a vector type with verified size and contents, where a maximum possible size maxSize is specified. The maximum capacity is always allocated on creation of a verified vector in Coco and cannot be changed, but the member functions createWithCapacity and reserve are provided to control the target implementation object’s capacity.

VerifiedVector values can be directly iterated over using for loops.

Warning

The verification performance can potentially suffer significantly as maxSize increases.

It has the following builtin member functions:

external function createWithCapacity(capacity : Bounded<0, maxSize, UInt>) : VerifiedVector<T, maxSize>

Creates a verified vector with a given initial capacity. The verified vector declared in Coco is always created with maximum size capacity, but the specified capacity may have an effect in the target language implementation this maps on to.

external function reserve(capacity : Bounded<0, maxSize, UInt>) : Nil

Reserves a specified capacity in the vector to make sure it is sufficient for a given number of elements. This has no effect on the verified vector declared in Coco since the maximum size capacity is always allocated, but it may have an effect in the target language implementation this maps on to.

external function clear() : Nil

Clears the contents of the vector. The vector is empty after this operation.

external function size() : Bounded<0, maxSize, UInt>

Returns the current size of the vector, namely the number of elements held by the vector.

external function empty() : Bool

Returns true if the vector is currently empty, and false otherwise.

external function push(element : T) : Nil

Adds element on to the end of the vector, incrementing its size by 1.

external function pop() : T

Removes the last element in the vector, decrementing its size by 1.

external function get(pos : Bounded<0, maxSize - 1, UInt>) : T

Returns the element stored in the position pos.

external function set(pos : Bounded<0, maxSize - 1, UInt>, element : T) : Nil

Sets the value at position pos to element.

external function insert(pos : Bounded<0, maxSize - 1, UInt>, element : T) : Nil

Inserts the value element at the given position pos, incrementing the vector’s size by 1. The function insert(size(), element) is equivalent to push(element).

external function remove(pos : Bounded<0, maxSize - 1, UInt>) : Nil

Removes the element stored in position pos, decrementing the vector’s size by 1. The function remove(size() - 1) is equivalent to pop().

The VerifiedVector type implements the following trait instances:

trait instance Default<T, val maxSize : UInt where Verified<T>, 0 <= maxSize>(VerifiedVector<T, maxSize>)

Verified vectors can always be defaulted, even if the element type T is not defaultable. A vector’s size defaults to 0.

trait instance Eq<T, val maxSize : UInt where Eq<T>, Verified<T>, 0 <= maxSize>(VerifiedVector<T, maxSize>)

Verified vectors can be compared for equality precisely when the element type T is comparable for equality.

trait instance Iterable<T, val maxSize : UInt where Verified<T>, 0 <= maxSize>(VerifiedVector<T, maxSize>)

Verified vectors can be directly iterated over using for loops. For example, the following sums all the elements of a vector of integers:

var vector : Vector.VerifiedVector<Int, 10>;
vector.push(1);
vector.push(2);
var sum = 0;
for x in vector {
  sum = sum + x;
}
assert(sum == 3);

Note that the type of the iteration variable x is an immutable variable of the type of the vector’s elements, not a mutable reference, which means that the vector’s contents cannot be modified by writing to it.

Vector2 Module

Coco includes a builtin vector module, called Vector2.coco, which can be accessed by importing it in the usual way. This module defines the following four vectors, starting from the least to the greatest potential impact on the verification time:

  • NonVerifiedVector, which represents a vector with no verifiable properties, and will therefore have the least impact on verification performance.
  • BoundedVector, which represents a vector with a Bounded verifiable size, but where the contents is not verified.
  • UnboundedVector, which represents a vector with an unbounded verifiable size of type UInt, but where the contents is not verified. If the maximum possible size of the vector is known, then BoundedVector is recommended to be used instead for optimal verification performance.
  • VerifiedVector, which represents a vector where the size and contents are verified. This vector will have the greatest impact on the verification, and should therefore be used with caution.

Each vector type is summarised in more detail below.

Note

Vector2 replaces the Vector module, which has been deprecated in Coco language version 1.2. It defines the same vector types with a slight modification to their interface: the types of position parameters are now the same as the size type of a vector. For example, whereas the pos parameter in Vector.BoundedVector.get was Bounded<0, maxSize - 1, UInt>, in Vector2.BoundedVector it is Bounded<0, maxSize, UInt>. This allows for more convenience when mixing position and size values, for example when comparing them.

external type NonVerifiedVector<T where !Verified<T>>
Standard:1.2

Represents a vector type with no verifiable properties. When defaulted, its initial capacity is implementation dependent. The member function createWithCapacity can be used to specify its initial capacity.

It has the following builtin member functions:

external function createWithCapacity(capacity : NonVerified<UInt>) : NonVerifiedVector<T>

Creates a non-verified vector with a specified initial capacity.

external function reserve(capacity : NonVerified<UInt>) : Nil

Reserves a specified capacity in the vector to make sure it is sufficient for a given number of elements.

external function clear() : Nil

Clears the contents of the vector. The vector is empty after this operation.

external function size() : NonVerified<UInt>

Returns the current size of the vector, namely the number of elements held by the vector.

external function empty() : NonVerified<Bool>

Returns true if the vector is currently empty, and false otherwise.

external function push(element : T) : Nil

Adds element on to the end of the vector, incrementing its size by 1.

external function pop() : Result<T, Nil>

Removes the last element in the vector, decrementing its size by 1.

external function get(pos : NonVerified<UInt>) : Result<T, Nil>

Returns the element stored in the position pos.

external function set(pos : NonVerified<UInt>, element : T) : Result<Nil, Nil>

Sets the value at position pos to element.

external function insert(pos : NonVerified<UInt>, element : T) : Result<Nil, Nil>

Inserts the value element at the given position pos, incrementing the vector’s size by 1. The function insert(size(), element) is equivalent to push(element).

external function remove(pos : NonVerified<UInt>) : Result<Nil, Nil>

Removes the element stored in position pos, decrementing the vector’s size by 1. The function remove(size() - 1) is equivalent to pop().

The NonVerifiedVector type implements the following trait instances:

trait instance Default<T where !Verified<T>>(NonVerifiedVector<T>)

Non-verified vectors can always be defaulted, even if the element type T is not defaultable. The vector’s size defaults to 0.

trait instance NonVerifiedEq<T where !Verified<T>>(NonVerifiedVector<T>)

Non-verified vectors can be compared for equality, but only in the generated code.

external type BoundedVector<T, val maxSize : UInt where !Verified<T>, 0 <= maxSize>
Standard:1.2

Represents a vector with a verifiable size, where a maximum possible size maxSize is specified. The contents of the vector are not verified. When the vector is defaulted, its initial capacity is implementation dependent; the builtin external member function createWithCapacity can be used to specify its initial capacity.

It has the following builtin member functions:

external function createWithCapacity(capacity : Bounded<0, maxSize, UInt>) : BoundedVector<T, maxSize>

Creates a bounded vector with an initial size of capacity.

external function reserve(capacity : Bounded<0, maxSize, UInt>) : Nil

Reserves a specified capacity in the vector to make sure it is sufficient for a given number of elements.

external function clear() : Nil

Clears the contents of the vector. The vector is empty after this operation.

external function size() : Bounded<0, maxSize, UInt>

Returns the current size of the vector, namely the number of elements held by the vector.

external function empty() : Bool

Returns true if the vector is currently empty, and false otherwise.

external function push(element : T) : Nil

Adds element on to the end of the vector, incrementing its size by 1.

external function pop() : T

Removes the last element in the vector, decrementing its size by 1.

external function get(pos : Bounded<0, maxSize, UInt>) : T

Returns the element stored in the position pos.

external function set(pos : Bounded<0, maxSize, UInt>, element : T) : Nil

Sets the value at position pos to element.

external function insert(pos : Bounded<0, maxSize, UInt>, element : T) : Nil

Inserts the value element at the given position pos, incrementing the vector’s size by 1. The function insert(size(), element) is equivalent to push(element).

external function remove(pos : Bounded<0, maxSize, UInt>) : Nil

Removes the element stored in position pos, decrementing the vector’s size by 1. The function remove(size() - 1) is equivalent to pop().

The BoundedVector type implements the following trait instances:

trait instance Default<T, val maxSize : UInt where !Verified<T>, 0 <= maxSize>(BoundedVector<T, maxSize>)

A bounded vector can always be defaulted, even if the element type T is not defaultable. A vector’s size defaults to 0.

trait instance NonVerifiedEq<T, val maxSize : UInt where !Verified<T>, 0 <= maxSize>(BoundedVector<T, maxSize>)

Bounded vectors can be compared for equality, but only in the generated code.

external type UnboundedVector<T where !Verified<T>>
Standard:1.2

Represents a vector type with an unbounded size that is verified. The contents of the vector are not verified. When this vector type is defaulted, its initial capacity is implementation dependent. The member function createWithCapacity can be used to specify its initial capacity. If the maximum possible size of the vector is known, then BoundedVector is recommended to be used instead for optimal verification performance.

It has the following builtin member functions:

external function createWithCapacity(capacity : UInt) : UnboundedVector<T>

Creates an unbounded vector with an initial specified capacity.

external function reserve(capacity : UInt) : Nil

Reserves a specified capacity in the vector to make sure it is sufficient for a given number of elements.

external function clear() : Nil

Clears the contents of the vector. The vector is empty after this operation.

external function size() : Int

Returns the current size of the vector, namely the number of elements held by the vector.

external function empty() : Bool

Returns true if the vector is currently empty, and false otherwise.

external function push(element : T) : Nil

Adds element on to the end of the vector, incrementing its size by 1.

external function pop() : T

Removes the last element in the vector, decrementing its size by 1.

external function get(pos : UInt) : T

Returns the element stored in the position pos.

external function set(pos : UInt, element : T) : Nil

Sets the value at position pos to element.

external function insert(pos : UInt, element : T) : Nil

Inserts the value element at the given position pos, incrementing the vector’s size by 1. The function insert(size(), element) is equivalent to push(element).

external function remove(pos : UInt) : Nil

Removes the element stored in position pos, decrementing the vector’s size by 1. The function remove(size() - 1) is equivalent to pop().

The UnboundedVector type implements the following trait instances:

trait instance Default<T where !Verified<T>>(UnboundedVector<T>)

Unbounded vectors can always be defaulted, even if the element type T is not defaultable. A vector’s size defaults to 0.

trait instance NonVerifiedEq<T where !Verified<T>>(UnboundedVector<T>)

Unbounded vectors can be compared for equality, but only in the generated code and not during verification.

external type VerifiedVector<T, val maxSize : UInt where Verified<T>, 0 <= maxSize>
Standard:1.2

Represents a vector type with verified size and contents, where a maximum possible size maxSize is specified. The maximum capacity is always allocated on creation of a verified vector in Coco and cannot be changed, but the member functions createWithCapacity and reserve are provided to control the target implementation object’s capacity.

VerifiedVector values can be directly iterated over using for loops.

Warning

The verification performance can potentially suffer significantly as maxSize increases.

It has the following builtin member functions:

external function createWithCapacity(capacity : Bounded<0, maxSize, UInt>) : VerifiedVector<T, maxSize>

Creates a verified vector with a given initial capacity. The verified vector declared in Coco is always created with maximum size capacity, but the specified capacity may have an effect in the target language implementation this maps on to.

external function reserve(capacity : Bounded<0, maxSize, UInt>) : Nil

Reserves a specified capacity in the vector to make sure it is sufficient for a given number of elements. This has no effect on the verified vector declared in Coco since the maximum size capacity is always allocated, but it may have an effect in the target language implementation this maps on to.

external function clear() : Nil

Clears the contents of the vector. The vector is empty after this operation.

external function size() : Bounded<0, maxSize, UInt>

Returns the current size of the vector, namely the number of elements held by the vector.

external function empty() : Bool

Returns true if the vector is currently empty, and false otherwise.

external function push(element : T) : Nil

Adds element on to the end of the vector, incrementing its size by 1.

external function pop() : T

Removes the last element in the vector, decrementing its size by 1.

external function get(pos : Bounded<0, maxSize, UInt>) : T

Returns the element stored in the position pos.

external function set(pos : Bounded<0, maxSize, UInt>, element : T) : Nil

Sets the value at position pos to element.

external function insert(pos : Bounded<0, maxSize, UInt>, element : T) : Nil

Inserts the value element at the given position pos, incrementing the vector’s size by 1. The function insert(size(), element) is equivalent to push(element).

external function remove(pos : Bounded<0, maxSize, UInt>) : Nil

Removes the element stored in position pos, decrementing the vector’s size by 1. The function remove(size() - 1) is equivalent to pop().

The VerifiedVector type implements the following trait instances:

trait instance Default<T, val maxSize : UInt where Verified<T>, 0 <= maxSize>(VerifiedVector<T, maxSize>)

Verified vectors can always be defaulted, even if the element type T is not defaultable. A vector’s size defaults to 0.

trait instance Eq<T, val maxSize : UInt where Eq<T>, Verified<T>, 0 <= maxSize>(VerifiedVector<T, maxSize>)

Verified vectors can be compared for equality precisely when the element type T is comparable for equality.

trait instance Iterable<T, val maxSize : UInt where Verified<T>, 0 <= maxSize>(VerifiedVector<T, maxSize>)

Verified vectors can be directly iterated over using for loops. For example, the following sums all the elements of a vector of integers:

var vector : Vector2.VerifiedVector<Int, 10>;
vector.push(1);
vector.push(2);
var sum = 0;
for x in vector {
  sum = sum + x;
}
assert(sum == 3);

Note that the type of the iteration variable x is an immutable variable of the type of the vector’s elements, not a mutable reference, which means that the vector’s contents cannot be modified by writing to it.

Attributes

An attribute is additional information that can be added to a Coco declaration or module. These attributes are used in both verification and code generation. For example, when using a code generator that translates Coco into another language, an attribute on a Coco type might tell a code generator which target language type corresponds to the Coco type.

Coco has a number of built-in attributes summarised below. Further, Coco allows users to define their own attributes.

Attributes take the form of a key and a list of arguments:

@«key»(«arguments»)

The key is a sequence of identifiers separated by a dot(.). The arguments are a comma-separated list of expressions, but will usually be constants. Attributes are placed immediately before the declaration or the keyword module to which they apply. A declaration or module can be prefixed by multiple attributes.

Built-in Attributes

attribute @compatible(runtime… : Runtime)

This attribute is used to label derived ports with the runtimes they are expected to be compatible with for the purposes of verifying conformance when using port inheritance.

This is a variadic attribute, and can therefore have a variable number of arguments of type Runtime, for example @compatible(.MultiThreaded) and @compatible(.MultiThreaded, .SingleThreaded).

Applies to:Port declarations.

See also

Implements the Base Port Specification section for further details and examples.

attribute @derive(trait… : Any)
Applies to:Enum declarations, struct declarations, and external type declarations.

This attribute is used to automatically derive instances of traits for the declarations that it can be applied to. @derive is a variadic attribute, and can therefore have a variable number of arguments all of which must be traits.

Consider the following example of a tagged enum declaration:

@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, Coco will automatically derive the instances of the traits Default and Eq for the enum Colour, since Colour is both defaultable, with the default value .RGB(0, 0, 0), and comparable for equality.

The following table summarises which traits can be passed as arguments to @derived for each declaration:

Declaration / Trait Default Eq NonVerifiedEq NonVerifiedOrd
Simple enum
Tagged enum
Struct
External type (with members)
External type (no members)

In the case of automatically deriving the instance of the trait NonVerifiedOrd, the instance of NonVerifiedEq is also required, and has to be explicitly included in the @derive attribute. For example:

@derive(NonVerifiedEq, NonVerifiedOrd)
enum OrderUnverified {
  case One
  case Two
  case Three
}

function f(x : OrderUnverified) : NonVerified<Bool> = {
  val y : OrderUnverified;
  return x < y;
}
attribute @eventually
Applies to:Spontaneous transitions, individual branches of a nondet, individual branches of an offer, and the expression of an optional.

See also

Eventually Attribute section for further details and examples.

attribute @eventually(whenDependable : Bool)
Applies to:Spontaneous transitions, individual branches of a nondet, individual branches of an offer, and the expression of an optional.

See also

Eventually Attribute section for further details and examples.

attribute @eventually(whenDependable : Bool, tag : EventuallyAssumption)
Applies to:Spontaneous transitions, individual branches of a nondet, individual branches of an offer, and the expression of an optional.

See also

Spanning Multiple Transitions section for further details and examples.

attribute @satisfiesEventually(tag : EventuallyAssumption)
Applies to:Event transitions for function calls, spontaneous transitions, individual branches of a nondet, individual branches of an offer, and the expression of an optional.

See also

Spanning Multiple Transitions section for further details and examples.

attribute @ignoreWarning(warning : Warning)

This attribute suppresses various warnings as follows:

enum Warning
case DeadState

Applies to individual states in port state machines, and has the effect of suppressing any dead state warnings for those states.

case IncompleteMatch

Applies to match expressions, and has the effect of suppressing the warning that not all possible cases are explicitly covered.

case MutableNeverWritten

Applied to variable or parameter declarations, and has the effect of suppressing warnings about the variables or parameters being declared mutable, but only read and never written to.

case SingletonEnum

Applies to enum declarations, and suppresses the warnings about the enums only having a single member.

case Unreachable

Applies to states, transitions, provided or required fields in components, and state machines. It has the effect of suppressing the warnings about the corresponding states or transitions being unreachable.

case Unused

Applies to variable and parameter declarations with the effect of suppressing the warning about the variable or parameter declaration being unused; and to field declarations in encapsulating components with the effect of suppressing the warning that there are unused provided ports on component instances.

case Usability

Applies to port state machines, and has the effect of suppressing any warnings about this port state machine being unusable.

attribute @mustUse
Applies to:Enum declarations, struct declarations, external type declarations, and function declarations.

When applied to an enum, struct or external type, this attribute specifies that a corresponding value must be used, otherwise an error will be emitted. See the builtin type Result as an example of how @mustUse can be applied to an enum declaration.

When applied to a function declaration, this attribute specifies that if the function is called as a statement, then the return value cannot be ignored. If it is, then an error is emitted. Consider the following example:

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

In this example, square() is labelled with @mustUse, which means that its return value cannot be ignored when it is called as a statement, as illustrated in the following example:

function squareIgnored(x : Int) : Nil = {
  square(x);
  return nil;
}

The function squareIgnored() calls square(x), but ignores its return value. Coco will report this an error pointing out that the return value of square(x) must be used due to the @mustUse attribute.

The following function is an example of one that correctly uses square():

function squareUsed(x : Int, y : &out Int) : Nil = {
  y = square(x);
  return nil;
}

In this example, the return value of square(x) is assigned to the variable y, which satisfies the @mustUse requirement.

Note

This check is not exhaustive, for example, using function pointers can circumvent this.

attribute @noLog
Applies to:Arguments of a function, signal or state; fields of a struct or an enum case; return type of a function; type declarations.

Specifies that the given item should not be logged using the Log trait.

If this is applied to:

  • An argument of a function, signal or a state: this parameter will not be included in any of the logged events.
  • Field of a struct or an enum case: this parameter will not be included as part of any derived Log trait.
  • Return type of a function: the return type will not be logged as part of any event.
  • A type declaration: the type will never be logged and a Log instance will not be required, even if logValues is set to Always.

See also

Logging Events

Log trait

attribute @noSideEffects
Applies to:Expressions, function interface declarations, and arguments in function declarations.

Specifies that the construct to which the attribute is applied is side-effects free.

When applied to an argument in a function declaration, then this means that the corresponding argument in every call of that function must be side-effects free.

When applied to a function interface declaration in a port, this imposes the requirement on a component providing that port that its implementation of the function must be side-effects free.

Some standard library functions such as assert require their arguments to be side-effects free expressions.

See also

Side Effects section for further details and examples.

attribute @nonExhaustive
Applies to:Enum declarations.

Specifies that if an enum labelled with this attribute is used in a match, then the match expression must have a fallback clause, regardless of whether its match clauses cover all of the enum cases or not. The omission of a fallback clause will lead to a static error in Coco.

Consider the following example:

@nonExhaustive
enum Colour {
  case Red
  case Green
  case Blue
}

function isPrimary(colour : Colour) : Bool = {
  match (colour) {
    .Blue => true,
    .Red => true,
    .Green => true,
    _ => false,
  }
}

The fallback clause in the function isPrimary() declared above is required, since it is using the enum Colour, which is labelled with @nonExhaustive.

We advise using this attribute for enum declarations that are mapped to a version in the generated code (e.g. C++) using the @mapToEnum attribute, in order to make this mapping more robust. This will help cover the case where the Coco version of an enum accidentally omits some cases defined in the corresponding version that it is mapped to. This can arise, for example, if the C++ version is extended with additional cases, and the Coco version is not by mistake.

See also

@mapToEnum attribute.

attribute @queue(kind : Queue)
Applies to:Implementation components and external components.

See also

Queues section for further details and examples.

enum Queue
case Bounded(size : Int)

size specifies the maximum number of signals the queue can hold. During verification, an attempt to send a signal to a component with a full queue is a dynamic error. At runtime, this results in the program being aborted.

case Unbounded(size : Int)

size specifies the maximum number of signals the queue can hold during verification. If a component can receive signals from @unbounded transitions, then size will have to be one greater than the maximum number of other signals (i.e. not from unbounded transitions) the queue can hold. During verification, an attempt to send a signal to a component with a full queue is a dynamic error. At runtime, the queue will automatically expand to increase its capacity. If there is insufficient memory available to expand the queue, then program execution is aborted.

trait instance Cast(Int, Queue)
trait instance ImplicitCast(Int, Queue)
attribute @queue(size : Int)
Applies to:Implementation components and external components.

This is equivalent to:

attribute @represents(description : String)
Applies to:Spontaneous transitions, nondet cases, and offer cases.

The purpose of this attribute is to annotate the counterexample output with the text specified by description.

attribute @runtime(runtime : Runtime)
Applies to:Components.
enum Runtime
case MultiThreaded
case SingleThreaded

See also

Runtimes section for further details and examples.

attribute @slow
Applies to:Spontaneous transitions.

See also

Slow Attribute section for further details and examples.

attribute @unbounded
Applies to:Spontaneous transitions that send of a signal.

See also

Unbounded Attribute section for further details and examples.

attribute @unbounded(whenDependable : Bool)
Applies to:Spontaneous transitions that send of a signal.

See also

Unbounded Attribute section for further details and examples.

attribute @untidy(check… : TidyCheck)
Applies to:Declarations.

This attribute suppresses the warnings resulting from the Coco Tidy checks listed as arguments. The checks are of type TidyCheck, defined as follows:

enum TidyCheck
case ReadabilityBoolLikeEnum
case ReadabilityCognitiveComplexity
case ReadabilityElseAfterControlFlow
case ReadabilityNaming
case ReadabilityPortOfferNondet

See also

Coco Tidy section for further details and examples.

attribute @unreliable
Applies to:Spontaneous transitions.

See also

Unreliable Attribute section for further details and examples.

attribute @unreliable(isUnreliable : Bool)
Applies to:Spontaneous transitions.

See also

Unreliable Attribute section for further details and examples.