Skip to content
This repository has been archived by the owner on Jul 31, 2023. It is now read-only.

Handling of traits #3

Open
alastairreid opened this issue Sep 1, 2020 · 0 comments
Open

Handling of traits #3

alastairreid opened this issue Sep 1, 2020 · 0 comments
Labels
enhancement New feature or request propverify Related to propverify / proptest
Milestone
modular verification

Comments

@alastairreid
Copy link
Contributor

alastairreid commented Sep 1, 2020 •
edited
Loading

At present, traits are handled by testing with specific instances of the trait (see compatibility-test/src/dynamic.rs).
This seems like the only option when fuzzing but, for tools that support modular verification, we would ideally be using a contract for the methods in the trait so that the verification is valid for all possible implementations of the trait, not just the ones that we test with.
@alastairreid alastairreid added the enhancement New feature or request label Sep 1, 2020
@alastairreid alastairreid added this to the modular verification milestone Sep 1, 2020
@alastairreid alastairreid added the propverify Related to propverify / proptest label Sep 13, 2020
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
enhancement New feature or request propverify Related to propverify / proptest
Projects
None yet
Milestone
modular verification
Development

No branches or pull requests
1 participant
@alastairreid