Develop your software with Coco

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.

Ports

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.

port LightControl {
  function on(status : Bool) : Bool
  function off() : Nil
  outgoing signal fault(id : ErrorId)

  machine {
    @unreliable
    spontaneous = fault(_)

    state Off {
      on(status) = nondet {
        {
          setNextState(On(status)); true
        },
        false,
      }
    }
    state On(status : Bool) { … }
  }
}

Implementations

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.

@queue(4)
@runtime(.MultiThreaded)
component TrafficControlImpl {
  val client : Provided<TrafficControl>
  val lights : Required<LightControl>
  val barriers : Required<BarrierControl>

  machine {
    state Uninitialised { … }

    state Operational {
      state TrafficFlowing {
        client.stopTraffic() = {
          lights.flashingOn();
          setNextState(Stopping);
        }
        lights.fault(errorId) = setNextState(Recovery(errorId))
      }

      state Recovery(id : ErrorId) { … }
      …
    }
  }
}

Integration

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.

@runtime(.MultiThreaded)
external component BarrierController {
  val client : Provided<BarrierControl>
}

port BarrierControl {
  function initialise() : Bool
  function open() : Nil
  function close() : Nil
  outgoing signal status(isOpen : Bool)

  machine {
    // …
  }
}

Architectures

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.

@runtime(.MultiThreaded)
component BridgeSystem {
  val user : UserGui
  val maintenance : UserGui
  val bridge : BridgeControlImpl
  val traffic : TrafficControlImpl
  val lightControl : LightControlImpl
  val barriers : BarrierController
  val light0 : LightSource
  val light1 : LightSource
  val lift : LiftSystem

  init() = {
    connect(user.bridge, bridge.client[0]);
    connect(maintenance.bridge, bridge.client[1]);
    connect(bridge.traffic, traffic.client);
    connect(bridge.lift, lift.client);
    connect(traffic.lights, lightControl.client);
    connect(traffic.barriers, barriers.client);
    connect(lightControl.lights[0], light0.client);
    connect(lightControl.lights[1], light1.client);
  }
}

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.

> traffic (Operational.TrafficFlowing): client.stopTraffic{}
> light (Operational): client.flashingOn{}
> halLight: client.onOff{onOff=true}
< halLight: client.onOff{}
< light (Operational.Flashing): client.flashingOn{}
< traffic (Stopping.SettingLights): client.stopTraffic{}

You can find further details about Coco in our Language Reference.

Next step

Eliminate errors in your system

Explore more

Make your software development more effective and efficient

Book a demo