For now, Ortac/QCheck-STM doesn't generate tests for functions having multiple
occurrences of sut in the function's parameter.
Extending the test coverage in order to include these functions would be a nice improvement.
The first step would be to have multiple suts at hand when calling a function (with muliple sut arguments).
That raises multiple questions:
where to find the extra suts?
how to compute their models?
how to store them?
Next there is the question of how to trace the modifications of the suts given as argument to a function (meaning changing how the next_state function works)?
And finally, what to do when there is not enough suts at hand to call a function?
Regarding how to get extra suts and their model, I can see two reasonable solutions:
doing something similar to what Monolith does for abstract type
using init_sut and init_state multiple times
As an example for 1:
val sub : 'a array -> int -> int -> 'a array
(*@ res = sub a pos len
ensures res.contents = a.contents[pos..pos+len-1] *)
Here we would store res as a new sut with res.contents as model. Note that this works if we didn't had the size field for the model.
2 would restrict the space explored by the tests, but could well be a fallback solution when we have not enough suts at hand.
Another solution to deal with the lack of suts is to make the command generator aware of how many suts are available.
For now, Ortac/QCheck-STM doesn't generate tests for functions having multiple occurrences of
sut
in the function's parameter.Extending the test coverage in order to include these functions would be a nice improvement.
The first step would be to have multiple
sut
s at hand when calling a function (with muliplesut
arguments).That raises multiple questions:
sut
s?Next there is the question of how to trace the modifications of the
sut
s given as argument to a function (meaning changing how thenext_state
function works)?And finally, what to do when there is not enough
sut
s at hand to call a function?Regarding how to get extra
sut
s and their model, I can see two reasonable solutions:init_sut
andinit_state
multiple timesAs an example for
1
:Here we would store
res
as a newsut
withres.contents
as model. Note that this works if we didn't had thesize
field for the model.2
would restrict the space explored by the tests, but could well be a fallback solution when we have not enoughsut
s at hand.Another solution to deal with the lack of
sut
s is to make the command generator aware of how manysut
s are available.