[AIP-X][Discussion] Move Specification Testing
Closed this issue · 0 comments
AIP Discussion
The Move Specification Testing project aims to check whether the Move formal specifications are complete. As there is no standard solution for testing Move specifications, we propose to create a set of tools that will be able to test Move specifications.
The Move Specification Verification tool (spec-verify) will be responsible for running The Move Mutator tool, which will be able to generate Move programs (mutants) by introducing small changes in the code. Then, they will be passed to the Move Prover and checked if they are valid according to the Move specifications. The number of mutants killed will measure how good the specification is. The tool will also generate appropriate reports.
Read more about it here: #277