Papers by Martin Ward

[Home] [Publications] [Software] [G.K. Chesterton] [GKC books] [GKC pictures]

Click on any title to download a gzipped PostScript file with the full text of the paper.

All papers also have PDF versions, click on the (PDF) link after the title.

Papers are listed in chronological order of publication, so the most recent papers are at the end.

Creative Commons License
These works are licenced under a Creative Commons Licence.


Proving Program Refinements and Transformations,
M. Ward
DPhil Thesis, Oxford University, 1989

Abstract

In this thesis we develop a theory of program refinement and equivalence which can be used to develop practical tools for program development, analysis and modification. The theory is based on the use of general specifications and an imperative kernel language. We use weakest preconditions, expressed as formulae in infinitary logic to prove refinement and equivalence between programs.

The kernel language is extended by means of ``definitional transformations'' which define new concepts in terms of those already present. The extensions include practical programming constructs, including recursive procedures, local variables, functions and expressions with side-effects. This expands the language into a ``Wide Spectrum Language'' which covers the whole range of operations from general specifications to assignments, jumps and labels. We develop theorems for proving the termination of recursive and iterative programs, transforming specifications into recursive programs and transforming recursive procedures into iterative equivalents. We develop a rigorous framework for reasoning about programs with EXIT statements that terminate nested loops from within; and this forms the basis for many efficiency-improving and restructuring transformations. These are used as a tool for program analysis and to derive algorithms by transforming their specifications. We show that the methods of top-down design and program verification using assertions can be viewed as the application of a small subset of transformations.


Transforming a Program into a Specification (PDF)
M. Ward
Durham University Computer Science Technical Report 88-1, Jan 1988.

Abstract

There has been much research in recent years on the problems of program and system development but very little work has been done on the problems of maintaining developed programs. This is despite the fact that for many years it has been well-known that maintenance consumes the largest percentage of the programming budget. We apply the techniques of program transformation to a published program which was written in such a way that the structure and effect of the program are very hard to discern. This will reveal the true structure of the program and enable its effect to be summarised as a specification. The method is language-independent and so can be used with a wide variety of programming languages, the same method can be used to derive a program from a specification, transform a program from one language to another, and (as illustrated here), to transform a program into a specification.

A Knowledge-Based System for Software Maintenance, (PDF)
F. Callis, M. Khalil, M. Munro and M. Ward
Conference on Software Maintenance 1988, Phoenix, Arizona
October 24-27, 1988.

Abstract

A description of an Intelligent, Knowledge-Based maintenance tool, being developed by the Centre for Software Maintenance at the University of Durham is described. The tool is intended to help reduce the amount of time spent on analysing code. Code analysis is performed when a programmer is familiarising himself with a piece of code, and when the effects of a proposed modification of the code is being assessed.

The Maintainer's Assistant (PDF)
M. Ward, F. Callis and M. Munro
Conference on Software Maintenance 1989, Miami Beach, Florida,
October 16th-19th 1989.

Abstract

The Maintainer's Assistant is a code analysis tool aimed at helping the maintenance programmer to understand and modify a given program. Program transformation techniques are employed by the Maintainer's Assistant both to derive a specification from a section of code and to transform a section of code into a logically equivalent form. The general structure of the tool is described and two examples of the application of program transformations are given.

Derivation of a Sorting Algorithm (PDF)
M. Ward
Technical Report
Durham University, November 1990

Abstract

We derive a hybrid sorting algorithm (a combination of Quicksort and insertion sort which combines the best features of both algorithms) from a formal specification of sorting via a sequence of correctness-preserving program transformations.

A Recursion Removal Theorem -- Proof and Applications (PDF)
M. Ward
Technical Report
Durham University 1991

Abstract

In this paper we briefly introduce a Wide Spectrum Language and its transformation theory and describe a recent success of the theory: a general recursion removal theorem. This theorem includes as special cases the two techniques discussed by Knuth and Bird. We describe some applications of the theorem to cascade recursion, binary cascade recursion, Gray codes, the Towers of Hanoi problem, and an inverse engineering problem.

Using Formal Transformations to Construct a Component Repository (PDF)
M. Ward
In: "Software Reuse: the European Approach", Springer-Verlag, Feb 1991

Abstract

This paper discusses how theoretical results from the field of program transformations can be applied to develop a new approach to software reuse. We describe a model for the semantics of nondeterministic programs and specifications and use this model to show how refinements and transformations of programs and specifications can be proved correct by reference to their corresponding _Weakest_Preconditions_ expressed as formulae in infinitary first order logic. We then show how this theory of program refinements and transformations (which is further developed in [.Ward thesis.]) can be applied to the construction of a repository of reusable components consisting of code, specifications, documentation and development methods. These components are linked together in such a way that specifications and their implementations can be extracted easily.

A Recursion Removal Theorem (PDF)
M. Ward
BCS Refinement Workshop, 8-11 Jan 1992

Abstract

