Model testing using Qcheck - #21
Merged
Merged
Conversation
The model and the tests were initially developped for Frama-C's Intmap and are not yet exhaustive. The tests consist of: - model.ml implements a data structure that models a Intmap while being much simpler. - symbolic.ml describes operations for building trees and builds random trees using both the model's and patricia-tree's APIs. - test.ml defines and runs Qcheck tests for the API's functions. The tests compare the result computed by patricia-tree and the one computed by the model. They are run with `dune runtest`. Some tests are not passing at this stage: fold (due to the order of iteration) and intersection.
The model doesn't compute the same result as the implementation for any reconciliation function. This is due to optimisations that use physical equality to avoid traversing part of the datastructure.
The result is a list literal containing the test definitions inline. This might not seem like an improvement at first as the list doesn't contain any line break and is uglier than the previous code. It is a time saver however to not have to name each test at the top-level and then to edit the list of tests separately.
Model the behavior when values at the same key are physically equals. It was not correct when `f` returned None. The qcheck arbitrary also contained a bug, the `choose` function uses the printer of the first element (which is not intuitive) and doesn't tries to magically call the right printer.
In the model implementation, same-domain checks and universal quantification are checked separately for readability purpose. Reflexivity of the predicate is guaranteed by wrapping the (not necessarily reflexive) generated one.
This is the same test than for the `reflexive` version, without the wrapping make the predicate reflexive.
The function assumes `f k v v = None`. This is guaranteed here by wrapping the generated function.
- `update` and `mapi`: Cover the case where the new value is physically equal. - `reflexive_compare`: Cover trees with an intersection. - `max_binding_inter`: Fix typo in test definition.
Generate random and intersecting trees more often than identical trees.
Collaborator
|
Thanks for this PR ! Having more tests is always good. There are a few issues remaining though:
|
The only source of incompatibility was the use of Fun.compose, which can be easily avoided. The "with_" combinators are removed as their expansion is trivial.
The model for this function needs to change since the recent change.
Contributor
Author
|
Thanks for your feedback! I've merged main, updated the model for Is it OK if I move the tests in |
Collaborator
|
Yes you're right, having the |
Contributor
Author
|
Hi! I reorganized the tests in the last commit. |
dlesbre
reviewed
Jan 17, 2026
The existing tests are moved into test/property. The new tests are placed into test/model.
Contributor
Author
|
Thanks :) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This adds extensive testing for the API generated by
MakeMapusing Qcheck and model-based testing.These new tests don't replace the existing ones but complete them with a slightly different approach.
We choose to follow the method from QuickChecking Patricia Trees by Jan Midtgaard.
To summarize, the test framework is composed of these parts:
Model: ModelsPatriciaTree's API. The implementation is very simple and we can have good confidence in its correctness by review alone.It can also serve as specification or documentation when developing new operations.
Symbolic: Generate a sequence of operation that construct trees. It is used to generate trees of all shapes and is shrinkable by Qcheck.Test: Defines tests for functions in the API and Qcheck generators for their arguments.Unlike the existing tests, the output of functions is not validated, instead it is compared with the output from the model.
During the development of this PR, we caught a bug (#19) and had a question (#18).
This PR is based on top of #20 so we could monitor the coverage.
According to
bisect_ppx, the test coverage increases from 63% to 83%.