core-language.md

The Copilot Core Language

This document describes the Copilot Core language.

Syntax

A Copilot specification, p, in the core language consists of:

1. A list of streams, s.1 ... s.n.

2. A list of triggers, t.1 ... t.n.

A stream, s, consists of

1. a finitite list of atomic values, x.1 ... x.n, which we denote buffer(s). The length of the list we denote size(s).

2. An expression, e, which we denote exp(s).

A trigger, t, consists of:

1. An expression of type bool, g, which we denote guard(t).

2. A list of trigger arguments, a.1 ... a.n, which we denote args(t).

A trigger argument, a, consists of:

1. An expression, e, which we denote exp(a).

Expressions are constructed as follows:

1. If e is an expression and x is an atomic value, then const(x) is an expression.

2. If s is a stream with a buffer of length i and k is an integer such that 0 <= k < i, then s[k]_ is an expression.

3. If op is an n-ary atomic operator and e.1 ... e.n are expressions, then op(e.1 ... e.n) is an expression.

Atomic values

T.B.D.

Typing rules

T.B.D.

Semantics

Program execution is devided into a well ordered sequence of atomic instants, where each instant, i, corresponds to a natural number.

The value of an expression e at the instant i is denoted E|i|(e) and is defined by:

• E|i|(const(x)) = V(x)

• E|i|(s|k|) = E|i-k|(s)

• E|i|(op(e.1, ..., e.n)) = (V(op))(E|i|(e.0), ...,E|i|(e.n))

The value of a stream s at the instant i is denoted E|i|(s) and is defined by:

• E|i|(s) = if i < 0 then buffer(s).(i + size(s)) else E|i|(*exp(s)).