Coma specification

In Coma, the abstraction barrier is flexible.

The barrier

In a function definition, the abstraction barrier divides the part that is visible to the caller from the implementation part which is hidden from the caller.

In traditional contract-based languages, this barrier is implicitly set at the level of the = symbol, for example in WhyML:

  let rec fact n
    requires { n >= 0 }
    ensures  { result = n! }
  = if n = 0 then 1 else n * fact (n-1)
   🯊
there is an implicit abstraction barrier here

Here the caller only sees the specification, but not the implementation.

Later in the code:

  (* here we have to prove the precondition (55 >= 0) *)
  let f55 = fact 55 in
  (* here we learn the postcondition (f55 = 55!) *)

Examples in Coma

If you want the traditional barrier and specification

let rec fact (n: int) { n >= 0 } (return (r: int) { r = n! })
                      ─────┬────                  ────┬─────
                           β”‚                precondition of `return`
    precondition of `fact` β”˜              ≑ postcondition of `fact`
= if {n = 0} (-> return {1})
             (-> fact {n-1} (fun (r: int) -> return {n*r})

Remark: the latter is syntactic sugar for

let rec fact (n: int) (return (r: int))
= { n >= 0 }
  (! if {n = 0} (-> out {1})
                (-> fact {n-1} (fun (r: int) -> out {n*r}))
  [ out (res: int) -> { r = n! } (! return {res})]

where the precondition is an assertion over a abstraction barrier which hides the implementation and the postcondition is put in a wrapper over the call of the outcome.

Or else, you can remove the assertion without touching the barrier

let rec fact (n: int) {} (return (r: int) { r = n! })
= if {n = 0} (-> return {1})
             (-> fact {n-1} (fun (r: int) -> return {n*r})

Here again, the body is hidden (which is what we want since the handler is recursive). It is the same as before but with a precondition equivalent to true.

Or else, you can push the barrier inside the code

let rec fact (n: int) (return (r: int) { r = n! })
= if {n = 0} (-> return {1})
             (-> { n > 0 } (! fact {n-1} (fun (r: int) -> return {n*r}))
                 ^^^^^^^^^ ^^                                         ^

The precondition will only have to be proved in the else case. The then case is inlined (from the verification point of view).

Or else, do not put the barrier at all, which will lead to a fully inlined handler

Consider the rotate_left handler, which one can use for balancing a binary tree.

let rotate_left (t: tree) (return (r: tree))
= unTree {t} (fun (a:tree) (x:elt) (r:tree) ->
  unTree {r} (fun (b:tree) (y:elt) (c:tree) ->
  return {node (node a x b) y c})
  fail) fail

This is a good example where the specification would be the same as the code. Thus we prefer not to put a barrier, which has the effect of fully inlining the handler at the call position.

Notice that a barrier is mandatory in the definition of fact because it is recursive. Any recursive call must be protected by a barrier.

Handler declaration

We can declare and specify a handler without implementing it.

let if (b: bool) (then {b}) (else {not b}) = any

Here {b} (resp. {not b}) is the postcondition of if in the then (resp. else) branch. This is syntactic sugar for:

let if (b: bool) (then) (else) =
  any
  [ tt -> {b}     (! then)
  | ff -> {not b} (! else) ]