Closed n-osborne closed 5 months ago
For demo purpose, I have pushed this branch with a failing test.
You can then see (with colours):
λ dune build @launchtests
File "plugins/qcheck-stm/test/dune.inc", line 49, characters 0-75:
49 | (rule
50 | (alias launchtests)
51 | (action
52 | (run %{dep:array_stm_tests.exe} -v)))
random seed: 476198396
generated error fail pass / total time test name
[✗] 1 0 1 0 / 1000 0.0s Array STM tests (generating)
--- Failure --------------------------------------------------------------------
Test Array STM tests failed (7 shrink steps):
length
+++ Messages ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Messages for test Array STM tests:
Gospel specification violation in function length
File "array.mli", line 7, characters 12-18:
i = 42
File "array.mli", line 8, characters 12-26:
i = t.size + 1
when executing the following sequence of operations:
length : 16
================================================================================
failure (1 tests failed, 0 tests errored, ran 1 tests)
Thanks!
- I assume you went with
(++)
to get it infix in the generated code? I think I would prefer the fully-qualified call, just like what is done for all the Gospel operators. And I would suggest picking a different one, to avoid the confusion withGospelstdlib.(++)
.
Yes, I went for the infix operator to avoid things like (append (append x y) z)
but the risk of confusion with another function is a good reason to not do that. And if we don't have the infix notation because we qualify (which is reasonable), no reason to not adopt append
.
- This is really quibbling: I noticed various uses of
@\n
, which is better avoided according toFormat
’s documentation. Did you try alternatives (thinking it might make the generated output a bit more robust)?
This is the end-of-line that is mostly used in the project I think. Maybe we can change it with consistency in the whole repo if we find a better candidate.
CI is green, merging. Thanks for the review @shym :-)
This PR improve the state of #188
This PR is based on #197, please consider only the last 7 commits.
Basically, this PR makes
postcond
return the reason of the failure rather than just a boolean, so that we can print the Gospel terms being violated back to the user in case of failing test.This lead to give another implementation of the
STM_Sequential.Make
functor in a newOrtac_runtime_qcheck_stm
package to use this newpostcond
function and build and pass toQCheck
the new failure message.