In this paper we briefly introduce a Wide Spectrum Language and its transformation theory and describe a recent success of the theory: a general recursion removal theorem. Recursion removal often forms an important step in the systematic development of an algorithm from a formal specification. We use semantic-preserving transformations to carry out such developments and the theorem proves the correctness of many different classes of recursion removal. This theorem includes as special cases the two techniques discussed by Knuth [.Knuth goto.] and Bird [.Bird recursion removal.]. We describe some applications of the theorem to cascade recursion, binary cascade recursion, Gray codes, and an inverse engineering problem.

Abstracting a Specification from Code (PDF)
M. Ward
Journal of Software Maintenance: Research and Practice,
Vol 5, 1993, pp 101-122

Abstract

Much of the work on developing program transformation systems has concentrated on systems to assist in program development. However, the four separate surveys carried out between 1977 and 1990, summarised in [.Foster.], show that between 40% and 60% of all commercial software effort is devoted to software maintenance rather than the development of new systems. In this paper we describe a joint project between the University of Durham and CSM Ltd to develop a method and tool for reverse engineering and software maintenance based on program transformation theory. We present an example which illustrates how such a tool can extract a high-level abstract specification from the low-level source code of a program by a process of formal program transformation based on a theory of program equivalence [.Ward thesis.]. All the code-level reverse engineering of the example program was carried out on the prototype tool with the resulting code pasted directly into the paper.

Iterative Procedures for Computing Ackerman's Function
(PDF)
M. Ward
Technical Report
Durham University, July 1993

Abstract

This paper uses Ackerman's function as a testbed to illustrate the operation of various program transformations which take recursive procedures to equivalent iterative forms. The transformations are taken from the author's DPhil thesis [.Ward89.]. In this paper we illustrate that they can be successfully applied to even the most convoluted recursion. For many programs a recursive function is the most natural and clear specification while an iterative (or tail-recursive) form is the most efficient implementation. This paper illustrates how an efficient iterative program can be developed and verified by starting with a simple recursive program and using proven transformations to remove the recursion. The resulting iterative program will be correct by construction, so the problem of a direct verification of the iterative algorithm is avoided. This process can also throw light on the nature of the recursive specification. Several interesting properties of Ackermann's function and the iterative algorithms are derived in the course of this development.

A Practical Program Transformation System (PDF)
M. Ward and K.H. Bennett
Working Conference on Reverse Engineering, 21st-22nd May 1993, Baltimore

Abstract

Program transformation systems provide one means of formally deriving a program from its specification. The main advantage of this development method is that the executable program is correct by construction. In this paper we describe a tool called ReForm which is designed to address the inverse problem to support the extraction of a specification from existing program code, using transformations. This is an important activity during software maintenance. One of the problems of transformation systems is the scarcity of practical tools which can address industrial scale problems, rather than contrived laboratory ``toy'' problems. The main contribution of this paper is an analysis of the important software engineering factors that contribute to a successful transformation based tool. Results from using the tool are also presented.

Understanding Concurrent Programs using Program Transformations (PDF)
E.J. Younger and M. Ward
Proceedings of the 1993 2nd Workshop on Program Comprehension,
8th-9th July 1993, Capri, Italy

Abstract

Reverse engineering of concurrent real-time programs with timing constraints is a particularly challenging research area, because the functional behaviour of a program, and the non-functional timing requirements, are implicit and can be very difficult to discover. In this paper we present a significant advance in this area, which is achieved by modelling real-time concurrent programs in the wide spectrum language WSL. We show how a sequential program with interrupts can be modelled in WSL, and the method is then extended to model more general concurrent programs. We show how a program modelled in this way may subsequently be ``inverse engineered'' by the use of formal program transformations, to discover a specification for the program. (We use the term ``inverse engineering'' to mean ``reverse engineering achieved by formal program transformations'').

Specifications from Source Code — Alchemists' Dream or Practical Reality? (PDF)
M. Ward
4th Reengineering Forum, September 19-21, 1994, Victoria, Canada

Abstract

We describe a method for extracting high-level specifications from unstructured source code. The method is based on a theory of program refinement and transformation, which is used as the bases for the development of a catalogue of powerful semantics-preserving transformations. Each transformation is an operation on a program which has a mechanically-checkable correctness condition, and which has been rigorously proved to produce a semantically equivalent result. The transformations are carried out in a wide spectrum programming language (called WSL). This language includes high-level specifications as well as low-level programming constructs. As a result, the formal reverse engineering process (from source code to equivalent specifications) and the redevelopment process (refinement of specifications into source code) can both be carried out within a single language and transformation theory. We also discuss a tool (FermaT) which has been developed to support this approach to reengineering. The tool is a program transformation system, largely written in an extension to WSL called MetaWSL. Thus it is possible to use the tool in the maintenance of its own source code, and this is starting to be the case.

Reverse Engineering through Formal Transformation (PDF)
M. Ward
The Computer Journal, Vol 37, No 9, 1994, pp 795-813
doi:10.1093/comjnl/37.9.795

Abstract

