Standard Library¶

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 2³¹ - 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.

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.

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

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.