Coma Programs

Coma programs are executable expressions we want to specify and prove.

Coma Syntax

A Coma program is a collection of handlers.

A top level handler definition is of the form: let <prototype> = <body>. A handler can be recursive using the let rec binding and multiple top-level handlers can be mutually recursive using

let rec <prototype> = <body>
with <prototype> = <body>
with <prototype> = <body>

As a first example, let's look at the definition of the cons handler.

let cons < 'a >  (h: 'a)  (t: list 'a)  (ret (l: list 'a)) = ret {Cons h t}
    ─┬── ─┬────  ─────┬─  ─────┬──────  ───┬────────────┬─   ─┬────────────
     │    │           │        │           │            │     │
    name  │           │        │   outcome parameter    │     │
     │    └ type      │        │                        │     │
     │      parameter │        │                        │     │
     │                └ term parameters                 │     │
     │                                                  │     │
     └───┬──────────────────────────────────────────────┘     │
         └ <prototype>                                        └ <body>

The prototype follows the grammar:

<prototype> ::= h π
                ┬ ┬
                │ │
                │ └ signature
                │
                └ handler name

          π ::= < 'a >* (x: τ)* (&x: τ)* { t }* <prototype>*
                ──┬───  ──┬───  ───┬───  ──┬──  ──┬────────
                  │       │        │       │      │
   type parameter ┘       │        │       │      │
                          │        │       │      │
           term parameter ┘        │       │      │
                                   │       │      │
               reference parameter ┘       │      │
                                           │      │
                              precondition ┘      │
                                                  │
                                handler parameter ┘

where τ is a term type:

  τ ::= 'a                               type variable
      | int | bool | …                   basic type
      | list τ                           type application
      | …

The body is a Coma expression (e), which follows the grammar:

  t ::= WhyML terms¹

  e ::= h                                  handler
      | e < t >                            application to a type `t`
      | e { t }                            application to a term `t`
      | e &r                               application to a reference `r`
      | e₁ e₂                              application to an expression
      | (! e)                              abstraction barrier
      |  { t }  e                          assertion
      | -{ t }- e                          assumption
      | fun π -> e                         anonymous handler
      | (-> e)                             anonymous nullary handler
      | e [ h π₁ =  e₁ | g π₂ =  e₂ ]      group of mutually recursive definitions²
      | e [ h π₁ -> e₁ | g π₂ -> e₂ ]      group of nonrecursive definitions
      | e [ x:  τ = t ]                    `let x = t in e`     (let binding)
      | e [ &x: τ = t ]                    reference allocation
      | [ &x <- t ] e                      reference modification
      | e₁ . e₂                            syntactic sugar for `e₁ (e₂)`

¹Check the syntax of WhyML terms.

²The user can read “e where h π₁ = e₁ and g π₂ = e₂ are mutually recursive handlers”

Remarks

the terms must be written inside curly braces { x+2 }, { sorted l } (with the exception of those in let and set)

the let and set can be done multiple times in one with the syntax

    e [ x: τ = 34 | y: τ = 55 ]            parallel let-binding
    e [ &x <-  89 | &y <- 144 ]            parallel set

Examples

Many examples can be found in https://gitlab.inria.fr/why3/why3/-/blob/coma-only/examples/coma/.

Program definition

Top-level handler definition:
- two parameters x and y, single continuation ret
```
let add (x y: int) (return (z: int)) = return {x+y}
```
- same example using mutable state (only z is mutable)
```
let add (x y &z: int) (return) = [&z <- x+y] return
```

Handler declaration (specification without implementation)

let unList < 'a > (l: list 'a)
  (onCons (h: 'a) (t: list 'a) {l = Cons h t})
  (onNil {l = Nil})
= any

Element insertion in a sorted list

let rec insert (x: int) (l: list int) {sorted l}
               (return  (r: list int) {sorted r && permut r (Cons x l)})
= unList <int> {l}
    (fun (h: int) (t: list int) ->
      if {x < h} (-> return {Cons x l}) .
      insert {x} {t} . fun (r: list int) ->
      return {Cons h r})
    (return {Cons x Nil})