In this paper we will take a detailed look at a larger example of program analysis by transformation. We will be considering Algorithm 2.3.3.A from Knuth's ``Fundamental Algorithms'' [.Knuth Fundamental Algorithms.] (P.357) which is an algorithm for the addition of polynomials represented using four-directional links. [.Knuth 74.] describes this as having ``a complicated structure with excessively unrestrained \keyword{goto} statements'' and goes on to say ``I hope someday to see the algorithm cleaned up without loss of its efficiency''. Our aim is to manipulate the program, using semantics-preserving operations, into an equivalent high-level specification. The transformations are carried out in the WSL language, a ``wide spectrum language'' which includes both low-level program operations and high level specifications, and which has been specifically designed to be easy to transform.

A Multipurpose Backtracking Algorithm (PDF)
H.A. Priestley and M.P. Ward
Journal of Symbolic Computation, 18, pp 1-40, 1994
doi:10.1006/jsco.1994.1035

Abstract

A backtracking algorithm with element order selection is presented, and its efficiency discussed in relation both to standard examples and to examples concerning relation preserving maps which the algorithm was derived to solve.

The source code is available.


Language Oriented Programming (PDF)
M. Ward
Software---Concepts and Tools, 15, pp 147-161, 1994

Abstract

This paper describes the concept of LANGUAGE ORIENTED PROGRAMMING which is a novel way of organising the development of a large software system, leading to a different structure for the finished product. The approach starts by developing a formally specified, domain-oriented, very high-level language which is designed to be well-suited to developing ``this kind of program''. The development process then splits into two independent stages: (1) Implement the system using this ``middle level'' language, and (2) Implement a compiler or translator or interpreter for the language, using existing technology. The approach is claimed to have advantages for domain analysis, rapid prototyping, maintenance, portability, user-enhanceable systems, reuse of development work, while also providing high development productivity. We give an example where the method has been used very successfully (in conjunction with rapid prototyping) in the development of a large software system: the FermaT reverse engineering tool. A major benefit of this approach to software development, as compared to the usual sequential ``waterfall model'' is the speed with which products can be brought to market. This is due to ``concurrent engineering'': the effective overlap of development stages. Finally, the ``middle out'' development style is compared and contrasted with the more usual ``top down'', ``bottom up'' and ``outside in'' development methods.

Inverse Engineering a simple Real Time program (PDF)
E. J. Younger and M. Ward
Journal of Software Maintenance: Research and Practice,
Vol 6, 1993, pp 197-234
doi:doi.wiley.com/10.1002/smr.4360060404

Abstract

Reverse engineering of interrupt-driven real-time programs with timing constraints is a particularly challenging research area, because the functional behaviour of a program, and the non-functional timing requirements, are implicit and can be very difficult to discover. However, in this paper we present a significant advance in this area, which is achieved by modelling real-time programs with interrupts in the wide spectrum language WSL. A small example program is modelled in this way, and formal program transformations are used to derive various timing constraints and to ``inverse engineer'' a formal specification of the program. (We use the term ``inverse engineering'' to mean ``reverse engineering achieved by formal program transformations'').

Foundations for a Practical Theory of Program Refinement and Transformation (PDF)
Martin Ward
Durham University Technical Report,
1994

Abstract

A wide spectrum language is presented, which is designed to facilitate the proof of the correctness of refinements and transformations. Two different proof methods are introduced and used to prove some fundamental transformations, including a general induction rule which enables transformations of recursive and iterative programs to be proved by induction on their finite truncations. A theorem for proving the correctness of recursive implementations is presented, which provides a method for introducing a loop, without requiring the user to provide a loop invariant. A powerful, general purpose, transformation for removing or introducing recursion is described and used in a case study in which we take a small, but highly complex, program and apply formal transformations in order to uncover an abstract specification of the behaviour of the program. The transformation theory supports a transformation system, called FermaT, in which the applicability conditions of each transformation (and hence the correctness of the result) are mechanically verified. These results together considerably simplify the construction of viable program transformation tools; practical consequences are briefly discussed.

Formal Methods for Legacy Systems (PDF)
M. Ward and K.H. Bennett
Journal of Software Maintenance: Research and Practice,
Vol 7, no 3, May-June 1995, pp 203-219
doi:10.1002/smr.4360070305

Abstract

A method is described for obtaining useful information from legacy code. The approach uses formal proven program transformations, which preserve or refine the semantics of a construct while changing its form. The applicability of a transformation in a particular syntactic context is checked before application. By using an appropriate sequence of transformations, the extracted representation is guaranteed to be equivalent to the code. In this paper, we focus on the results of using this approach in the reverse engineering of medium scale, industrial software, written mostly in languages such as assembler and JOVIAL. Results from both benchmark algorithms and heavily modified, geriatric software are summarised. It is concluded that the approach is viable, for self contained code, and that useful design information may be extracted from legacy systems at economic cost. We conclude that formal methods have an important practical role in the reverse engineering process.

