[QCheck-STM] Catch Partial_function in postcond and precond and return false instead

[n-osborne]

This issue is related to the discussion on #271

At the moment, the execution of specifications containing partial functions (e.g Sequence.hd) may raise the Partial_function exception (when called on Sequence.empty). This exception is never caught. A message is printed to the user to inform about what is happening ([see here).

I believe this is not as much informative that it could be on the user perspective regarding checking postconditions and preconditions.

Let's consider a pop function for a stack which logical model contents is a Sequence.t. One would like to write something like:

val pop : 'a t -> 'a
(*@ v = pop s
    modifies t.contents
    raises Empty -> t.contents = old t.contents = Sequence.empty
    ensures t.contents = if t.contents = Sequence.empty
                         then Sequence.empty
                         else Sequence.tl (old t.contents)
    ensures v = Sequence.hd (old t.contents)

Now, if by some strange behaviour, the actual implementation of the pop function manages to return a value of type 'a when the given stack is empty, the postcondition will fail with the Partial_function exception and without the benefit of the runnable scenario and the printing of the violated specification part.

Though, I believe that when one writes v = Sequence.hd Sequence.empty, one means false.

I propose to wrap execution of postconditions (in the ortac_postcond function, not in next_state) in a try ... with ... to capture Partial_function and return false instead.

We should also be careful about disjunctions in order to correctly handle a pop function with a default value:

val pop_default : 'a -> 'a t -> 'a
(*@ v = pop_default a s
    modifies t.contents
    ensures t.contents = if t.contents = Sequence.empty
                         then Sequence.empty
                         else Sequence.tl (old t.contents)
    ensures v = Sequence.hd (old t.contents) \/ v = a

One simple way to implement this idea would be to have a second version of Ocaml_of_gospel.term_with_catch that does not generate a raise Ortac_runtime.Partial_function ... but return false instead. Call the latter instead of the former when translating boolean terms when generating the postcond and the precond functions, making sure to translate separately parts of a disjunction and rebuilding it with the translated parts.