Specification Slicing for VDM-SL
<|reference_start|>Specification Slicing for VDM-SL: The executable specification is one of the powerful tools in lightweight formal software development. VDM-SL allows the explicit and executable definition of operations that reference and update internal state through imperative statements. While the extensive executable subset of VDM-SL enables validation and testing in the specification phase, it also brings difficulties in reading and debugging as in imperative programming. In this paper, we define specification slicing for VDM-SL based on program slicing, a technique used for debugging and maintaining program source code in implementation languages. We then present and discuss its applications. The slicer for VDM-SL is implemented on ViennaTalk and can be used on browsers and debuggers describing the VDM-SL specification.<|reference_end|>
@article{oda2024specification,
    title={Specification Slicing for VDM-SL},
    author={Tomohiro Oda and Han-Myung Chang},
    journal={arXiv preprint arXiv:2410.03180},
    year={2024},
    number={OVT22/2024/02},
    archivePrefix={arXiv},
    eprint={2410.03180},
    primaryClass={cs.SE}
}