Formal Methods to Aid the Evolution of Software (PDF)
M. Ward and K.H. Bennett
International Journal of Software Engineering and Knowledge Engineering,
Special Issue on "Software Evolution", Vol 5, No 1, pp 25-47 1995
doi:dx.doi.org/10.1142/S0218194095000034

Abstract

There is a vast collection of operational software systems which are vitally important to their users, yet are becoming increasingly difficult to maintain, enhance and keep up to date with rapidly changing requirements. For many of these so called LEGACY SYSTEMS the option of throwing the system away an rewriting it from scratch is not economically viable. Methods are therefore urgently required which enable these systems to evolve in a controlled manner. The approach described in this paper uses formal proven program transformations, which preserve or refine the semantics of a program while changing its form. These transformations are applied to restructure ans simplify the legacy systems and to extract higherlevel representations. By using an appropriate sequence of transformations, the extracted representation is guaranteed to be equivalent to the code. The method is based on a formal wide spectrum language, called WSL, with accompanying formal method. Over the last ten years we have developed a large catalogue of proven transformations, together with mechanically verifiable applicability conditions. These have been applied to many software development, reverse engineering and maintenance problems.

A Definition of Abstraction (PDF)
M. Ward
Journal of Software Maintenance: Research and Practice,
Vol 7, no 6, Nov-Dec 1995, pp 443-450
doi:10.1002/smr.4360070606

Abstract

What does it mean to say that one program is "more abstract" then another? What is "abstract" about an abstract data type? What is the difference between a "high-level" program and a "low-level" program? In this paper we attempt to answer these questions by formally defining an abstraction relation between programs which matches our intuitive ideas about abstraction. The relation is based on examining the operational semantics of the programs, expressed as a set of traces (sequences of states) from a given initial state to a possible final state.

Note: This paper was updated on 9th April 1996


Derivation of Data Intensive Algorithms by Formal Transformation
--The Schorr-Waite Graph Marking Algorithm
(PDF)
M. Ward
IEEE Transactions on Software Engineering,
Vol 22, No 9, Sept 1996, pp 665-686
doi:doi.ieeecomputersociety.org/10.1109/32.541437

Abstract

In this paper we consider a particular class of algorithms which present certain difficulties to formal verification. These are algorithms which use a single data structure for two or more purposes, which combine program control information with other data structures or which are developed as a combination of a basic idea with an implementation technique. Our approach is based on applying proven semantics-preserving transformation rules in a wide spectrum language. Starting with a set theoretical specification of ``reachability'' we are able to derive iterative and recursive graph marking algorithms using the ``pointer switching'' idea of Schorr and Waite. There have been several proofs of correctness of the Schorr-Waite algorithm, and a small number of transformational developments of the algorithm. The great advantage of our approach is that we can derive the algorithm from its specification using only general-purpose transformational rules: without the need for complicated induction arguments. Our approach applies equally well to several more complex algorithms which make use of the pointer switching strategy, including a hybrid algorithm which uses a fixed length stack, switching to the pointer switching strategy when the stack runs out.

Program Analysis by Formal Transformation (PDF)
M. Ward
The Computer Journal,
Vol 39, No 7, 1996, ISSN 0010-4620
doi:10.1093/comjnl/39.7.598

Abstract

This paper treats Knuth and Szwarcfiter's topological sorting program, presented in their paper ``A Structured Program to Generate All Topological Sorting Arrangements'', as a case study for the analysis of a program by formal transformations. This algorithm was selected for the case study because it is a particularly challenging program for any reverse engineering method. Besides a complex control flow, the program uses arrays to represent various linked lists and sets, which are manipulated in various ``ingenious'' ways so as to squeeze the last ounce of performance from the algorithm. Our aim is to manipulate the program, using semantics-preserving operations, to produce an abstract specification. The transformations are carried out in the WSL language, a ``wide spectrum language'' which includes both low-level program operations and high level specifications, and which has been specifically designed to be easy to transform.

Assembler to C Migration using the FermaT Transformation System (PDF)
M. Ward
International Conference on Software Maintenance,
30th Aug – 3rd Sept 1999, Oxford, England.

Abstract

The FermaT transformation system, based on research carried out over the last twelve years at Durham University and Software Migrations Ltd., is an industrial-strength formal transformation engine with many applications in program comprehension and language migration. This paper describes one application of the system: the migration of IBM 370 Assembler code to equivalent, maintainable C code. We present an example of using the tool to migrate a small, but complex, assembler module to C with no manual intervention required. We briefly discuss a mass migration exercise where 1,925 assembler modules were sucessfully migrated to C code.

Recursion Removal/Introduction by Formal Transformation: An Aid to Program Development and Program Comprehension (PDF)
M. Ward and K. H. Bennett
The Computer Journal,
Vol 42, No 8, pp 650-673, 1999, ISSN 0010-4620
doi:10.1093/comjnl/42.8.650

Abstract

