Coco is a strongly typed expression-orientated language that was designed specifically for developing event-driven software, and is packed with features you would expect in a modern programming language.
Formalising behavioural interfaces between components
A Coco port specifies the interface to part of the software. Ports are like interfaces in other languages, in that they describe the APIs that can be used. In addition, they also include a state machine that defines how the APIs must be used, thereby specifying a contract between connected components. These contracts act both as specifications for components implementing them, and as assumptions that other components using them can make.
Implementing your event-driven software in Coco
With native support for state machines, including hierarchical and parameterised states – as well as the usual constructs you’d expect in a modern programming language – Coco is ideal for implementing the event-driven parts of your software.
Thanks to the verification provided by Popili, your Coco implementations are automatically formally verified to check whether they meet their specifications, and interact with other parts of the system correctly too.
Capturing the environment your software will run in
Coco components always interact with other parts of the system that are not implemented in Coco. These are explicitly captured in Coco as external components. By capturing the boundary with ports, this provides the verification engine with precise assumptions of how the rest of the system behaves. External components also generate skeletons to ease integration.
Building your system in Coco
Using Coco, you can decompose large systems into a collection of smaller well-defined subsystems, and precisely specify how they are connected together. Thanks to the power of Coco, it’s possible for teams to build different subsystems independently of one another, and be confident that they will work correctly upon integration.
Architectures are expressed directly in Coco, and graphical representations are auto-generated to make it easier to visualise and share with others.
State machines are a great way of expressing event-driven software. With Coco, you can create state machines that include hierarchical states, parameterised states, entry and exit functions, invariants, and timers. You can also factor out common code by declaring functions anywhere in your state machine, or by using state machine inheritance.
component Resource {
val client : Array<Provided<LockableResource>, kClients>
machine {
state Unlocked {
client[val i].lock() = {
setNextState(Locked(i).Idle);
return true;
}
}
state Locked(owner : Bounded<0, kClients - 1>) {
client[val j | j != owner].lock() = false
client[owner].unlock() = setNextState(Unlocked)
state Idle {
client[owner].action() = setNextState(Running)
}
state Running {
after(seconds(10)) = {
client[owner].finished();
setNextState(Idle);
}
}
}
}
}
Event-driven systems often have to handle errors, so Coco includes built-in support for explicit error handling using a dedicated Result type. This provides a simple method of modelling operations that might succeed with a result, or fail with an error. Coco also includes built-in constructs to allow easy propagation of errors between functions, saving developers time from writing boilerplate error handling code.
external function isValid(id : String) : Result<Nil, Nil> =
nondet {
.Error(nil),
.Ok(nil),
}
external function isValid(id : String, password : String) : Result<Nil, Nil> =
nondet {
.Error(nil),
.Ok(nil),
}
function login(username : String, password : String) : Result<String, Nil> = {
isValid(username)?;
isValid(username, password)?;
return .Ok(username);
}
No two projects are the same, and so Coco allows users to create and verify custom user-defined types, which can also be generic. In fact, Coco is sufficiently expressive that all the built-in types are defined in Coco, and Coco’s state machine semantics can even be described directly in Coco. All of this enables developers to concisely express their logic, leading to more reliable, more maintainable software.
@derive(Default, Eq)
enum Optional<T> {
case None
case Some(value : T)
function hasValue() : Bool =
match (self) {
Some(_) => true,
_ => false,
}
function value() : T = match (self) { Some(v) => v, }
function valueOr(default : T) : T =
match (self) {
None => default,
Some(v) => v,
}
mut function reset() : Nil = { self = .None; }
}
Coco has been designed from the start to support easy integration into your existing codebase, for example, via external types and functions. These allow you to refer to pre-existing types and functions, declared elsewhere in your codebase, from within Coco. External types and functions can even include abstract specifications that allow Popili to verify whether they are being used correctly. Coco’s powerful attribute system allows you to tell Coco what the corresponding mappings are in the target language.
@derive(Default)
@CPP.mapToType("std::vector<{0}>", .ConstReference, .System("vector"))
external type Vector<T, val max : Int where 0 <= max> {
var size_ : Bounded<0, max>
@CPP.mapToMember("clear")
mut external function clear() : Nil = {
size_ = 0;
}
@CPP.mapToMember("size")
external function size() : Bounded<0, max> = size_
@CPP.mapToMember("push_back")
mut external function pushBack(x : T) : Nil = {
size_ = size_ + 1;
}
}