Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(13)
Algorithm Design
Case Study
Formal Method
Formal Specification
General Methods
Generalized Derivation
Probability Density Function
Program Slicing
Program Transformation
Reverse Engineering
Source Code
Weakest Precondition
First Order Logic
Subscribe
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
Edit
Deriving a Slicing Algorithm via FermaT Transformations
(
Citations: 2
)
BibTex

RIS

RefWorks
Download
Martin P. Ward
,
Hussein Zedan
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. 2447, 2011
DOI:
10.1109/TSE.2010.13
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.
(
ieeexplore.ieee.org
)
(
www.cse.dmu.ac.uk
)
(
www.informatik.unitrier.de
)
(
dx.doi.org
)
(
ieeexplore.ieee.org
)
(
www.tech.dmu.ac.uk
)
(
www.gkc.org.uk
)
(
ieeexplore.ieee.org
)
More »
References
(77)
Revised Report on the Algorithmic Language Scheme
(
Citations: 98
)
Harold Abelson
,
R. Kent Dybvig
,
Christopher T. Haynes
,
Guillermo Juan Rozas
,
N. I. Adams IV
,
Daniel P. Friedman
,
Eugene E. Kohlbecker
,
Guy L. Steele Jr.
,
David H. Bartley
,
Robert H. Halstead Jr.
,
Don Oxley
,
Gerald J. Sussman
http://academic.research.microsoft.com/io.ashx?type=5&id=798556&selfId1=0&selfId2=0&maxNumber=12&query=
Journal:
Higherorder and Symbolic Computation / Lisp and Symbolic Computation
, vol. 11, no. 1, pp. 7105, 1998
Correctness Preserving Program Re炉nements
(
Citations: 24
)
R. J. R. Back
Published in 1980.
A Calculus of Refinements for Program Derivations
(
Citations: 185
)
Ralphjohan Back
Journal:
Acta Informatica  ACTA
, vol. 25, no. 6, pp. 593624, 1988
Refinement Concepts Formalized in Higher Order Logic
(
Citations: 42
)
R. j. r. Back
,
J. Von Wright
Journal:
Formal Aspects of Computing  FAC
, 1989
Formal Construction by Transformation  Computer Aided Intuition Guided Programming
(
Citations: 16
)
F. L. Bauer
,
B. Moller
,
H. Partsch
,
P. Pepper
Journal:
IEEE Transactions on Software Engineering  TSE
, 1989
Sort by:
Citations
(2)
Combining dynamic and static slicing for analysing assembler
(
Citations: 1
)
Martin P. Ward
,
Hussein Zedan
Journal:
Science of Computer Programming  SCP
, vol. 75, no. 3, pp. 134175, 2010
Transformational Programming and the Derivation of Algorithms
Martin Ward
,
Hussein Zedan