The transformation of a recursive program to an iterative equivalent is a fundamental operation in Computer Science. In the reverse direction, the task of reverse engineering (analysing a given program in order to determine its specification) can be greatly ameliorated if the program can be re-expressed in a suitable recursive form. But the existing recursion removal transformations, such as the techniques discussed by Knuth [.Knuth goto.] and Bird [.Bird recursion removal.], can only be applied in the reverse direction if the source program happens to match the structure produced by a particular recursion removal operation. In this paper we describe a much more powerful recursion removal and introduction operation which describes its source and target in the form of an action system (a collection of labels and calls to labels). A simple, mechanical, restructuring operation can be applied to a great many iterative programs which will put them in a suitable form for recursion introduction. Our transformation generates strictly more iterative versions than the standard methods, including those of Knuth and Bird [.Knuth goto, Bird recursion removal.]. With the aid of this theorem we prove a (somewhat counterintuitive) result for programs that contain sequences of two or more recursive calls: under a reasonable commutativity condition, ``depth-first'' execution is more general than ``breadth-first'' execution. In ``depth-first'' execution, the execution of each recursive call is completed, including all sub-calls, before execution of the next call is started. In ``breadth-first'' execution, each recursive call in the sequence is partially executed but any sub-calls are temporarily postponed. This result means that any breadth-first program can be reimplemented as a corresponding depth-first program, but the converse does not hold. We also treat the case of ``random-first'' execution, where the execution order is implementation dependent. For the more restricted domain of tree searching we show that breadth first search is the most general form. We also give two examples of recursion introduction as an aid to formal reverse engineering.

Reverse Engineering from Assembler to Formal Specifications via Program Transformations (PDF)
M. Ward
7th Working Conference on Reverse Engineering,
23-25th November 2000, Brisbane, Queensland, Australia
IEEE Computer Society

Abstract

The FermaT transformation system, based on research carried out over the last sixteen years at Durham University, De Montfort University and Software Migrations Ltd., is an industrial-strength formal transformation engine with many applications in program comprehension and language migration. This paper is a case study which uses automated plus manually-directed transformations and abstractions to convert an IBM 370 Assembler code program into a very high-level abstract specification.

The FermaT Assembler Re-engineering Workbench (PDF)
M. Ward
International Conference on Software Maintenance 2001,
6th-9th November 2001, Florence, Italy
IEEE Computer Society

Abstract

Research into the working practices of software engineers has shown the need for integrated browsing and searching tools which include graphical visualisations linked back to the source code under investigation. In addition, for assembler maintenance and re-engineering there is an even greater need for sophisticated control flow analysis, data flow analysis, slicing and migration technology. All these technologies are provided by the FermaT Workbench: an industrial-strength assembler re-engineering workbench consisting of a number of integrated tools for program comprehension, migration and re-engineering. The various program analysis and migrations tools are based on research carried out over the last sixteen years at Durham University, De Montfort University and Software Migrations Ltd., and make extensive use of program transformation theory.

The Formal Transformation Approach to Source Code Analysis and Manipulation (PDF)
M. Ward
Keynote speech at the First International Workshop on Source Code Analysis and Manipulation,
10th November 2001, Florence, Italy
IEEE Computer Society

Abstract

In this paper we give a brief introduction to the foundations of WSL transformation theory and describe some applications to program slicing. We introduce some generalisations of traditional slicing, amorphous slicing and conditioned slicing, which are possible in the framework of WSL transformations. One generalisation is ``semantic slicing'' which combines slicing and abstraction to a specification.

ConSUS: A Scalable Approach to Conditioned Slicing (PDF)
M. Daoudi, L. Ouarbya, J. Howroyd, S. Danicic, Mark Harman, Chris Fox, M. P. Ward
9th IEEE Working Conference on Reverse Engineering, 2002.
October 28 - November 1, 2002 Richmond, Virginia, USA
IEEE Computer Society

Abstract

Conditioned slicing can be applied to reverse engineering problems which involve the extraction of executable fragments of code in the context of some criteria of interest. This paper introduces ConSUS, a conditioner for the Wide Spectrum Language, WSL. The symbolic executor of ConSUS prunes the symbolic execution paths, and its predicate reasoning system uses the FermaT Simplify transformation in place of a more conventional theorem prover. We show that this combination of pruning and simplification-as-reasoner leads to a more scalable approach to conditioning.

Program Slicing via FermaT Transformations (PDF)
M. Ward
COMPSAC 2002,
26th Annual International Computer Software and Applications Conference
Oxford, England, 26th-29th August 2002
IEEE Computer Society

Abstract

In this paper we describe how the concept of program slicing can be formalised in WSL transformation theory. This formalism naturally lends itself to several generalisations including amorphous slicing and conditioned slicing. One novel generalisation is ``semantic slicing'' which combines slicing and abstraction to a specification. Interprocedural semantic slicing has been implemented in the FermaT transformation system: an industrial-strength transformation system designed for forward and reverse engineering, re-engineering and program comprehension.

Successful Evolution of Software Systems (PDF) (Compiled HTML Help) (Download from archive.org)
Hongji Yang and Martin Ward
ISBN 1-58053-349-3
294 pages.
Artech House (20 December 2002)

Publisher's Blurb

In today's fast-changing, competitive environment, having an up-to-date information system (IS) is critical for all companies and institutions. Rather than creating a new system from scratch, reengineering is an economical way to develop an IS to match changing business needs. Using detailed examples, this practical book gives you methods and techniques for reengineering systems for flexibility and reliability. It helps you reengineer a system to continue to provide for business critical missions as well as achieve a smooth transformation to an up-to-date software technology environment. What's more, it shows you how to redevelop a flexible system that can evolve to meet future business objectives, reduce start time and save money in the reengineering process.

This unique resource places particular emphasis on the reengineering of legacy assembler systems using the FermaT workbench, and describes other widely available general techniques. The book poses the key questions that you need to address before reengineering can provide an integrated framework that reveals the answers. A built workbench is used to illustrate the approach with the application of real case studies.

Contents:

Constant Software Changes - Legacy Systems. Business Changes. Software Evolution.

Software Engineering and Software Maintenance - Software and Software Engineering. Software Maintenance. Summary.

Software Reengineering - Introduction. Taxonomy of Software Reengineering. Reverse Engineering. Issues of Reverse Engineering. Current State of Formal Methods in Reengineering. Classification of Formal Methods. Criteria and Results. Analysis and Summary.

An Integrated Reengineering Framework - Characteristics of Legacy Systems. The Reengineering Approach. Wide Spectrum Language.

Process for Reengineering - A system Architecture for Implementing the Process of Reengineering. Abstracting. Translation of Source Code to an Intermediate Representation. Restructuring. Elicitating Business Rules. Abstraction and Abstraction Patterns. Reusing Components. Retargeting. Measuring Reegineering.

Reengineering Workbench - FermaT Workbench.

Case Studies. Conclusions. References.


ConSUS: A Light-Weight Program Conditioner (PDF)
Sebastian Danicic, Mohammed Daoudi, Chris Fox, Mark Harman, Rob M. Hierons, John R. Howroyd, Lahcen Ourabya and Martin Ward
Journal of Systems and Software (Elsevier),
Volume 77, Issue 3, September 2005, Pages 241-262.
doi:10.1016/j.jss.2004.03.034

Abstract

