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.
-
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 either0
or1
. 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 ofBounded
.Bounded
has the following static constants:The bounds of a
Bounded
type are accessible by using the static constantsFirst
andLast
. For example, the following variable declaration is initialised with the upper bound of theBounded
type: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 constantsFirst
andLast
, rather than defining the bounds as independent constants as follows:The constant variable
upper
is of typeInt
, and will only work in contexts requiring anInt
. In contrast, ifDeviceId
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 aDeviceId
or anInt
type, sinceBounded
is implicitly convertible toInt
.-
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
-
type
BoundedInt
<val lower : Int, val upper : Int where lower <= (upper - 1)> = Bounded<lower, upper - 1, Int>¶ Represents a bounded integer
value
in the rangelower <= value < upper
. For example,BoundedInt<0, 2>
is an integer that can be assigned to either0
or1
. 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 typeBounded
.BoundedInt
is atype alias
ofBounded
, where the upper bound is a symbolic binary type expression, namelyupper - 1
. Since this bound is not a simple literal, Coco does not check whether bounded literal initialisers are out of bounds.
-
external type
Duration
¶ Specifies the time interval used in a
timer transition
.-
trait instance
NonVerifiedEq
(Duration)
Instances of
Duration
can be constructed using the following functions:-
external function
microseconds
(t : NonVerified<Int>) : Duration¶ Creates a
Duration
oft
microseconds.
-
external function
milliseconds
(t : NonVerified<Int>) : Duration¶ Creates a
Duration
oft
milliseconds.
-
external function
seconds
(t : NonVerified<Int>) : Duration¶ Creates a
Duration
oft
seconds.
-
external function
minutes
(t : NonVerified<Int>) : Duration¶ Creates a
Duration
oft
minutes.
-
external function
hours
(t : NonVerified<Int>) : Duration¶ Creates a
Duration
oft
hours.
-
trait instance
-
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
(NonVerified<Int>, NonVerified<Int>)
-
trait instance
Cast
(NonVerified<Int>, NonVerified<UInt>)
-
trait instance
Integer
(NonVerified<Int>)
-
trait instance
Negatable
(NonVerified<Int>)
-
trait instance
Num
(NonVerified<Int>)
-
trait instance
-
external type
UInt
¶ A 32-bit unsigned integer.
-
trait instance
Cast
(NonVerified<UInt>, NonVerified<Int>)
-
trait instance
Cast
(NonVerified<UInt>, NonVerified<UInt>)
-
trait instance
Integer
(NonVerified<UInt>)
-
trait instance
Num
(NonVerified<UInt>)
-
trait instance
-
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 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.
-
trait instance
-
external type
Range
¶ Represents an integer range so that it can be iterated over within a
for
loop.-
external function
range
(lowerBound : Int, upperBound : Int) : Range¶ This creates a
Range
object that is suitable for iterating over the integersx
such thatlowerBound <= x < upperBound
. For example, the following sums all the integers between1
and10
(including1
but excluding10
):var sum = 0 for x : Int in range(1, 10) { sum = sum + x; }
-
external function
-
external type
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 aSymmetricArray
. It can only be used withinstate machines
ofimplementation components
, and cannot be used inside complex types, such asstructs
. The following example illustrates the use ofSymmetricArrayIndex
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.-
trait instance
Container Types¶
-
external type
Array
<T, val size : Int where 0 <= size>¶ Represents a fixed-size array of size
size
containing items of typeT
. 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
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
-
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
andCPP.mapToValue
attributes.-
trait instance
ImplicitCast
<T, val size : Int where 0 <= size>(Array<T, size>, List<T>)
-
trait instance
-
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()
isOptional<Int>
, and the function body specifies that it will nondeterministically return eitherOptional.None
,Optional.Some(0)
, orOptional.Some(1)
.The main function
update(msg : &out Message)
steps throughmsg
, and for each array element, assigns the value returned from callinggetData()
. In the event thatOptional.None
is returned,-1
is assigned as the value in the corresponding array element (msg[index]
). The function returnstrue
in the case wheremsg
only contains actual values received fromgetData()
, andfalse
otherwise.The enum
Optional<T>
also has the following builtin member functions:-
function
hasValue
() : Bool¶ If the value is of the form
Some(v)
wherev
is a value of typeT
, then this function returnstrue
, otherwise it returnsfalse
.
-
function
value
() : T¶ This function assumes that the value is of the form
Some(v)
wherev
is a value of typeT
, and returnsv
. It is a dynamic error to call this function with the valueNone
.
-
function
valueOr
(default : T) : T¶ If the value is of the form
Some(v)
, then this function returnsv
, otherwise it returns the value of default.
Consider the following simple example functions to illustrate the use of these member functions:
The function
hasData1()
will always returntrue
, because the variabledata
is assigned the valueOptional.Some(3)
, and therefore the member functiondata.hasValue()
returnstrue
. In contrast, the functionhasData2()
will always returnfalse
, because after the variabledata
is assigned a value, and before the function returns,data
is reset to having no value as a result of callingdata.reset()
.See also
Try operator
expression.-
case
-
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 thetry 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 expressione
of typeResult
is ignored. The following example illustrates the importance of this attribute when usingResult<T, E>
and thetry operator
for error handling:In this example, if
check(x)?
evaluates to.Error(nil)
, then the functionsquare(…)
will immediately return early with the value.Error(nil)
. Since the builtin typeResult<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
error
() : E¶ This function assumes that the value is of the form
Error(e)
wheree
is a value of typeE
, and returnse
. It is a dynamic error to call this function with a value of the formOk(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)
wherev
is a value of typeT
, and returnsv
. It is a dynamic error to call this function with a value of the formError(e)
.
-
function
valueOr
(default : T) : T¶ If the value is of the form
Ok(v)
, then this function returnsv
, otherwise it returns the value of default.
See also
Try operator
expression.-
case
-
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 typeSlot<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
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 byT
. By default, all instances ofSlot<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:
where the return type of
getData()
isData
, which is declared as anexternal type
. This component fails verification with a runtime error becauseclient.getData()
is called and is trying to returnv
, which has not been initialised or assigned a value. In contrast, consider the following example:In this example, when
client.getData()
is called, it is guaranteed to return a valid value forv
, because of the call on the external functiongetUpdate(&v)
before it returns.The external function
getUpdate(_ : &out Data)
is guaranteed to write an arbitrary but validData
into the variable, because Coco requires allout
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 aSlot<T>
is passed to a function taking aT
, 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:This function has an
&out
parameterdata
of type&out Slot<Data>
, which means that, unlike the previous example, the value ofdata
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 todata
by the time it returns, the decision of which is made nondeterministically. If it has written a valid value, then the function returnstrue
, otherwise it returnsfalse
.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
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 constant
-
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 formProvided<T>
. The second parametersize
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 typeSymmetricArrayIndex
, 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.
-
trait instance
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.-
function
-
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()
).-
function
-
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 overNonVerifiedEq
. You should not implement bothEq
andNonVerifiedEq
for the same type.
-
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 ifEq
is not also defined. You should not implement bothEq
andNonVerifiedEq
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.
!=
).
-
function
-
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.-
type
-
trait
Iterable
<ContainerType>¶ Represents a container of type
containerType
that contains items that can be iterated over using afor
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.
-
type
-
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.
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:
The following example illustrates how the fields in a struct
can be referenced in format strings:
-
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
logBeginArray
() : ArrayLogFormatter¶
-
external function
logBeginEnum
(caseName : String, positional : Bool) : EnumLogFormatter¶
-
external function
logBeginStruct
() : StructLogFormatter¶
-
external function
Formatter also utilises several helper types:
-
external type
ArrayLogFormatter
¶ Standard: 1.2
-
external type
EnumLogFormatter
¶ Standard: 1.2
-
external type
StructLogFormatter
¶ Standard: 1.2
Consider the following example of a simple struct
:
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 overNonVerifiedOrd
. You should not implement bothOrd
andNonVerifiedOrd
for the same type.
-
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 ifOrd
is not also defined. You should not implement bothOrd
andNonVerifiedOrd
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>¶
-
function
-
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¶
-
function
-
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¶
-
function
-
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¶
-
function
-
trait
Verified
<T>¶
General Functions¶
-
external function
abort
() : Div¶ If this function is ever executed then it is a dynamic error. For example:
The above handles
x
if it evaluates totrue
, and callsabort()
otherwise.Note
The function
abort()
differs fromillegal
: ifabort()
is ever called, then this is a fatal error. In contrast, declaring that an event isillegal
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
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.
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 : NonVerified<Bool>, second : NonVerified<Bool>) : NonVerified<Bool>
Implements !
:
-
external function
logicalNot
(first : NonVerified<Bool>) : NonVerified<Bool>¶
Implements ||
:
-
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 aBounded
verifiable size, but where the contents is not verified.UnboundedVector
, which represents a vector with an unbounded verifiable size of typeUInt
, but where the contents is not verified. If the maximum possible size of the vector is known, thenBoundedVector
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, andfalse
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
toelement
.
-
external function
insert
(pos : NonVerified<UInt>, element : T) : Result<Nil, Nil>¶ Inserts the value
element
at the given positionpos
, incrementing the vector’s size by 1. The functioninsert(size(), element)
is equivalent topush(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 functionremove(size() - 1)
is equivalent topop()
.
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 to0
.
-
trait instance
NonVerifiedEq
<T where !Verified<T>>(NonVerifiedVector<T>) Non-verified vectors can be compared for equality, but only in the generated code.
-
external function
-
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 functioncreateWithCapacity
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, andfalse
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
toelement
.
-
external function
insert
(pos : Bounded<0, maxSize - 1, UInt>, element : T) : Nil¶ Inserts the value
element
at the given positionpos
, incrementing the vector’s size by 1. The functioninsert(size(), element)
is equivalent topush(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 functionremove(size() - 1)
is equivalent topop()
.
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 to0
.
-
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 function
-
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, thenBoundedVector
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, andfalse
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
insert
(pos : UInt, element : T) : Nil¶ Inserts the value
element
at the given positionpos
, incrementing the vector’s size by 1. The functioninsert(size(), element)
is equivalent topush(element)
.
-
external function
remove
(pos : UInt) : Nil¶ Removes the element stored in position
pos
, decrementing the vector’s size by 1. The functionremove(size() - 1)
is equivalent topop()
.
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 to0
.
-
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 function
-
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 functionscreateWithCapacity
andreserve
are provided to control the target implementation object’s capacity.VerifiedVector
values can be directly iterated over usingfor
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, andfalse
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
toelement
.
-
external function
insert
(pos : Bounded<0, maxSize - 1, UInt>, element : T) : Nil¶ Inserts the value
element
at the given positionpos
, incrementing the vector’s size by 1. The functioninsert(size(), element)
is equivalent topush(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 functionremove(size() - 1)
is equivalent topop()
.
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 to0
.
-
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.
-
external function
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 aBounded
verifiable size, but where the contents is not verified.UnboundedVector
, which represents a vector with an unbounded verifiable size of typeUInt
, but where the contents is not verified. If the maximum possible size of the vector is known, thenBoundedVector
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, andfalse
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
toelement
.
-
external function
insert
(pos : NonVerified<UInt>, element : T) : Result<Nil, Nil>¶ Inserts the value
element
at the given positionpos
, incrementing the vector’s size by 1. The functioninsert(size(), element)
is equivalent topush(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 functionremove(size() - 1)
is equivalent topop()
.
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 to0
.
-
trait instance
NonVerifiedEq
<T where !Verified<T>>(NonVerifiedVector<T>) Non-verified vectors can be compared for equality, but only in the generated code.
-
external function
-
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 functioncreateWithCapacity
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, andfalse
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
toelement
.
-
external function
insert
(pos : Bounded<0, maxSize, UInt>, element : T) : Nil¶ Inserts the value
element
at the given positionpos
, incrementing the vector’s size by 1. The functioninsert(size(), element)
is equivalent topush(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 functionremove(size() - 1)
is equivalent topop()
.
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 to0
.
-
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 function
-
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, thenBoundedVector
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, andfalse
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
insert
(pos : UInt, element : T) : Nil¶ Inserts the value
element
at the given positionpos
, incrementing the vector’s size by 1. The functioninsert(size(), element)
is equivalent topush(element)
.
-
external function
remove
(pos : UInt) : Nil¶ Removes the element stored in position
pos
, decrementing the vector’s size by 1. The functionremove(size() - 1)
is equivalent topop()
.
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 to0
.
-
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 function
-
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 functionscreateWithCapacity
andreserve
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, andfalse
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
toelement
.
-
external function
insert
(pos : Bounded<0, maxSize, UInt>, element : T) : Nil¶ Inserts the value
element
at the given positionpos
, incrementing the vector’s size by 1. The functioninsert(size(), element)
is equivalent topush(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 functionremove(size() - 1)
is equivalent topop()
.
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 to0
.
-
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.
-
external function
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, andexternal 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:In this example, Coco will automatically derive the instances of the traits
Default
andEq
for the enumColour
, sinceColour
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 ofNonVerifiedEq
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 anondet
, individual branches of anoffer
, and the expression of anoptional
.See also
Eventually Attribute section for further details and examples.
-
attribute
@eventually
(whenDependable : Bool) Applies to: Spontaneous transitions
, individual branches of anondet
, individual branches of anoffer
, and the expression of anoptional
.See also
Eventually Attribute section for further details and examples.
-
attribute
@eventually
(whenDependable : Bool, tag : EventuallyAssumption) Applies to: Spontaneous transitions
, individual branches of anondet
, individual branches of anoffer
, and the expression of anoptional
.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 anondet
, individual branches of anoffer
, and the expression of anoptional
.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.
-
case
-
enum
-
attribute
@mustUse
¶ Applies to: Enum
declarations,struct
declarations,external type
declarations, andfunction
declarations.When applied to an
enum
,struct
orexternal type
, this attribute specifies that a corresponding value must be used, otherwise an error will be emitted. See the builtin typeResult
as an example of how@mustUse
can be applied to anenum
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: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:The function
squareIgnored(…)
callssquare(x)
, but ignores its return value. Coco will report this an error pointing out that the return value ofsquare(x)
must be used due to the@mustUse
attribute.The following function is an example of one that correctly uses
square(…)
:In this example, the return value of
square(x)
is assigned to the variabley
, 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 anenum
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 anenum
case: this parameter will not be included as part of any derivedLog
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 iflogValues
is set toAlways
.
-
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 amatch
, then thematch
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 enumColour
, 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, thensize
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
ImplicitCast
(Int, Queue)
-
case
-
enum
-
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, andoffer
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
.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
¶
-
case
See also
Coco Tidy section for further details and examples.
-
enum
-
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.