Open n-osborne opened 8 months ago
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.
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 andraises
ones (exceptional postconditions) when the function does raise the specified exception. Of course, it is possible to describe the pre-state using theold
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:
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 contructorsNormal
andExceptional
). 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:
Or matching on the argument (also allowing
x = exception E
to be sugar formatch x with | exception E -> true | _ -> false
in the example):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: