Add support for type invariants

ocaml-gospel / ortac

Runtime assertion checking based on Gospel specifications

https://ocaml-gospel.github.io/ortac/

MIT License

36 stars 10 forks source link

Add support for type invariants #197

Closed n-osborne closed 5 months ago

n-osborne commented 6 months ago

This PR proposes to add checks for type invariants (for sut) in:

postcond in order to guarantee preservation of invariants
init_state in order to check that the user-provided value respects the invariants.

The second one is done in init_state and not init_sut as Gospel invariants are supposed to be talking about the model, not the actual value.

n-osborne commented 6 months ago

This PR is still a draft as the type invariants are placed in an assert in the init_state function. This will cause a crash. We should find a better way to communicate with the user, via QCheck for example.

n-osborne commented 6 months ago

This should close #186

n-osborne commented 6 months ago

Checking for type invariant regaring init_state is now done with QCheck.Test.fail_report This allow to have a nice test failure message from QCheck.

n-osborne commented 5 months ago

Thanks for your suggestions @shym Reworking check_init_state led to some more refactoring, but I believe it is nicer now.