Academic
Publications
Deriving a Slicing Algorithm via FermaT Transformations

Deriving a Slicing Algorithm via FermaT Transformations,10.1109/TSE.2010.13,IEEE Transactions on Software Engineering,Martin P. Ward,Hussein Zedan

Deriving a Slicing Algorithm via FermaT Transformations   (Citations: 2)
BibTex | RIS | RefWorks Download
In this paper we present a case study in deriving an algorithm from a formal specification via FermaT transformations. The general method (which is presented in a separate paper) is extended to a method for deriving an implementation of a program transformation from a specification of the program transformation. We use program slicing as an example transfor- mation, since this is of interest outside the program transformation community. We develop a formal specification for program slicing, in the form of a WSL specification statement, which is refined into a simple slicing algorithm by applying a sequence of general purpose program transformations and refinements. Finally, we show how the same methods can be used to derive an algorithm for semantic slicing. The main novel contributions of this paper are: (1) Developing a formal specification for slicing. (2) Expressing the definition of slicing in terms of a WSL specification statement. (3) By applying correctness preserving transformations to the specification we can derive a simple slicing algorithm. In this paper we present a case study in the derivation of an algorithm from a formal speci- fication. The general derivation method is presented in a separate paper: in this paper we show how the method can be applied to deriving an implementation of a program transformation from a specification of the program transformation. This process is called metatransformation (65) since the program which is being transformed is the source code for another transformation. Previous work by the authors (66) has shown that program slicing, can be formalised as a program transformation. Slicing is of interest outside the field of program transformations so in this paper we will use slicing as a case study in the derivation of a transformation from a specification. We will develop a formal specification for program slicing and use transformations to refine this specification into an implementation. The WSL language and transformation theory is based on infinitary logic: an extension of normal first order logic which allows infinitely long formulae. The application of infinitary logic to specifications and weakest preconditions is central to the method. The main novel contribution of the paper is the derivation of a slicing algorithm from a formal
Journal: IEEE Transactions on Software Engineering - TSE , vol. 37, no. 1, pp. 24-47, 2011
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
Sort by: