diff-containers: Test preconditions, invariants and postconditions for positivity and normality.
#16
Conversation
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
7 tasks
dnadales
reviewed
Feb 8, 2023
jasagredo
reviewed
Feb 8, 2023
jorisdral
force-pushed
the
jdral/diff-containers-test-invariants
branch
from
3c78927 to
65bd594
Compare
* Better explain unresolved sums and subtractions. * Better explain positivity and normality. * Remove duplicate module documentation. * Refactor `isNormalDiffHistory` to use `zip`. * Preserve invariants in shrinkers. * Be more explicit about normality/normal form.
Contributor
Author
|
@dnadales @jasagredo I have added tests for the generators/shrinkers. While writing them, I also realised that "positivity implies normality": a positive diff or diff history is by definition also normal. So I've added a test for that as well, and the documentation now also mentions this |
* Test generators * Remove implications that are no satisfied by generators. * New property: positivity implies normality
jorisdral
force-pushed
the
jdral/diff-containers-test-invariants
branch
from
7d59dff to
47aaf2b
Compare
dnadales
approved these changes
Feb 14, 2023
dnadales
left a comment
dnadales
left a comment
There was a problem hiding this comment.
Thank you! I'm really happy with the tests for the generators
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Precursor reference: #15 (comment)
#15 brought back unsafe constructors in the
diff-containerspackage. A side-effect of this is that we can not hide the internals (Data.Map.Diff.Strict.Internal) behind a truly safe interface (Data.Map.Diff.Strict). Instead, downstream code now has the responsibility to use the semi-safe interface faithfully.What it means to use diffs in a safe way is now documented in the code, amongst others using PRECONDITION, INVARIANT and POSTCONDITION annotations. This PR also introduces tests for these properties.
The invariant for downstream code to uphold is to only ever apply diffs that are both "normal" and "positive". Faithful use of the API should prevent this from happening.
The README that will be added in resolving #8 will explain both the normality and positivity properties, and it will contain examples of use cases.