Program conditioning consists of identifying and removing a set of statements which cannot be executed when a condition of interest holds at some point in a program. It has been applied to problems in maintenance, testing, re-use and re-engineering. Program conditioning relies upon both symbolic execution and reasoning about symbolic predicates. Automation of the process therefore requires some form of automated theorem proving. However, the use of a full-power `heavyweight' theorem prover would impose unrealistic performance constraints.

This paper reports on a lightweight approach to theorem proving using the FermaT simplify decision procedure. This is used as a component to ConSUS, a program conditioning system for the Wide Spectrum Language WSL. The paper describes the symbolic execution algorithm used by ConSUS, which prunes as it conditions.

The paper also provides empirical evidence that conditioning produces a significant reduction in program size and, although exponential in the worst case) the conditioning system, has low degree polynomial behaviour in many cases, thereby making it scalable to unit level applications of program conditioning.


Slicing the SCAM Mug: A Case Study in Semantic Slicing (PDF)
Martin Ward
Third IEEE International Workshop on Source Code Analysis and Manipulation,
27th September 2003, Amsterdam, Netherlands.
IEEE Computer Society

Abstract

In this paper we describe an improved formalisation of slicing in WSL transformation theory and apply the result to a particularly challenging slicing problem: the SCAM mug. We present both syntactic and semantic slices of the mug program and give semantic slices for various generalisations of the program. Although there is no algorithm for constructing a minimal syntactic slice, we show that it is possible, in the WSL language, to derive a minimal semantic slice for any program and any slicing criteria.

Pigs from Sausages? Reengineering from Assembler to C via FermaT Transformations (PDF)
Martin Ward
Science of Computer Programming, Special Issue on Program Transformation, Vol 52/1-3, pp 213-255, 2004.
doi:dx.doi.org/10.1016/j.scico.2004.03.007

Abstract

Software reengineering has been described as being ``about as easy as reconstructing a pig from a sausage'' [.Eastwood 1992.]. But the development of program transformation theory, as embodied in the FermaT transformation system, has made this miraculous feat into a practical possibility. This paper describes the theory behind the FermaT system and describes a recent migration project in which over 544,000 lines of assembler ``sausage'' (part of a large embedded system) were transformed into efficient and maintainable structured C code.

Legacy Assembler Reengineering and Migration (PDF)
Martin Ward, Hussein Zedan and Tim Hardcastle
ICSM2004, The 20th IEEE International Conference on Software Maintenance, 11th-17th Sept Chicago Illinois, USA.
IEEE Computer Society

Abstract

In this paper we describe the legacy assembler problem and describe how the FermaT transformation system is used to reengineer assembler systems and migrate from assembler to C and COBOL.

Conditioned Semantic Slicing via Abstraction and Refinement in FermaT (PDF)
Martin Ward, Hussein Zedan and Tim Hardcastle
9th European Conference on Software Maintenance and Reengineering (CSMR) Manchester, UK, March 21-23 2005

Abstract

In this paper we describe an improved formalisation of slicing in WSL (Wide Spectrum Language) transformation theory and apply the result to give syntactic and semantic slices for some challenging slicing problems. Although there is no algorithm for constructing a minimal syntactic slice, we show that it is possible, in the WSL language, to derive a minimal semantic slice for any program and any slicing criteria. We describe the Representation Theorem and show how it is (partially) implemented in the FermaT transformation system. The theorem has applications to semantic (or conditioned) slicing, and we use a combination of abstraction (via the representation theorem), simplification and refinement plus other program transformations to develop a powerful conditioned slicing algorithm.

MetaWSL and Meta-Transformations in the FermaT Transformation System (PDF)
Martin Ward and Hussein Zedan
The 29th Annual International Computer Software and Applications Conference COMPSAC 2005, Edinburgh, Scotland, July 26-28, 2005

Abstract

A program transformation is an operation which can be applied to any program (satisfying the transformations applicability conditions) and returns a semantically equivalent program. In the FermaT transformation system program transformations are carried out in a wide spectrum language, called WSL, and the transformations themselves are written in an extension of WSL called MetaWSL which was specifically designed to be a domain-specific language for writing program transformations . As a result, FermaT is capable of transforming its own source code via meta-transformations. This paper introduces MetaWSL and describes some applications of meta-transformations in the FermaT system.

Slicing as a Program Transformation (PDF)
Martin Ward and Hussein Zedan
ACM Transactions on Programming Languages and Systems, Volume 29, Issue 2, March 2007
doi:doi.acm.org/10.1145/1216374.1216375

Abstract

The aim of this paper is to provide a unified mathematical framework for program slicing which places all slicing work, for sequential programs, on a sound theoretical foundation. The main advantage to a mathematical approach is that it is not tied to a particular representation. In fact the mathematics provides a sound basis for any particular representation. We use the WSL (Wide Spectrum Language) program transformation theory as our framework. Within this framework we define a new semantic relation, semi-refinement which lies between semantic equivalence and semantic refinement. Combining this semantic relation, a syntactic relation (called reduction) and WSL's remove statement, we can give mathematical definitions for backwards slicing, conditioned slicing, static and dynamic slicing and semantic slicing as program transformations in the WSL transformation theory. A novel technique of "encoding" operational semantics within a denotational semantics allows the framework to handle "operational slicing". The theory also enables the concept of slicing to be applied to nondeterministic programs. These transformations are implemented in the industry-strength FermaT transformation system.

Conditioned Semantic Slicing for Abstraction; Industrial Experiment (PDF)
Martin Ward, Hussein Zedan, Matthias Ladkau and Stefan Natelberg
Software: Practice and Experience, Volume 38, Issue 12, pp 1273-1304, October 2008
doi:doi.wiley.com/10.1002/spe.869

Abstract

One of the most challenging tasks a programmer can face is attempting to analyse and understand a legacy assembler system. Many features of assembler make analysis difficult, and these are the same features which make migration from assembler to a high level language difficult. In this paper we discuss the application of program transformation technology to assist with analysing and understanding legacy assembler systems. We briefly introduce the fundamentals of our program transformation theory and program slicing which generalises to conditional semantic slicing. These transformations are applied to a large commercial assembler system to automatically generate high-level abstract descriptions of the behaviour of each assembler module, with error handling code sliced away. The assembler system was then migrated to C. The result is a dramatic improvement in the understandability of the programs: on average a 6,000 line assembler listing is condensed down to a 132 line high level language abstraction. A second case study, involving over one million lines of source code from many different assembler systems showed equally dramatic results.

Properties of Slicing Definitions (PDF)
Martin Ward
Ninth IEEE International Working Conference on Source Code Analysis and Manipulation IEEE Computer Society Press, September 2009

Abstract

Weiser's original papers on slicing defined the concept in an informal way. Since then there have been several attempts to formalise slicing using various formal methods and semantics of programs. In this paper we start by defining some properties that a definition of slicing might reasonably be expected to satisfy and then compare different definitions of slicing to see which properties are satisfied.

Properties are classified into "floor" requirements: all slices satisfying the property must be considered as valid, and "ceiling" requirements: slices which do not satisfy the property must not be considered valid. Any slicing relation which lies above a "floor" requirement, or below a "ceiling" requirement, satisfies the property in question.

The main result of the paper is the proof that, given a certain property of the programming language (informally: it is possible to write an infinite loop in the language), two of the most basic and fundamental properties of slicing are sufficient to completely characterise the semantic part of the slicing relation. These properties are: behaviour preservation and truncation.


Combining Dynamic and Static Slicing for Analysing Assembler (PDF)
Martin Ward and Hussein Zedan
Science of Computer Programming, Volume 75, Issue 3, March 2010, Pages 134-175
doi:10.1016/j.scico.2009.11.001

Abstract

One of the most challenging tasks a programmer can face is attempting to analyse and understand a legacy assembler system. Many features of assembler make analysis difficult, and these are the same features which make migration from assembler to a high level language difficult. In this paper we describe some of the methods used in the FermaT transformation system for analysing and migrating assembler systems. One technique we discuss in detail is to combine a simple dynamic slice, computed with virtually no overhead, and a static slice implemented using program transformation technology, to generate very concise high-level descriptions of the sliced code.

Deriving a Slicing Algorithm via FermaT Transformations (PDF)
Martin Ward and Hussein Zedan
IEEE Transactions on Software Engineering, Jan/Feb 2011, Volume 37, Number 1, Pages 24-47, ISSN 0098-5589. doi:10.1109/TSE.2010.13

Abstract

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 transformation, 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.

Using Software Metrics to Evaluate Static Single Assignment Form in GCC (PDF)
Jeremy Singer, Christos Tjortjis and Martin Ward
International Workshop on GCC Research Opportunities, GROW 2010 5th International Conference on High-Performance Embedded Architectures and Compilers (HiPEAC), Pisa, Italy, 23rd January 2010

Abstract

Over the past 20 years, static single assignment form (SSA) has risen to become the compiler intermediate representation of choice. Compiler developers cite many qualitative reasons for choosing SSA. However in this study, we present clear quantitative benefits of SSA, by applying several standard software metrics to compiler intermediate code in both SSA and non-SSA forms. The average complexity reduction achieved by using SSA in the GCC compiler is between 32% and 60% according to our software metrics, over a set of standard SPEC benchmarks.

Transformational Programming and the Derivation of Algorithms (PDF)
Martin Ward and Hussein Zedan
25th International Symposium on Computer and Information Sciences, ISCIS 2010, 22nd – 24th September 2010, London, England.

Abstract

The transformational programming, method of algorithm derivation starts with a formal specification of the result to be achieved (which provides no indication of how the result is to be achieved), plus some informal ideas as to what techniques will be used in the implementation. The formal specification is then transformed into an implementation, by means of correctness-preserving refinement and transformation steps. The informal ideas are used to guide the selection of transformations to apply: since they only guide the selection of valid transformations, the ideas do not themselves have to be formalised. At any stage in the process, sub-specifications can be extracted and transformed separately. The main difference between this approach and the invariant based programming approach (and similar stepwise refinement methods) is that loops can be introduced and manipulated while maintaining program correctness and with no need to derive loop invariants. Another difference is that at every stage in the process we are working with a correct program: there is never any need for a separate "verification" step. These factors help to ensure that the method is capable of scaling up to the dvelopment of large and complex software systems.

Assembler Restructuring in FermaT (PDF)
Martin Ward
13th IEEE International Working Conference on Source Code Analysis and Manipulation, 22–23 September 2013, Eindhoven, The Netherlands.

Abstract

The FermaT transformation system has proved to be a very successful tool for migrating from assembler to high level languages, including C and COBOL. One of the more challenging aspects facing automated migration, specifically when the aim is to produce maintainable code from unstructured "spaghetti" code, is to restructure assembler subroutines into semantically equivalent high level language procedures. In this paper we describe some of the many varieties of assembler subroutine structures and the techniques used by the migration engine to transform these into structured code. These transformations require a deep analysis of both control flow and data flow in order to guarantee the correctness of the result. Two separate case studies, involving over 10,000 assembler modules from commercial systems, demonstrate that these techniques are able to restructure over 99% of hand-written assembler, with no human intervention required.

Provably Correct Derivation of Algorithms Using FermaT (PDF)
Martin Ward and Hussein Zedan
Formal Aspects of Computing, Volume 26, Issue 5, Pages 993–1031, September 2014
doi:10.1007/s00165-013-0287-2

Abstract

The transformational programming method of algorithm derivation starts with a formal specification of the result to be achieved, plus some informal ideas as to what techniques will be used in the implementation. The formal specification is then transformed into an implementation, by means of correctness-preserving refinement and transformation steps, guided by the informal ideas. The transformation process will typically include the following stages: (1) Formal specification (2) Elaboration of the specification, (3) Divide and conquer to handle the general case (4) Recursion introduction, (5) Recursion removal, if an iterative solution is desired, (6) Optimisation, if required. At any stage in the process, sub-specifications can be extracted and transformed separately. The main difference between this approach and the invariant based programming approach (and similar stepwise refinement methods) is that loops can be introduced and manipulated while maintaining program correctness and with no need to derive loop invariants. Another difference is that at every stage in the process we are working with a correct program: there is never any need for a separate "verification" step. These factors help to ensure that the method is capable of scaling up to the development of large and complex software systems. The method is applied to the derivation of a complex linked list algorithm and produces code which is over twice as fast as the code written by Donald Knuth to solve the same problem.
[Home] Back to my home page.
Last modified: 9th September 2014
Martin Ward, Software Technology Research Lab, De Montfort University, Leicester.
Email: martin@gkc.org.uk