Abstract Since the original development of program slicing in 1979 there have been many attempts to define a suitable semantics, which will precisely define the meaning of a slice. Particular issues include handling termination and nontermination, slicing nonterminating programs, and slicing nondeterministic programs. In this paper we review and critique the main attempts to construct a semantics for slicing and present a new operational semantics, which correctly handles slicing for nonterminating and nondeterministic programs. We also present a modified denotational semantics, which we prove to be equivalent to the operational semantics. This provides programmers with 2 different methods to prove the correctness of a slice or a slicing algorithm and means that the program transformation theory and FermaT transformation system, developed last 25 years of research, and which has proved so successful in analyzing terminating programs, can now be applied to nonterminating interactive programs.

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.

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.

Users and systems requirements are fundamental for software development and maintenance. However, for most of existing systems, you may only find design documents without requirement specification. This paper presents an ontology-based reengineering approach to recovering requirements from existing systems. The proposed approach consists of three main parts: ontology development, ontology mapping and derivation of the requirements. Domain ontology is used to model domain specific requirements and program ontology is used to present system structure and behaviour. The algorithm of ontology mapping is developed to match domain ontology and program ontology for requirement recovery. A case study of Point of Sale Terminal (POST) system is used to illustrate the approach. Conclusions are drawn and further research directions are advocated.

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, and 3) by applying correctness preserving transformations to the specification, we can derive a simple slicing algorithm.

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.

The FermaT Maintenance Environment (FME) is a platform independent graphical user interface for the FermaT program transformation system. It is able to represent WSL code and apply FermaT transformations on single statements.

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 that 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 generalizes 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 6000‐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. Copyright © 2008 John Wiley & Sons, Ltd.

The aim of this article 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, semirefinement , 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.

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.

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.

Reengineering a COBOL legacy system is a difficult multi-step process, particularly when the COBOL legacy system is a sequential procedural-driven system which is being reengineered into an object oriented, event-driven system. In this scenario, it is necessary to analyse the legacy system in order to identify which tasks can be executed independently and which tasks must be executed sequentially. The focus of reengineering is too often based on theory rather than based on experience gained from real-world examples. This paper hopes to address this imbalance by providing a practical application of reengineering to an actual legacy telecommunications system.

We describe how the concept of program slicing can be formalised in WSL transformation theory. This formalism naturally tends 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 (Ward, 1999): an industrial-strength transformation system designed for forward and reverse engineering, re-engineering and program comprehension.

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 FermaT transformation system, based on research carried out over the last twelve years (1987-99) at Durham University and Software Migrations Ltd., is an industrial-strength formal transformation engine with many applications in program comprehension and language migration. The 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 1925 assembler modules were successfully migrated to C code.

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. However, the existing recursion removal transformations, such as the techniques discussed by Knuth [1] and Bird [2], 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 [1, 2]. 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 a ‘breadth-first’ search is the most general form. We also give two examples of recursion introduction as an aid to formal reverse engineering.

This paper treats Knuth and Szwarcfiter's topological sorting program 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.

Considers 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 (1967). 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.

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 and 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 and simplify the legacy systems and to extract higher-level 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 an accompanying formal method. Over the last ten years we have developed a large catalog of proven transformations, together with mechanically verifiable applicability conditions. These have been applied to many software development, reverse engineering, and maintenance problems. 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 summarized. We conclude that formal methods have an important practical role in software evolution.

Abstract What does it mean to say that one program is ‘more abstract’ than 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.

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 summarized. 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.

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 (1968) (p. 357) which is an algorithm for the addition of polynomials represented using four-directional links. Knuth (1974) describes this as having “a complicated structure with excessively unrestrained 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.

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’.)

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 (Foster and Kiekuth, 1990; Lientz and Swanson, 1980; Morton, 1988; Nosek and Palvia, 1990), summarized in Foster (1991), 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, 1989a). 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.