Specification Slicing for VDM-SL

TL;DR

The paper addresses the challenge of reading and debugging executable VDM-SL specifications that employ imperative state updates. It introduces a formal notion of static backward specification slices for VDM-SL and implements a slicer within ViennaTalk, enabling extraction of relevant code fragments from operations with respect to a given slicing criterion. The contributions include a precise slice definition, a dependency-driven slicing algorithm for expressions, assignments, patterns, and control structures, and practical demonstrations in debugging and refactoring workflows. The work improves maintainability and correctness of formal specifications by isolating dependencies and facilitating targeted edits, with potential for reuse of library fragments and broader tool support.

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.

Figures (15)

• Figure 1: An example static backward slice
• Figure 2: Pseudo-code of the variables in the slicer and their initialization
• Figure 3: Pseudo-code of the overview of how the slicer process each AST node
• Figure 4: Pseudo-code of processing binary operator expressions
• Figure 5: Pseudo-code of processing assignment statements