Gospel is moving towards talking only of logical models in the specifications (not OCaml values).
Ortac/QCheck-STM is already using relational postconditions to propose model-based testing (maintaining an implementation of the logical model in parallel of the OCaml value).
There are some clearly identified limitations on taking this approach for Ortac/Wrapper (see section 7.1 of Clément Pascutto PhD dissertation
I propose to take another approach with Ortac/Wrapper, inspired by bisimulation (see also Section 5 of this paper)
A bisimulation is a property on labeled transition systems.
We can see function calls (and the corresponding relational postconditions) as such labels.
We then want to check that:
a ~ m
| |
φ | | σ
V V
a' ~ m'
Where:
a and a' are OCaml values (a' correspond to a after the function call)
m and m' are logical models (m' is old m in Gospel terms)
φ is an OCaml function call
σ is the modification of logical models expressed in a relational postcondition
~ is the relation between OCaml values and logical models that defines the bisimulation and can be implemented with a projection (a to_model function): a ~ m ≡ to_model a = m
Obviously, we can't generate the projection for the user (we mainly deal with abstract types).
Following the same idea as #214, I propose that the user provides these projections in a module-based configuration, relying on a naming convention.
Then, when/before translating the Gospel terms, we will substitute access to a logical model (it is coded as the access to a field in current Gospel) with a call to the right projection.
Whenever a projection is not available, we can skip the Gospel term.
That way, given an interface like this one (in queue.mli file):
type 'a t
(*@ mutable model contents : 'a list *)
val create : unit -> 'a t
(*@ q = create ()
ensures q.contents = [] *)
val push : 'a -> 'a t -> unit
(*@ push a q
modifies q.contents
ensures q.contents = a :: old q.contents *)
Ortac/Wrapper would generate something along the line of:
include Queue
let contents = .... (* taken from the configuration module *)
let create () =
let q = create () in
assert (contents q = []);
q
let push a q =
let q' = copy q in
push a q;
assert (contents q = a :: contents q')
Gospel is moving towards talking only of logical models in the specifications (not OCaml values).
Ortac/QCheck-STM is already using relational postconditions to propose model-based testing (maintaining an implementation of the logical model in parallel of the OCaml value).
There are some clearly identified limitations on taking this approach for Ortac/Wrapper (see section 7.1 of Clément Pascutto PhD dissertation
I propose to take another approach with Ortac/Wrapper, inspired by bisimulation (see also Section 5 of this paper)
A bisimulation is a property on labeled transition systems.
We can see function calls (and the corresponding relational postconditions) as such labels.
We then want to check that:
Where:
a
anda'
are OCaml values (a'
correspond toa
after the function call)m
andm'
are logical models (m'
isold m
in Gospel terms)φ
is an OCaml function callσ
is the modification of logical models expressed in a relational postcondition~
is the relation between OCaml values and logical models that defines the bisimulation and can be implemented with a projection (ato_model
function):a ~ m ≡ to_model a = m
Obviously, we can't generate the projection for the user (we mainly deal with abstract types).
Following the same idea as #214, I propose that the user provides these projections in a module-based configuration, relying on a naming convention.
Then, when/before translating the Gospel terms, we will substitute access to a logical model (it is coded as the access to a field in current Gospel) with a call to the right projection.
Whenever a projection is not available, we can skip the Gospel term.
That way, given an interface like this one (in
queue.mli
file):Ortac/Wrapper would generate something along the line of: