ocaml-gospel / ortac

Runtime assertion checking based on Gospel specifications
https://ocaml-gospel.github.io/ortac/
MIT License
38 stars 10 forks source link

Add type invariant to postcond #186

Closed n-osborne closed 6 months ago

n-osborne commented 8 months ago

Gospel type invariants are talking about models. As we only build the model of the type sut (and call it state), we can only check invariants on state

jmid commented 8 months ago

Ah, good point. Perhaps simply asserting the invariant in run (where a sut is available) could work instead, since run is set up to handle side-effects (such as an assertion failure)? :thinking: Generally I'm thinking that we would want to check the invariant initially (where?) and for preservation across each cmd execution...

n-osborne commented 8 months ago

I believe a sut is available both in precond and postcond. My point was that if the library has two types, both with gospel type invariants, there is no need to collect the invariants for the non-sut type as we don't have a model to check them against for this type. (My first though and experiment was to check invariants for all the types in the library).

Checking for preservation of invariants, I'm currently implementing checking them in the postcond function. Regarding the initial value, as it is provided by the user in the init_sut value we can either wrap this value in a check for invariants, or assume that it is the user responsability. I think it is not costly enough to not check it.

jmid commented 8 months ago

I believe a sut is available both in precond and postcond.

Nope, unfortunately not: https://ocaml-multicore.github.io/multicoretests/0.3/qcheck-stm/STM/module-type-Spec/index.html

val precond : cmd -> state -> bool
val postcond : cmd -> state -> res -> bool

...but yes it seems I misunderstood you :slightly_smiling_face:

n-osborne commented 6 months ago

Closed by #197