Specification Slicing for VDM-SL

TL;DR

This paper introduces a specification slicing technique for VDM-SL, enhancing debugging and comprehension of executable formal specifications by adapting program slicing methods.

Contribution

It defines and implements a novel specification slicing method for VDM-SL, facilitating easier debugging and understanding of executable specifications.

Findings

Implemented slicer on ViennaTalk for browser and debugger use

Enables targeted analysis of VDM-SL specifications

Improves readability and debugging of executable specifications

Abstract

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.