Revise exceptional specifications

[n-osborne]

In the current state, Gospel distinguishes between normal and exceptional postonditions. It is pretty straitforward to describe how the function let the state after raising an exception. It is however less easy to express why an exception has been raised.

ensures clauses (normal postconditions) should hold when the function doesn't raise any exception and raises ones (exceptional postconditions) when the function does raise the specified exception. Of course, it is possible to describe the pre-state using the old operator in both of these kinds of clause. But there is no guarantee that the two clauses are exclusive.

For now, we are using some cumbersome way of enforcing this exculsive disjunction between normal and exceptional postconditions:

type 'a t
(*@ mutable module contents 'a list *)

val pop : 'a t -> 'a
(*@ r = pop q
    modifies q.contents
    ensures match (old q.contents) with
            | [] -> false
            | x :: _ -> r = x
    raises Empty -> q.contents = old q.contents = [] *)

Acsl uses behaviours to distinguish between normal behaviours and failures (for example), but the user has to indicate whether the behaviours are exclusives or not in the specifications.
I think we can leverage the fact that we have types and pattern matching to express this.

The idea is that a function that returns a value of type 'a but can raise an exception is in fact returning a value of type: 'a + ⊥ (⊥ standing for exceptions). In the following example, the + sign in 'a + ⊥ is interpreted as an extention operator, but we could also make it a real sum type (for example with the two contructors Normal and Exceptional). We can then pattern match on the result in the post-conditions to get the information whether an exception has been raised or not.

Matching on the result:

val pop : 'a t -> 'a
(*@ r = pop q
    modifies q.contents
    ensures match r with
            | x -> x = List.hd (old q.contents) /\ q.contents = List.tail (old q.contents) (* this will fail if the list is empty *)
            | exception Empty -> q.contents = old q.contents = [] *)

Or matching on the argument (also allowing x = exception E to be sugar for match x with | exception E -> true | _ -> false in the example):

val pop : 'a t -> 'a
(*@ r = pop q
    modifies q.contents
    ensures match old q.contents with
            | [] -> r = exception Empty /\ q.contents = []
            | x :: xs -> r = x /\ q.contents = xs

In order to be able to analyse the exhaustivity of pattern matching, we will need to reintroduce the raises clause, but only with the name of the possible exceptions:

val pop : 'a t -> 'a
(*@ r = pop q
    modifies q.contents
    raises Empty
    ensures match old q.contents with
            | [] -> r = exception Empty /\ q.contents = []
            | x :: xs -> r = x /\ q.contents = xs

[fpottier]

In OCaml, when we write r = pop q or let r = pop q, the variable r denotes a value; it cannot denote an exception.

Still in OCaml, let r = pop q in match r with ... is not synonymous with match pop q with ..., due to exception clauses.

What I am trying to say is, if we want to reason about "results" (value + exception) in the logic, then we need to find a syntax that clearly distinguishes between values and results. Otherwise, we will create confusion.