Add support for type invariants #197
Conversation
|
This PR is still a draft as the type invariants are placed in an |
|
This should close #186 |
n-osborne
force-pushed
the
qcheck-stm-with-invariants
branch
2 times, most recently
from
e9490b9 to
d718ed2
Compare
|
Checking for type invariant regaring |
n-osborne
force-pushed
the
qcheck-stm-with-invariants
branch
3 times, most recently
from
11c3244 to
5bf542e
Compare
n-osborne
force-pushed
the
qcheck-stm-with-invariants
branch
from
5bf542e to
cda7ce7
Compare
There was a problem hiding this comment.
This looks very good, well done!
Still, I managed to find a couple of suggestions 😄
- Is the fact that the function is named
wrapped_init_statepart of a bigger plan, because, as this PR stands, it is used only to check the initial state and its result is always discarded. In the present state, I would then suggest renaming it ascheck_init_stateand giving it the typeunit -> unit.agree_propcould then use a simple sequencecheck_init_state (); .... - I noticed that
invariants_errors.expectedappears before theinvariants.mliis created. I would suggest squashing the “Check type invariants ininit_state” and “Add some tests” commits.
I also put smaller comments on some lines, they were harder to describe without context.
| @@ -383,8 +377,8 @@ let ghost_functions = | |||
| let run sigs config = | |||
| let open Reserr in | |||
| let open Ir in | |||
| let* state = state config sigs in | |||
| let* state, invariants = state config sigs in | |||
There was a problem hiding this comment.
This line reads a bit funny. I suggest renaming the state function as state_and_invariants.
| @@ -159,7 +159,15 @@ module Spec = | |||
| match cmd__010_ with | Get -> Res (int, (get sut__011_)) | |||
| end | |||
| module STMTests = (STM_sequential.Make)(Spec) | |||
| let wrapped_init_state () = | |||
| let __state__012_ = Spec.init_state in | |||
| if true | |||
There was a problem hiding this comment.
This makes me wonder: should the test deciding to generate a non-trivial wrapped_init_state rather be whether we have some invariants to test after translation, rather than Option.is_some at the beginning?
plugins/qcheck-stm/src/stm_of_ir.ml
Outdated
| @@ -843,11 +895,16 @@ let stm include_ config ir = | |||
| let descr = estring (module_name ^ " STM tests") in | |||
| [%stri | |||
| let _ = | |||
| let open QCheck in | |||
There was a problem hiding this comment.
Is QCheck necessary for more than just Test.make? If not, I would rather go with QCheck.Test.make.
Mostly add `list_or` and `enot` that will soon be needed, but take the opportunity to move `qualify` and redefine some functions that where worngfully using `evar` on qualified names.
This will guarantee preservation of type invariants for `sut`
n-osborne
force-pushed
the
qcheck-stm-with-invariants
branch
from
cda7ce7 to
15bfd2c
Compare
|
Thanks for your suggestions @shym |
This PR proposes to add checks for type invariants (for sut) in:
postcondin order to guarantee preservation of invariantsinit_statein order to check that the user-provided value respects the invariants.The second one is done in
init_stateand notinit_sutas Gospel invariants are supposed to be talking about the model, not the actual value.