BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR94-1434
ENTRY:: 1994-08-26
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: On Program Transformations
AUTHOR:: Efremidis, Sofoklis G.
DATE:: June 1994
PAGES:: 123
COPYRIGHT:: Sofoklis Efremidis 1994 - All Rights Reserved
ABSTRACT::
In understanding complex algorithms, the notions of encapsulation and 
modularization have played a key role.  An algorithm is broken into several 
parts or modules, and understanding of each part is independent of others.  In
addition, each part contains details that are not needed by other parts and 
so can be hidden from them.

Programming languages provide support for encapsulation and modularization in 
many different forms.  Early programming languages provided the procedure and 
function as a means for modularization.  Later, files were introduced as a 
means of modularizing programs.  More sophisticated mechanisms were then 
introduced, like modules, packages, structures, and classes.  In all these 
cases, the interface to a module remained the procedure or function call.  
Programs that use such modules contain calls to functions and procedures for 
communicating with a module.  Ideally, using the operations that are provided 
by a module should be done in exactly the same way as using operations that 
are provided by modules should be easy to intermix.  In addition, substituting
one module for another that has the same functionality but different 
implementation should involve a minimal amount of effort.

Recently, a new programming language, Polya, has been designed, which 
attempts to support modularization and at the same time incorporate the 
operations that are provided by the modules in the programming language 
itself.  This is done by a sophisticated type-definition facility and a 
mechanism for transforming programs at the source-program level.

This thesis studies mechanisms for program transformation at the source 
program level, in the context of Polya.  Program transformation is 
based on a set of transformation rules that prescribe how a part of a program 
is to be transformed, and a set of directives that prescribe which program 
variables are to be transformed.

We first give an algorithm for processing program transformations as described
by the transform construct.  The algorithm constructs a coordinate 
transformation of an abstract program based on a set of transforms and 
transform directives for transforming program variables.  We then study the 
problem of transforming expressions that have compound types.  Both the type 
constructor and the component expressions of the original expression may be 
transformed.  No extra rules need be added  to the bodies of transforms that 
transform the type constructor and the component expressions.

In the sequel  we investigate the problem of transforming procedures and 
functions that have parameters that need to be transformed.  Finally, the 
problem of transforming program-transformation rules is studied.

The program transformation techniques are applied to two well-known 
algorithms.  The algorithms are source programs, which are subsequently 
transformed to programs of conventional programming languages, and then 
compiled and run.
END:: CORNELLCS//TR94-1434
BODY::
On Program Transformations
Sofoklis Efremidis
Ph.D Thesis
TR 94-1434
June 1994
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
ON PROG?AM TRANSFOIQMATIONS
A Dissertation
Presented to the Faculty of the Graduate School
of Cornell University
in Partial Fulfillment of the Requirements for the Degree of
Doctor of Philosophy
by
Sofoklis Efremidis
May 1994
Qc Sofoklis Efremidis 1994
ALL RIGHTS RESERVED
ON PROGRAM TRANSFORMATIONS
Sofoklis Efremidis, Ph.D.
Cornell University 1994
In understanding complex algorithms, the notions of encapsulation and modulariza-
tion have played a key role. An algorithm is broken into several parts or modules, and
understanding of each part is independent of others. In addition, each part contains
details that are not needed by other parts and so can be hidden from them.
Programming languages provide support for encapsulation and modularization
in many different forms. Early programming languages provided the procedure and
function as a means for modularization. Later, files were introduced as a means
of modularizing programs. More sophisticated mechanisms were then introduced,
like modules, packages, structures, and classes. In all these cases, the interface to
a module remained the procedure or function call. Programs that use such modules
contain calls to functions and procedures for communicating with a module. Ide-
ally, using the operations that are provided by a module should be done in exactly
the same way as using operations of primitive types of the programming language.
Primitive operations of the language and operations provided by modules should be
easy to intermix. In addition, substituting one module for another that has the same
functionality but different implementation should involve a minimal amount of effort.
Recently, a new programming language, Polya, has been designed, which attempts
to support modularization and at the same time incorporate the operations that
are provided by the modules in the programming language itself. This is done by
a sophisticated type-definition facility and a mechanism for transforming programs
at the source-program level.
This thesis studies mechanisms for program transformation at the source program
level, in the context of Polya. Program transformation is based on a set of transfor-
mation rules that prescribe how a part of a program is to be transformed, and a set
of directives that prescribe which program variables are to be transformed.
We first give an algorithm for processing program transformations as described
by the transform construct. The algorithm constructs a coordinate transformation of
an abstract program based on a set of transforms and transform directives for trans-
forming program variables. We then study the problem of transforming expressions
that have compound types. Both the type constructor and the component expres-
sions of the original expression may be transformed. No extra rules need be added
to the bodies of transforms that transform the type constructor and the component
expressions.
In the sequel we investigate the problem of transforming procedures and func-
tions that have parameters that need to be transformed. Finally, the problem of
transforming program-transformation rules is studied.
The program transformation techniques are applied to two well-known algorithms.
The algorithms are source programs, which are subsequently transformed to programs
of conventional programming languages, and then compiled and run.
BIOGRAPHICAL SKETCH
Sofoklis Efremidis was born on August 3, 1963 in Agia Paraskevi, a suburb of Athens,
Greece. He attended the Anavryta Model School in Kifissia, Athens and graduated
in June 1981. While in high school he pursued studies in classical music, and in June
1981 he was awarded an advanced degree in Classical Guitar performance from the
National Conservatory of Athens.
In September 1981 he was admitted to the University of Patras, in Patras,
Greece. In September 1982 he transferred to the Department of Electrical Engi-
neering, National Technical University of Athens. He graduated in September 1986
with a Diploma in Electrical Engineering. He then worked as a Research Assistant
at the National Technical University of Athens and at the University of Maryland,
College Park.
He joined the Graduate School at Cornell University in September 1988. In
August 1991 he was awarded a Master of Science Degree in Computer Science by
Cornell University. He completed the requirements for the Ph.D. Degree at Cornell
University in May 1994.
Sofoklis Efremidis is a civilian pilot having the Airplane Single and Multiengine
Land and Instrument Airplane ratings.
iii
??ou? yov?k ?ou F??py? X?L
X?L
OTa a???cp?a \LO? eav?a? xaL
F?a 6aa ?xa?av yLa ?s'va
xaL
YLa T7)V ay&?? xaL au??a?a'aTaaY)' TOU?
iv
ACKNOWLEDGEMENTS
First and foremost, I would like to express my deep gratitude, respect, and thanks to
Professor David Gries. This thesis would have been impossible to complete without
his constant encouragement and suppoft. An inspiring researcher, an outstanding
teacher, a human full of warmth and understanding, David Gries was always willing
to help and advise, especially during the critical phases of this work.
I would also like to thank Professor Steve Vavasis and Professor Anil Nerode for
serving on my special committee.
I greatfully acknowledge the generous support by DARPA-ONR (Research Grant
Nooo14--H91--HJ--H4123) for the work of this thesis.
I wish to express my sincere thanks to Aswin van den Berg, who helped immensely
during this work and who was always there when I needed his expertise. I would
also like to thank the other members of the Polya group for introducing me to the
language and for their help, especially during the early stages of this work. Many
thanks to my coauthors Khalid Mughal and John Reppy.
My sincere thanks also go to the support staff of the Department of Computer Sci-
ence at Cornell University, especially to Jan Batzer, Diana Catley, Dorothy Marsch,
Holly Mingins, and Becky Personius, for the outstanding help they provided while
I was graduate student.
v
My friends both made my life in Ithaca more enjoyable and helped in my intel-
lectual growth. I would like to thank each one of them. Special thanks to Caroline-
Fotene Chisham for her true friendship and her pleasant companionship during my
stay in Ithaca. Special thanks also to Victor and Roula Balopoulos, Alessandro
Panconesi, Nikos Pitsianis, and Pankaj Rohatgi for their constant interest and en-
couragement on academic and non-academic matters. I also wish to thank my friends
at East Hill Flying Club in Ithaca, for exposing me to the wonderful and exciting
world of aviation.
Finally, I would like to deeply thank my family: my parents and my brothers for
their love, encouragement, and support all these years.
vi
TABLE OF CONTENTS
1 Introduction
1.1			Program Refinement .
1.2			Rewrite Systems
1.3			About this Thesis
1.4			Related work
2 Preliminaries
2.1			Types .
2.2			Terms			.
3 The Transform
3.1			Introduction
3.2			Components of a transform
3.2.1 Local declarations
3.3			An example of a transform
3.4			Transform directives
3.5			Examples of using a			transform
3.6			Program transformation
4
4.1
4.2
4.3
4.4
4.5
4.6
4.7
4.8
4.9
4.10
4.11
4.12			. .
Transforming variables that have base types
Introduction . .
Overview .			. . .			. . .
Pattern matching			.
Replacement Instantiation			. . .			.
The main algorithm . .
Representations and transformation of variables
Representations and transformations of constants
Representations and transformations of expressions
Transformations of statements .
Transformations of programs			.
Correctness . . . .			. . .
Complexity analysis
vii
3
5
7
9
10
10
11
14
14
16
21
22
23
24
25
26
26
26
32
33
36
36
42
42
45
46
47
49
5 Transforming expressions that have compound types
5.1			Introduction			. .
5.2			Overview . 			. .
5.3			Transform and Transform			Directives
5.3.1 Extensions to transforms			. . 						. 			.
5.3.2 Notation. 			. . 			. .
5.3.3			Steps in transforming expressions that have compound types
5.4			Preprocessing the transforms			. .
5.4.1 Processing transform directives of the form M(?x)
5.4.2 Processing transform directives of the form 1(x)
5.4.3			Processing transform directives of the form M. .			. .
5.4.4 An example of preprocessing a transform for sequences
5.5			Transforming the abstract program . . . 			. . .
5.5.1			Replacing variables that are transformed
5.5.2			Transforming expressions
5.5.3			An example of transforming the elements of an array			. .
6 Transforming functions, procedures, and transforms
6.1			Transforming functions and procedures			.
6.1.1 Functions and procedures
6.1.2			Examples of transforming function and procedure calls .
6.1.3			Transforming Functions and Procedures .
6.1.4 Some theoretical results
6.2			Transforming variables in a transform. . .			.
6.2.1			Directives for transforming variables of a transform			. . .
6.2.2			Processing transform directives for variables in transforms			. .
7 A second approach to dealing with compound types
8 Methodology and examples
8.1 Interfering implementations. 			. . .
8.2 Example: The Huffman Encoding Algorithm			. .			. .
8.2.1			The algorithm. .
8.2.2			Abstract types used in the algorithm			. .			.
8.2.3			Transforming the algorithm
8.3 Example: The Hopcroft-Tarjan Planarity Test Algorithm
8.3.1			Abstract types used in the algorithm . .			.			. .
8.3.2			Input and output of the algorithm . .
8.3.3			Constructing a directed graph . .
8.3.4			Producing an embedding . . . . . .						. .
51
51
51
52
53
55
56
56
57
58
58
58
60
60
60
62
64
64
64
65
67
69
70
70
73
76
80
80
84
85
85
89
100
100
101
102
103
viii
8.3.5
8.3.6
8.3.7
8.3.8
8.3.9
Printing all embedding
The main program			.
Directives			. .
The transforms used			.
Example of execution			. .
Bibliography
ix
108
108
108
112
119
121
LIST OF FIGURES
1.1			Relationship of abstract and concrete state changes			4
2.1			Definition of type seq(t).			. . 			. . 						11
2.2			Definition of function subst.			. .			. 			13
3.1			BN implements a variable of type bool with a variable of type nat.			15
4.1
4.2
4.3
4.4
4.5
4.6
4.7
4.8
6.1
6.2
6.3
8.1
8.2
8.3
8.4
8.5
8.6
8.7
8.8
8.9
8.10
8.11
8.12
8.13
Definition of pattern matching. . .
Definition of app'
Definition of replacement instantiation.
Main transformation algorithm
Application of a transform rule to an abstract tree node.
Construction of representations of an expression.
Construction of conversion of representations.
Construction of transformation of an expression.
Complex implements a variable of type complex with a tuple of real
numbers
Rtuple implements a variables of type rtuple with a record.
Gomplex?RtupTh implements a variable of type complex with a record.
Graph implements variables of type dgraph.
Defining a local meaning for operation delete. . . . . .
Implementation of graphs according to transform Graph'
Huffman encoding algorithm with directives. . . .
Definition of type set(t).			. .			. .			.
Definition of type seq(t).			. .			. .			. . . .
Definition of type bfree(t).
Definition of type ptr(t).			.			. .			. .
Transform Btree? Trec. . .
Implementation of tree (:(:tn?l, d2, tnil:?, dl, (:tnil, d3, tnil:?:? according
to Btree?'Prec			. . .
Transform Seq?Dll, part			1.			. .			. .			.
Transform Seq?Dll, part			2.			. .			.			. . . .
?ansform Seq?Dll, part			3.			.			. . .			. . .
x
34
35
37
38
43
44
45
46
72
72
73
82
83
83
86
87
88
89
90
90
91
92
93
94
8.14
8.15
8.16
8.17
8.18
8.19
8.20
8.21
8.22
8.23
8.24
8.25
8.26
8.27
8.28
8.29
8.30
8.31
8.32
8.33
8.34
8.35
8.36
8.37
8.38
8.39
Implementation of sequence ((d1,... , dn? according to Seq?D11.
Transform Set?5eq, part 1. . . .			. 			. .
Transform Set?Seq, part 2.
Transformed program, part 1. . . .			. . .
Transformed program, part 2. .
Output of lluffman encoding algoritlim. .
Definition of type dgraph
Definitions of Readgraph and PrintGraph
Definition of RenamGraph, part 1.
Definition of RenamGraph,			part			2.			. .						. .
Definition of Planarity, part			1.			.			. .
Definition of P1anamt?, part			2.			. 			. . .
Definition of PrintEmbed. .			. .
Definition of PmntSeq.			. .						. . . .
Main program. .			.			.
Directives for transforming abstract program variables
Transform Seq?L?st, part 1.			. .
Transform Seq?List, part 2.
Implementation of ((d1,... , dn')? according to Seq?List
Transform RevSeq			..
Transform Set?Seq
Transform Graph?AdjList, part 1.. .
Transform Graph?AdjL?st, part 2			. .
Transform Arr
(a) Input graph. (b) A corresponding palm graph.
Output of the planarity algorithm. . .
xi
95
95
96
98
99
99
101
102
104
105
106
107
109
110
110
111
113
114
115
115
116
117
118
119
119
120
Chapter 1
Introduction
Modern programming languages tend to be of higher level than those designed and
implemented a few decades ago, in the sense that they are more problem-oriented
than implementation-oriented. They focus on the problem to be solved and provide
mechanisms for abstracting from the implementation details for solving it. Modu-
larization and encapsulation are two primary mechanisms that most modern pro-
gramming languages provide for abstraction. With modularization, a program can
be split into independent modules that have well-defined interfaces. Encapsulation
allows implementation details to be hidden from parts of a program where they are
not needed.
Modules in modern programming languages provide for the definition and im-
plementation of types. However they are rather restrictive, in that the interface
between a module and a program is the procedure or function call and not an ar-
bitrary statement or expression. Operations that are provided by modules do not
look like primitive operations that the programming language provides. For example,
most programming languages support integers as primitive data types, and a program
may contain expression a + b for computing the sum of two integer variables a and b.
On the other hand, types like set may not be supported, so users of type set have
to use modules that implement operations on sets. However, mathematical notation
can not be introduced and integrated in the language. As an example, assume that
an algorithm contains statement
s 5 U ?e1
where s is a set of integers (say) and e is an integer. A program that implements this
algorithm needs to use a module that implements sets and operations on them. As
mentioned before, the interface to a module is the procedure or function call. Hence,
a program cannot contain a statement like the one above. Instead, depending on the
module that is used in the implementation for sets, the statement may have to be
2
written as
or
insert(s, e)
assign(s, union(8, singleton(e))).
And, if one wants to switch back and forth between implementations, the program
itself has to be changed accordingly.
The advantages of using mathematical notation in a program are apparent. Pro-
grams look like the mathematical algorithms they are supposed to implement. But
more importantly, the designer of an algorithm can use a notation that facilitates
focusing on the algorithm itself instead of its implementation details. The algorithm
designer may use abstract mathematical objects like sets, bags, sequences, and lat-
tices that may be needed in the algorithm, using the notation that best suits the
domain.
If a programming language is to support new abstract types and operations on
them in the same way it supports primitive types and operations, it needs to be
tuned to the new syntax of the literals and the operations of the new types.
Prom a practical viewpoint, one would also like to be able to run an algorithm on
a machine. This implies that the algorithm has to be changed from its abstract form
that humans understand and reason about to a form that a machine can execute. Put
in another way, the algorithm needs to be refined. Apparently, some sort of transfor-
mation of the original algorithm has to take place, and one would like to automate
this transformational process as much as possible. In existing languages that restrict
the interface of a module to be the procedure or function call, this transformation is
accomplished by the compiler that implements the language. The transformational
mechanism is hard-wired in the compiler. On the other hand, for a language that
can be tuned to a specific syntax of interest, the transformational mechanism should
be independent of the transformations that are to be applied. The transformations
should be described in an appropriate language, and the transformational mechanism
should apply these transformations to the abstract program. One can think of the
transformations as rules that describe how parts of a program can be refined. As
an example, they may describe the refinement of abstract operations like b u c and
s s U ?e1.
With such a mechanism, reusability comes for free: the transformations can be
reused in other programs as well, as long as they implement the operations that
appear in those programs.
A mechanism is also needed for specifying what transformations are to be applied
to a program, i.e. a kind of directive. A directive is the link between an abstract
program and the transformations that are to be applied to it. Using a directive,
for example, one can specify that one set variable (and operations on it) are to be
3
implemented using a hash table, while another set variable is to be implemented
using a binary tree. The important point about having such a mechanism is that
the decisions on how to implement variables of the abstract program are localized.
If one decides that a different implementation of a variable of the abstract program
is desirable, one need only change the directive that specifies that transformation of
that variable. The abstract program remains unchanged.
The programming language Polya [GV92j was designed with this philosophy in
mind. The programming paradigm of Polya is as follows. The designer of an al-
gorithm decides which types are needed by the algorithm. The new types and the
operations they involve are formally defined, including the concrete syntax for each
operation. The new types are then incorporated into the language and the newly
defined types and operations can be used like the primitive types and operations
provided by the language. Programs can be written that make use of the new types
and can later be data-refined into a more concrete form.
Languages like Ct+ [Str9l] provide sophisticated mechanisms for encapsulation
and modularization. One disadvantage is that these languages lack extendibility of
concrete syntax. No new syntax can be defined, and only the built-in operators
can be overloaded. In addition, a class is essentially a data type together with its
implementation. This means that two variables of the same type that are to be im-
plemented differently have to be of different classes. It also means that conversions of
representation have to explicitly appear in the abstract program. This, together with
the fact that the interface between an abstract program and an implementation is
the procedure or function call, means that the abstract algorithm will be far removed
from its implementation. Too much must be done to the abstract program by the
programmer to make it efficiently implementable.
1.1 Program Refinement
The notion of program refinement is fundamental in computing science. When one
refers to program refinement, one has to specify what a program is. A program may
be a specification that is expressed in a formal language, like predicate calculus or
temporal logic. Or, it may be a detailed description of machine instructions. Program
refinement is the process by which a program that is expressed in a high-level form is
changed to another one in a more concrete form. The refinement of a program need
not be one big step; it may be broken down to smaller steps, which can be further
subdivided to even smaller steps, and so on.
A specification language is usually very expressive and contains powerful operators
and statements, and rich data types. Refinement of a specification entails refinement
of the operators and statements as well as the data types that are involved in the
4
aO			A			al
cO			c			cl
Figure 1.1: Relationship of abstract and concrete state changes.
specification. Replacing powerful operators and statements by simpler ones is known
as procedural refinement. Replacing rich data types by simpler ones is known as data
refinement.
[Gri81,Dij76j give a methodology for refining a specification that is expressed in
predicate logic into a program that can be executed by a machine. Their work focuses
mainly on procedural refinement. They give heuristics for refining specifications until
they are in a suitable form so that concrete programs can be derived from them. Since
the refinement takes place in a logical framework, the derived programs are provably
correct with respect to their specifications.
On the other hand, [MG90,Mor89J give a calculus for refining specifications into
concrete programs, focusing, mainly, on data refinement. They also give the required
proof obligations for the refinement to be proved correct. [GP85] and [GV91] also
give a methodology for data refinement and the required proof obligations for the
refinement to be proved correct.
Figure 1.1 shows the relationship between abstract and concrete state changes. In
that figure, aO and al are two states of the abstract program and A describes a state
change from aO to al, i.e. it is an abstract statement. Similarly, cO and cl are two
states of the concrete program that is a refinement of the abstract one, and C is
a state change from cO to ci, i.e. it is a concrete statement. 1 is a coupling invariant,
i.e. a predicate that describes the relation between abstract and concrete variables.
If cO is the state of the concrete program that corresponds to abstract state aO,
then I(aO, co) holds. Execution of abstract statement A from state aO results in
state al. If C is a refinement of A, then execution of concrete statement C from
state cO results in a state cl such that I(al, ci) holds. In other words the diagram in
Figure 1.1 commutes. This requirement is expressed as a proof obligation in ?MG9O,
Mor89] and [GP85].
5
According to [MG9O,Mor89], the proof obligation for concrete statement C to
refine abstract statement A is
I: IAwp(A,X))?wp(C,(?b I: lAx))			(1.1)
for all predicates X that contain no concrete variables. Predicate wp is the weakest
precondition, as defined in [Dij76j: for a statement S and a predicate P, wp(S, P)
is the weakest predicate that describes the set of states S such that execution of S
begun in a state in S terminates in a state described by P. Let X be a predicate that
holds in state a1 and contains only abstract variables. Assume for simplicity that
the abstract program contains one abstract variable b (say). Assume also that there
exists a value for b such that I A wp(A, X) holds, i.e. it satisfies coupling invariant I
in state a0. if execution of C starts in state cO it will terminate in state c1 such that
there must exist a value of b for which the coupling invariant holds, i.e. I A X.
According to [GP85], the proof obligation for concrete statement C to refine
abstract statement A is
IA wp(A,X) ? wp(C,?'wp(A,?I))			(1.2)
where X is a predicate that holds in state al. Let Y = wp(A, X) and assume
that I A Y holds in state cO where C starts execution. Then it must be the case
that execution of C when started at cO terminates in a state (ci in the diagram of
Figure 1.1) such that execution of statement A starting from state a0 may establish I.
in other words, execution of C will not result in a state where I is not established
after executing A.
[CU89j prove that the two formulations 1.1 and 1.2 are equivalent. They also give
three additional equivalent formulations.
1.2 Rewrite Systems
in this thesis, we study algorithms for program transformations. We are mainly
concerned with syntactic transformations of programs as opposed to semantic trans-
formations. To this extent, the program transformations we deal with bear some
similarity to transformations accomplished by rewrite-systems. in this section we
briefly discuss term- and string-rewrite systems. in the next section we discuss the
inapplicability of term-rewrite systems to the program transformations with which
we are concerned.
Rewrite systems are mathematical formalisms that are used to compute by suc-
cessive replacements. A rewflte system consists of a set of objects and a reduction
relation. The reduction relation is used in replacing part of an object by another one.
6
Rewrite systems have the same computational power as Thring Machines [11U79j.
There are two kinds of rewrite systems: term-rewrite and string-rewrite systems.
In term-rewrite systems [DJ9o] the objects that are subject to replacement are
terms. A term is either a variable, a constant symbol, or a function symbol applied
to a list of terms. As an example, consider the set of objects generated from constant
symbols a and b, function symbols f (of arity 2) and 9 (of arity 1), and the reduction
relation
R = t(f(a, b)			g(b)), (9(9(b))			9(b)), (h(g(b), 9(b))
Using the rules in R, we can reduce term h(f(a, b), g(f(a, b))) as follows.
H
H
H
H
H
A sequence like this is called a
In a string-rewrite system
characters of a finite alphabet.
reduction relation
h(f(a, b), g(f(a, b)))
h(f(a, b), g(f(a, b)))
h(9(b), g(f(a, b)))
h(g(b), g(g(b)))
h(9(b), g(b))
h(b)
reduction sequence.
[B093] the objects that are reduced are strings of
As an example, consider alphabet A = ta, b? and
R = taabb ab, bbaa ba, abab aa, baba bbl.
Using the rules in R we can reduce string aabbaabb as follows.
aabbaabb
abaabb
abab
aa
Depending on properties of the reduction relation, a string may or may not reduce
to a unique string. For example, string aabbaabb of the previous example may be
reduced as follows.
aabbaabb
aababb
aaab
7
On the other hand, a string may reduce to a unique string via two different reduction
sequences or it may not reduce to any string at all (i.e. give rise to an infinite reduction
sequence).
Rewrite systems provide purely syntactical transformations. The reduction pro-
cess assigns no semantics to the objects (terms or strings) that are reduced.
1.3 About this Thesis
In this thesis, we study the mechanics of program transformation according to the
transform construct, which is described in a later chapter. The thesis focuses on
the transformation system of Polya [GV92]. We give algorithms for transforming
programs at the source level. The transformation of programs we are concerned with
is completely syntactic; we do not cover issues of correctness of transforms.
First, we give an algorithm for transforming programs that contain variables and
expressions that have simple types. The algorithm constructs a coordinate transfor-
mation of an abstract program based on a set of transforms and transform directives
applied to it. A coordinate transformation of a program is an equal program in
which one or more program variables and operations on them have been replaced
by new ones. Then, we study the transformation of programs that contain expres-
sions that have compound types (like set(int)). We allow both the type constructor
(set in this case) and the component expressions (of type int) to be transformed,
and no additional rules need be added to transforms for the type constructor. In
the sequel, we study the transformation of functions and procedures that are called
with arguments that need to be transformed, and then we study the transforma-
tion of program-transformation rules. Finally, we give examples that illustrate these
methods.
An important methodological issue related to our work is the so-called partial
implementation of an abstract type. An implementation of an abstract type is partial
if either some operations of the type are not implemented or there are preconditions
that have to be satisfied for an implementation of the operation to be correct. The
main motivation for the partial implementation of an abstract type is efficiency. For
example, depending on what operations on sets are used in a program, the union-
find algorithm that implements efficiently set operations union and find may be
more appropriate to use than a hash-table implementation for sets. The partial
implementation of abstract types was studied in [Pri87]. In that thesis, operations of
data types were implemented by explicit transform rules that describe how a part of
a program can be refined to another one. The transform rules that were considered
in that work were mainly rewrite rules of a rewrite system.
In the present work, we also consider representations of expressions and transfor-
8
mations of expressions and statements, which are formally defined ill a later chapter.
Representations are defined only for expressions (not for statements). As mentioned
before, the coupling invariant is a predicate that connects the abstract and concrete
variables.
An expression r is a representation of an expression e if it contains no abstract
variables and the coupling invariant holds for r and e. For example, consider repre-
senting expressions of type bo9l with natural numbers, where the coupling invariant is:
"a boolean expression e is true if and only if its representation r (a natural number)
is greater than zero", i.e. I(e, r) is e = r > 0. Now consider boolean expressions bi
and b2, and assume that they are both represented with natural numbers as just ex-
plained. Let also ni be the representation of bi, and n2 be the representation of b2.
Then, the representation of e' = bi A b2 is r' = ni * n2, and it is straightforward
to prove that the coupling invariant holds for e' and r'.
A transformation of an expression or statement is an equal expression or state-
ment, respectively, in which one or more variables have been replaced by new ones.
The difference between the transformation and a representation of an expression can
be explained as follows. Let I(a, c) be the coupling invariant that connects variables a
and c. Assume that abstract expression e refers to variables ...... , a?--H1 that are
to be replaced by Co,... , Cn--H1, and assume that I(ai, ci) holds for 0 < i < n. Then,
e may be replaced by f iff e = f, and f is a representation of e iff I(e,f) holds. In
summary,
f is a transformation of e iff I(ao, co) A ... A I(a?--Hi, Cn--Hi) ? e = f
f is a representation of e iff I(ao, co) A ... A I(a?--Hi, cn--Hi) ? I(e,f).
An important point to note is that a given expression may have more than one
representation, and that there may be several transform rules that prescribe ways
of converting one representation to another one. For example, expressions of type
bool may also be represented with floating-point numbers, and there may be trans-
form rules that convert a natural-number representation of a boolean expression to
a floating-point-number representation, and vice versa.
The necessity for using representations of expressions becomes apparent when
we consider the implementation of arbitrary expressions that contain variables to be
transformed. Representations of expressions provide a way for implementing an ex-
pression from the implementations of its subexpressions.
The notion of expression-representations renders term-rewrite systems inapplica-
ble for our work. Application of a transform rule to part of a program is similar to
a term-reduction. The difference is that, in a reduction of a term with a term-rewrite
system, a single redex is chosen at each reduction step and gets replaced by a new
term. In our case, the choice of which representation to use for an expression may
be delayed until enclosing constructs are processed. Expressing this property with
9
rules of a term-rewrite system would require an exhaustive set of rewrite rules that
involves all possible combinations of nesting program expressions.
In addition, term-rewrite systems are rendered inapplicable for the transformation
of expressions that have compound types (for example seq(int)). The transformation
of type constructors (like seq) and component types (like int) should be independent
of each other as far as transform rules are concerned. This independency requirement
cannot be readily expressed with rules of a term-rewrite system.
Finally, term-rewrite systems are inapplicable for the transformation of functions
and procedures whose arguments are transformed. When a call to a function or
procedure involves arguments that need to be transformed, a new copy of the function
or procedure need be constructed, in which the appropriate parameters are suitably
transformed. This requirement cannot be expressed with rules of a term-rewrite
system.
Of course the transformation of a program can be simulated by a term-rewrite
system, since, as stated before, such a system has the power of a Thflng Machine,
but this is not our objective when carrying out program transformations.
1.4 Related work
The CIP project [Par90] focused on a transformational methodology for program
development. The transformational methodology of CIP involves both procedural
and data refinement. Transformations of programs in CIP involves semantic, as
opposed to our purely syntactic transformations.
Predicate calculus and algebraic specifications are used for specifying programs
and abstract types in the CIP framework. The program specification is subsequently
transformed to a concrete program in a series of steps. The transformation process
is not fully automated. Since semantic issues are involved, the system needs user
input. The user of the system is responsible for choosing appropriate rules to come
up with a concrete program that satisfies the specifications.
When transforming a program in CIP there is an interaction between the user
and the system. The decisions of the user are actually transformation directives that
are applied to the original program. In other words, the directives for transforming
a program are distributed and are part of the transformation process. If a different
transformation of the original program is desired, then different decisions need to be
taken by the user.
In our case, the directives for transforming a program are centralized and are
part of the program text. When a different transformation needs to be applied to
a program, a single directive need be changed.
Chapter 2
Preliminaries
We give the necessary technical material for understanding the rest of the thesis.
2.1 Types
The types of expressions that we later show how to transform are essentially the data
types of Polya [GV92J. We give a brief overview of Polya's type system.
Pot?a's type system tSmi9lJ is essentially ML's type system [Mil86], which is based
on the type system of Damas and Milner [DM82], extended to include overloading
and subtyping.
The definition of a new type in Polya includes definitions for literals and oper-
ations of the type. The definition of an operation involves definition of types of its
components, possible constraints on these types, as well as concrete syntax for the
operation. The definition of a new type in Polya is intended to extend the syntax of
the language to include the concrete syntax of the operations of the type.
There are three kinds of operations: functions, expressions, and statements. Con-
sider for example type seq(t), the type of sequences that have elements of type t,
shown in Figure 2.1. Type t can be any type; seq is a polymorphic type constructor.
Literal seq?ni1 denotes the empty sequence, and is written as
Function seq?rev has one parameter, s, which is of type seq(t) (the type of s is
enclosed in parentheses). It yields a value of type seq( t). If a program contains
a variable s:seq(t), then seq?rev(s) is a legal function call.
Expression seq?se1 has two components: an expression s of type seq(t) and a vari-
able i of type int. The type of the result is t. If a program contains a variable s: seq( t)
and a variable i:int, then s((i)) is a legal expression.
Statement seq?iter has three components: a variable v of type t, an expression 8
of type seq(t), and a statement z. If a program contains a variable s:seq(t) and
10
11
type seq(t)
literals
seq?ni1 as
operations
seq?rev exp-s (s:seq(t)) seq(t) o+..;
seq?se1 exp-s exp-i (s:seq(t); i:int) t as
seq?iter var-v exp-s stmt-z (s:seq(t)) o+..;
end
Figure 2.1: Definition of type seq(t).
a variable e:t, then "foreach e in s do o+.." is a legal statement.
The concrete syntax given in the type definition is used to augment Polya so
that operations that are defined in the type definition can appear in a program like
any other primitive operation of the language. For example, given the previous type
definition, the following is a syntactically correct Polya program fragment.
2.2 Terms
var s:seq(int) :=
var i:?nt,k:int =0;
foreach i in s do k := k + s((i));
Let C be a set of constants, V a set of variables, and ? a set of function symbols such
that C A V A = ?. With each function symbol F in ? we associate its arity OF,
which is a positive number. The set T of terms is defined as follows.
o+ A variable ?v in V is a term.
o+ A constant c in C is a term.
o+ If t is a list of terms, and F in ? is a function symbol of arity 0F = #i, then
Fct) is a term, called a compound term (and the ti's are its components).
By convention, variables begin with one or more "?" symbols.
A term that contains no variables is called a ground term. A term that contains
at least one variable is called a non-ground term. For example, assume that F is
12
a function symbol of arity 1, C is a constant symbol, and ?s is a variable. Then,
C and F(F(C)) are ground terms, and ?s and F(?s) are non-ground terms.
For a term tin T, denote by Var(t) the set of variables that appear in t.
iftis?v
Var(t)=			?			if t?C
(ui 0 <i < n : Var(tj)) if t is F(t0, . . ,tn?i)
Let ?v#t be the number of occurrences of variable ?v in t. A term t is simple if
(V?v I: ?v#t < 1).
A substitution is a finite mapping from variables to terms. We write a = ??vo
to, ... , ?Vn--H1 tn?1 ? for a substitution. The domain of a substitution is the set of
variables for which it is defined, i.e.
dom(a)=??v (?t :?v?t?a)J.
For example, dom(a) = ??vo,... , ?Vn?iY. If ?v E dom(a), then a(?v) is the term to
which ?v is mapped by a. If ?v ? dom(a), then a(?v) is undefined.
Define & to be the extension of a such that &(?v) = ?v for variables ?v that are
not in dom(a), i.e.
a(?v)			if ?v ? dom(a)
=			if ?v ? dom(a)
A substitution a = ??vo to,... , ?vn--Hi H tn--Hil is simple if none of the ?Vj'5 occur
in the t?'s:
dom(a) n (ui 0 <i < n : Va?tj)) =
Application t a of a substitution a to a term t is defined as follows.
iftis?v
t a =			t			if t E C
F(t0.a,...,t??i.a)			iftisF(t0,...,tn--Hi)
Theorem 2.2.1 There is a linear algorithm that, 9iven two simple terms s and t
for which Var(s) fl Var(t) = ?, finds a substitution a such that 5. a = t a, if such
a substitution exists, otherwise it reports failure. Furthermore, if a exists, then it is
simple.
Proof: This is a special case of the Unification Theorem [Rob65]. Call subst(s, t, ?)
of function subst, shown in Figure 2.2, constructs substitution a of the theorem if
such substitution exists. Otherwise, it returns special symbol 1, to indicate failure.
13
subst(?v, t, a) = a U ??v :?`
subst(t,?v,a) = aU ??v H tJ
subst(c, c, a) = a Comment for c in C
subst(F(?s), Fct), a) = subst'(s,t, a)
otherwise I
subs?(?s, t, I) = I
subst'([j,[],a) = a
substt(?s,t,a) =
if #s> 0A #t>o subst,(--Hs[1.i,?t[1.i,subst(?s0,t0,a))
II #?s=Ov#t=O? I
fi
otherwise I
Figure 2.2: Definition of function subst.
Now consider the call subst(s', t', a) and assume that a is simple. Since terms 8
and t are simple by hypothesis, and Var(s) A Var(t) = ?, it follows that for every
subterm s' of 5 and t' of tin the call subst(s', t', a)
Var(s') A dom(a) = Var(t') A dom(a) =
Initially a = ?, which is a simple substitution. We distinguish the following cases.
1. If 5' is ?v, since ?v ? Var(t'), then a U ??v ? t') is simple.
2. Likewise, if t' is ?v, then a U ??v H t'? is simple.
3. If 5' is F(?s') and t' is Fet'), then subst' augments a with the bindings that
result from the calls subst(?s'?,t'?), for 0 < i ? #s' Since s' and ? are simple, it
follows by an inductive argument that the resulting substitution a is simple.
Hence, subst(s', t', a) yields a simple substitution. It is also easy to see that this
algorithm is linear in the size of its inputs.			5
Types
As mentioned before, the types of expressions that we later show how to transform
are essentially the data types of Polya, and they are actually terms.
In the case of types, V is the set of type variables, C is the set of base types, and ?
is the set of type constructors. We denote by T the set of types. When we refer to
types we use the terms ground type, non-ground type, compound type, and component
type.
Chapter 3
The Transform
3.1 Introduction
A language construct, the transform (as a feature of the programming language
Polya [GV92j), has been proposed for program transformations at the source pro-
gram level [GV9l]. The advantage of the transform is that it lets programmers write
programs in an abstract form, which can then be transformed, using directives, to
a more concrete form that can be accepted and executed by a machine. Hence, pro-
grams may be written at a much higher (more abstract) level than most conventional
programming languages allow. A transform describes a coordinate transformation,
i.e. the replacement of some program variables by new ones, perhaps of different
types. A coordinate transformation can be a partial implementation of an abstract
type [GP85], a data refinement [MG9O,Mor89], or a general transformation like the re-
placement of a dummy variable in a loop for efficiency purposes [Knu63]. A transform
directive specifies which transform to use to replace a particular program variable.
The abstract program is transformed to a more concrete form with a set of trans-
forms. Each transform contains rules that prescribe various ways of transforming
components of a program. The selection of the transformations to be applied to pro-
gram variables is localized. By changing a single directive, a new transformation can
be applied to the abstract program, resulting in a probably different concrete pro-
gram. In this chapter we give the necessary background for transforms and transform
directives.
The declaration of a transform has the following form.
transform T(p:?1);
var avThat into var cvZct
?coupling invariant1
transform rules
(3.1)
14
15
with
local declarations
end
In the sequel we call the program that is being transformed the abstract program
and the program that is the result of the transformation the concrete program. The
same naming convention applies to parts of the abstract and concrete programs; for
example we use the terms abstract statement, abstract expression, concrete statement,
and concrete expression. If the abstract program is represented by a tree, we refer
to it as the abstract tree, which has abstract nodes. Similarly, we use the terms
concrete tree and concrete node.
An example of a transform is given in Figure 3.1. Transform BN has one abstract
variable, b: bool, and one concrete variable, j : nat. It has no parameters, and its
coupling invariant is b = j > 0. The parenthesized numbers on the left side of the
transform rules are used only for reference purposes and do not appear in an actual
transform. We will return to transform BN later, after we examine the components
of a transform.
transform BN;
(0)			var b:booi			into varj:nat
fCoupting invariant: CI(b,j) = b --H= j > OJ
(1)			II			itrue:booi?
(2)			II			ifaThe:booi?
(3)			II			i(BNIb)?
(4)			II			?BNjbj1 V BNjbj2?			=
(5)			II			IBNibil A BNjb?2?			=
(6)			I]			??BNjb?
(7)			II			frxp-x:booi?			--H
(8)			II			BNjb			into
(9)			II			BNibil := BNibi2			into
(10)			II			if BNjb then stmt-sl
else stmt-s2
II			var-v:booi := BNjb
(11)
end
0
(BNjj)
BNjjjl + BNjjj2
BNjjjl * BNUi2
if BNij > 0 then 0 else 1
if x then 1 else 0
BNjj >0
BNjjjl := BNjjj2
into if BNjj > 0 then si else s2
into v := BNjj > 0
Figure 3.1: BN implements a variable of type bool with a variable of type nat.
16
3.2 Components of a transform
Transform name and transform parameters
Each transform is uniquely identified by its name. The name of the transform in
Figure 3.1 is BN. A transform may have one or more parameters, which are enclosed
in parentheses following the name of the transform. If a transform has no parameters,
the parentheses are omitted. The parameters are separated by commas; both the
name and the type of each parameter have to be given. Transform T above has
parameters p, which have types t, respectively.
Abstract and concrete variables
In transform skeleton T of Section 3.1, av is a list of abstract variables (and at is
a corresponding list of their types), and cv is a list of concrete variables (and ct is
a corresponding list of their types). The abstract variables of a transform describe
the kinds of program variables on which the transform can be applied. The concrete
variables of a transform describe the program variables that are generated as the
result of applying the coordinate transformation that is described by the transform.
The two lists av and cv need not have the same length. Both are lists of dum-
mies, in that their consistent renaming throughout the transform will not change the
meaning of the transform.
The abstract variables of a transform are matched to the program variables on
which the transform is applied (with a transform directive). The concrete variables
of a transform are used for generating the appropriate program variables that result
from the coordinate transformation. In a later section, we discuss how the abstract
and concrete variables of a transform are used.
Coupling invariant
The coupling invariant, a predicate, relates the abstract and concrete variables. The
coupling invariant has no bearing on the transformation process, which is purely
syntactic. It is used by the author of a transform for proving the correctness of each
transform rule. Later in this section, we discuss the proof obligations for the author
of a transform.
Consider a transform T that transforms vl:tl to v2:t2, and let I(vl, v2) be its
coupling invariant. The coupling invariant of T gives rise to the definition of a repre-
sentation of an expression according to T. An expression r: t2 is a T-representation
of an abstract expression e:tl iff I(e, r) holds. For example, for a variable v:complex
17
that is represented by
u: record re, im:real end
the coupling invariant is v = u.re + i u.im.
Transform rules
Each rule in the list of transform rules describes a way of replacing an expression or
statement that involves one or more abstract variables. Each rule may have one of
the following forms.
P? expression-pattern
fPi statement-pattern
into expression-replacement
into statement-replacement
A transform rule may be preceded by a precondition (P, in the example above)
enclosed in braces. The user of a transform has the obligation to verify that the
precondition of a rule is satisfied at the place in the program where the rule is
applicable. The precondition has no effect on the transformation process, which is
a syntactic process.
The first kind of rule prescribes the transformation of an expression that may
contain abstract variables or expressions. Whenever expression-pattern matches an
expression e of an abstract program (pattern matching is defined in Section 4.3),
e can be replaced by the corresponding instance of expression-replacement.
The second kind of rule prescribes the transformation of a statement that may con-
tain abstract variables or expressions. Whenever statement-pattern matches a state-
ment 8 of an abstract program, 5 can be replaced by the corresponding instance
of statement-replacement.
The rules above describe the transformation of an expression or statement. There
is a third kind of rule, a representation rule, which has the following form
PJ ?expression-patternj = expression-replacement representation
A transform may have rules of the third kind only if it transforms exactly one abstract
variable to one concrete variable. A representation rule prescribes a way of construct-
ing a representation of an expression. If expression-pattern matches an expression
of an abstract program, then the corresponding instance of expression-replacement
is used to construct the specified representation of the expression. The type of the
corresponding instance of expression-replacement is the same as the type of the con-
crete variable of the transform whose representation is constructed. A representation
of an expression depends on the representations and/or transformations of its subex-
pressions. The representation of a variable according to a transform T is prescribed
18
by the first into rule of T, and the representations of constants and expressions are
prescribed by other transform rules of T. A pattern can refer to a specific represen-
tation of an expression, which can be used in the corresponding replacement of the
transform rule. The set of representation rules typically form a recursive definition
of the representation of any expression of the type.
The name of a transform identifies a representation of an abstract expression.
Thus, an abstract expression may have a representation according to transform Ti
(a Ti-representation), and a representation according to transform T2 (a T2-re-
presentation). The representation after symbol "j" in the third kind of transform
rule specifies which representation of an abstract expression is constructed when the
transform rule is applied. It also specifies the parameters of the transform whose
representation is constructed (if the transform has parameters). If "?representation"
is omitted, then the transform rule prescribes the representation of an expression
according to the transform in which the rule appears.
As mentioned above, an expression may have more than one representation with
respect to a set of transforms. A special kind of representation rule is the one that
specifies a conversion of representation: a function from one representation to an-
other. If expression-pattern in the third kind of rule above has no component sub-
patterns, then the corresponding rule is a conversion of representation. The syntax
of patterns and replacements of transform rules is discussed later in this section.
Proof obligations
The author of a transform has several proof obligations for proving the correctness
of each transform rule, depending on the kind of a transform rule. Here, we outline
the proof obligations for showing the correctness of a transform rule.
1.
2.
Rules that prescribe the transformation of an expression: The correctness of
the rule can be shown by proving that the pattern and replacement of the rule
are equal, under the assumption that the abstract and concrete variables that
appear in the pattern and replacement satisfy their coupling invariants.
Rules that prescribe the transformation of a statement: The correctness of the
rule can be shown by proving that the simultaneous execution of the pattern
and replacement of the rule maintains the coupling invariant, under the as-
sumption that the abstract and concrete variables that appear in the pattern
and replacement of the rule satisfy their coupling invariants.
3. Rules that prescribe the representation of an expression: The correctness of
the rule can be shown by proving that the pattern and replacement satisfy
the coupling invariant, under the assumption that the abstract and concrete
19
variables that appear in the pattern and replacement of the rule satisfy their
coupling invariants.
[MG9O,Mor89] develop a calculus for data refinement of programs. In doing so,
they give proof rules for the correctness of pattern-replacement pairs (in a different
notation and setting). Their rules are more complicated than ours but on the other
hand they are more powerful; they can be used in place of ours. In this thesis we cover
the algorithms for the transformation process, not issues of correctness of transforms.
Rule patterns and replacements
In this section, we discuss the syntax of patterns and replacements of transform rules.
Examples are given using transform BN of Figure 3.1.
A pattern of a transform rule may have one of the following forms.
1.
2.
3.
4.
5.
An abstract statement operator applied to subpatterns. For example, if stmtop
is an abstract statement operator of arity n and p is a list of n patterns,
then stmt?op p is a pattern. Pattern BNjbj1 BNjbj2 of rule (9) of BN is
an example.
An abstract expression operator applied to subpatterns. For example, if exp?op
is an abstract expression operator of arity n and p is a list of n patterns, then
exp?op p is a pattern. Pattern BNjbjlVBNjbj2 of rule (4) of BN is an example.
A reference to a representation of an expression. For example, if T is the
name of a transform and a is the name of its abstract variable, then Tja is
a pattern. Different instances of the same representation in the same pattern are
distinguished by a number after a second "j" symbol. For example, Tjajl and
Tj aj2 refer to two (possibly different) T-representations of different subtrees of
the abstract tree. Pattern BNj bj 1 of rule (4) of BN is an example of this case.
strnt-s is a pattern, where 8 is an identifier. The scope of s is the transform
rule in which it appears. If strnt-s appears more than once in a transform rule,
then all occurrences of strnt-s refer to the same s. Pattern strnt-s1 of rule (10)
of BN is an example.
exp-e:t is a pattern, where e is an identifier and t is a type. The scope of e is
the transform rule in which it appears. If exp-e:t appears more than once in
a transform-rule pattern, then all occurrences of exp-e:t refer to the same e.
Pattern exp- e: bool of rule (7) of BN is an example.
6. var-v:t is a pattern, where v is an identifier and t is a type. The scope of v is
the transform rule in which it appears. If var-v: t appears more than once in
20
a transform-rule pattern, then all occurrences of var-v:t refer to the same v.
Pattern var-v: boot of rule (11) of BN is an example.
7. const-c?reJ:t is a pattern, where cis an identifier and reis a regular expression
that describes constants of type t. This pattern can be simplified to c:t if re
is just a string c. The scope of c is the transform rule in which it appears.
Pattern false:boot of rule (2) of BN is an example. The same pattern can be
written as const-faThe?fatseJ:boot.
8. (p) is a pattern, if p is a pattern. (BNjb) of rule (3) of BN is an example.
A replacement of a transform rule has one of the following forms.
1. A concrete statement operator applied to subreplacements. For example, if
stmLop is an abstract statement operator of arity n and r is a list of n re-
placements, then stmLop r is a replacement. Replacement BNjjjl := BNjjj2
of rule (9) of BN is an example.
2. A concrete expression operator applied to subreplacements. For example,
if exp?op is an abstract statement operator of arity n and r is a list of n
replacements, then exp?op ris a replacement. Replacement BNijil * BNjjj2 of
rule (5) of BN is an example.
3.
A reference to a representation of an expression. For example, if T is a trans-
form, a is the name of its abstract variable and c is the name of its concrete
variable, then Tic is a replacement. This replacement corresponds to the rep-
resentation of an expression that is referred to by pattern Tja of the same
transform rule. Different instances of the T-representation in the same re-
placement are distinguished by a number that follows a second ??jfl symbol. For
example, Tjcjl and Tjcj2 refer to two (possibly different) T-representations of
different subtrees of the abstract tree. The BNjjjl part of the replacement of
transform rule (4) of BN is an example.
4. s is a replacement, where s is a name defined with strnt-s in the pattern of
the corresponding transform rule. The si part of the replacement of transform
rule (10) of BN is an example.
5.
6.
e is a replacement, where e is a name defined with exp-e:t in the pattern of
the corresponding transform rule. The x part of the replacement of transform
rule (7) of BN is an example.
v is a replacement, where v is a name defined with var-v:t in the pattern of
the corresponding transform rule. The v part of the replacement of transform
rule (11) of BN is an example.
21
7. c is a replacement, where c is a name defined with coust-c?re?:t in the pattern
of the corresponding transform rule.
8. A reference to a parameter of a transform is a replacement. For example, if p
is a parameter of a transform T whose abstract variable is a, then Tjp is a re-
placement. This replacement corresponds to the parameter that is associated
with the T-representation that is referenced by the Tj a part of the correspond-
ing pattern of the transform rule. Different instances of the same parameter
in the same replacement are distinguished by a number following a second
symbol. For example, Tipil and Tjpj2 refer to the two (possibly different)
instances of parameter p of the T-representations that are referenced by Tjajl
and Tj aj2, respectively, in the corresponding pattern.
9. (r) is a replacement, where r is a replacement. Replacement (BNjj) of trans-
form rule (3) of BN is an example.
In the case of a rule that specifies a representation of an expression, the replace-
ment of the rule has to specify which concrete representation of the abstract expres-
sion is constructed and the values of the parameters of the corresponding transform.
For example, if a rule specifies the construction of the T-representation of an expres-
sion, then this is denoted by the symbols "I T" that follow the replacement (assuming
that transform T has no parameters). If no such symbols follow the replacement,
then the rule specifies a representation according to the transform in which it appears.
Assume that T has an abstract variable a and parameters p. Each reference Tja
to a T-representation of an expression has an instance of parameters p associated
with it. We use the notation T7pj (0 < i < #?) to refer to parameter p? that is
associated with the T-representation of an expression.
If a transform rule specifies the construction of a T-representation for an expres-
sion, then it has to specify the values of parameters of T. For example, assume
that T has one parameter p and one abstract variable a. If a rule specifies the T-
representation of an expression and the associated value of parameter p is two times
the value of p that is associated with Tja, then the notation jT(2 * Tip) is used for
the representation part of the rule. The value of the parameter of the resulting rep-
resentation can be a function of the parameters of the transforms that are associated
with transform references only.
3.2.1 Local declarations
A transform may contain declarations that are local to its body, which are given
after keyword with. If a transform contains no local declarations, then with may be
22
omitted. Local declarations involve declarations of constants, functions, procedures,
and types. The scope of these declarations is the rule-replacements of the transform.
3.3 An example of a transform
Consider again transform BN, which was shown in Figure 3.1 earlier in this chapter.
BN is an example of a transform for the transformation of variables of type boot.
BN provides a way of replacing a variable of type boot by a variable of type nat and
ways of replacing boolean expressions that contain the operators V, A, and by new
ones that do not contain these operators.
Here we discuss some points about transform BN
As mentioned before, transform BN has no parameters. The precondition of
each rule is true and is omitted. Each one of the rules (1)--H(7) prescribes the
construction of a BN-representation, so the symbol "jBN" is omitted from the
end of the rule.
Transform BN contains rules that define the BN-representation of boolean con-
stants true and false (rules (1) and (2)). According to BN, one representation
of true is natural number 1 and one representation of false is 0.
Transform BN contains rules that define the BN-representation of boolean
expressions that are formed using operators V, A, and from the BN-r&
presentations of their subexpressions (rules (4), (5), and (6)). For example,
let el V e2 be a boolean expression that appears in a program (where e1 and e2
are boolean expressions). If e1 has a BN-representation ri (say) and e2 has
a BN-representation r2 (say), then according to rule (4) the BN-representation
of el V e2 is ri + r2.
Rule (7) prescribes the BN-representation of any expression of type boot. It is
a conversion of representation from the default representation of an expression
(which is the expression itself) to its BN representation.
o+ Rule (8) prescribes the transformation of an expression that has a BN-repres-
entation. If expression e has a BN-representation r, then according to rule (8)
the transformation of e is r > 0.
o+ Rule (9) prescribes the transformation of a statement that involves abstract
variables that have BN-representations.
Rule (10) prescribes the transformation of an if statement whose boolean ex-
pression has a BN-representation. (This rule is not needed in BN and is pre-
sented only as an example).
23
Rule (11) prescribes the transformation of an assignment statement whose right-
hand-side expression has a BN-representation. (This rule is not needed in BN
and is presented only as an example).
The correctuess of BN can be shown by proving each rule correct, as was discussed
earlier. For example, the correctness of rule (5) of BN is shown as follows.
bi A b2
((CI(bl,jl), CI(b2, c2)))
ji >OAj2>O
((since ji, j2 are of type nat)?
ji *j2 >0
3.4 Transform directives
A transform directive specifies a transform to be applied to a variable. There are two
kinds of transform directives.
Directive
change v using T(?w)
specifies that transform T, with arguments w, is to be applied to variables v. T is
applicable to v only if the types of v are the same as the types of the abstract variables
of T. When a transform directive is processed, v is replaced by new variables that
have the same types as the concrete variables of T. Different variables of the same
type may be transformed with different transforms.
For example, if abstract variable a: bool is to be transformed with BN, the trans-
form directive would be the following.
change a using BN
Transform BN is applicable to a since the type of variable a is the same as the type
of the abstract variable of BN. When this directive is given, a is replaced by a new
variable a? (say) of type nat. BN has no parameters. If BN had one parameter of
type int, then a legal transform directive would had been the following.
change a using BN(1O)
A second kind of directive may be given for the transformation of variables and
expressions. When directive
default t using T(?w)
24
is given, then, by default, every variable of type t that is not transformed by an ex-
plicit directive is transformed with T. In addition, every expression of type t is
removed from the program.
3.5 Examples of using a transform
Consider transform BN of Figure 3.1 and suppose that a program contains the fol-
lowing definitions and directives.
var a:bool;
var b:bool;
change a using BN;
change b using BN
According to these directives, variables a and b are transformed with transform BN.
The definitions of a and b are replaced by
var a?:nat;
var b?:nat
where a? and be are fresh concrete variables that correspond to a and b, respectively.
Variables a? and be are the BN-representations of a and b, respectively.
Suppose that an abstract program contains subexpression a V b. According to
rule (4) of transform BN, its BN-representation is a? + be since a? is the BN-
representation of a, and be is the BN-representation of b. Rule (8) of transform BN
can be used to construct the following transformation of the previous expression
+ be) > 0.
Employing rule (9) of transform BN, a transformation of statement
a a v b
is the following.
+ be
Suppose that variable c is defined in the abstract program as
var c:bool
and that no directive is given for its transformation. Then, statement
c a V b
25
gets transformed to
c			(a? + bc) > 0
as prescribed by rule (11) of BN. On the other hand, statement
c c V b
gets transformed to
c c V (bc > 0).
It should be emphasized that a transform can be a partial implementation of
a data type [Pri87]. Consequently, it may not provide implementations for all op-
erations of the data type. In addition, different transforms may provide different
partial implementations of the same data type. A given transform is suitable for
the implementation of an abstract data type that is used in a program if it provides
implementations for all operations of the data type that are used in the program. For
example, it would be acceptable if transform BN did not contain any representation
rule for operator V. In that case, BN could not be used in a program to transform
a boolean expression that contains operator V.
3.6 Program transformation
A program is transformed successfully with a set of transforms T and a set of trans-
form directives v if
1. For every list of program variables v for which a directive
change v using T(w)
is in V and T is applicable to v, the transformation removes all occurrences of
variables v from the program.
2. For a directive
default t using T(?w)
in V, every variable of type t that is not transformed by an explicit directive
is transformed with T, and every expression of type t is removed from the
program.
If the abstract program is type correct and the transforms have been proved correct,
then the transformed program is guaranteed to be type correct. Furthermore, if the
abstract program is correct, and all preconditions of transform rules are satisfied at
the places of the abstract program where the rules are applied, then the transformed
program is correct.
Chapter 4
Transforming variables that have
base types
4.1 Introduction
We present an algorithm for processing program transformations as described by
the transform construct. The algorithm constructs a coordinate transformation of
an abstract program based on a set of transforms and transform directives applied
to it.
4.2 Overview
The algorithm for processing transforms and transform directives works in two phases.
During the first phase, the source program, the transforms, and the transform direc-
tives are processed and converted to an internal representation, and the necessary
lists and tables are constructed. The second phase carries out the actual program
transformation. It processes the internal representation of the source program, and
applies the transformations as directed by the transforms and the transform direc-
tives.
In this section, we give an overview of the transformation algorithm, we describe
the representation of abstract trees, transforms, and transform directives, and we de-
fine functions that will be used later.
Symbol table entries for variables
The algorithm makes use of a symbol table where information about program iden-
tifiers is stored. The symbol table has an entry for each abstract program variable,
26
27
where its name and type is stored. It also has an entry for each concrete variable that
is generated as the result of applying a transform directive to one or more abstract
program variables.
Suppose transform T transforms vl:tl to v2:t2. For a directive
change v using T(?w)
or a directive
defa?1t ti using T(w)
a new variable Vc (say) of type t2 is generated and a symbol table entry is cre-
ated for it. The symbol table entry of v contains a reference to transform T, its
arguments w, and the corresponding concrete variable Vc.
Suppose T transforms 71:71 to 72:72. For a directive
change v using T(?w)
a list of new variables v? (say) of corresponding types 72 is generated and a symbol
table entry is created for each one of them. The symbol table entry of each Vj,
o < ? < #?v, contains a reference to transform T, its arguments w, every other
variable in v, and the list of the corresponding concrete variables v?.
Let v be an abstract program variable. The following functions are used later
and are assumed to be primitive.
1. geLconc?vars(v) is the list of concrete variables that are created when trans-
form T is applied to v.
2. geLabs?vars(v) is the list of abstract variables that are transformed along with v
when transform T is applied to v.
3. get?trans(v) is the transform that is applied to program variable v.
The generation of concrete variables that result from application of a transform
to a list of program variables is discussed in Section 4.6.
Abstract tree nodes
As mentioned before, the first phase converts the source program into an internal
representation, which is a tree (henceforth referred to as the abstract tree). A node
of the abstract tree (an abstract node) has one of the following forms.
1.
An abstract statement operator applied to substatements and subexpressions.
For example, if stmt?op is an abstract statement operator of arity n and s is
a list of n statements or expressions, then stmLop 5 is an abstract statement
node.
28
2. An abstract expression operator applied to subexpressions. For example, if
exp?op is an abstract expression operator of arity n and e is a list of n expres-
sions, then exp?op e is an abstract expression node.
3. A node that is labeled with an abstract variable av. For example var v is
a node labeled with variable v.
4. A node that is labeled with a constant ac. For example const c is a node
labeled with constant c.
5. A node that is labeled with a list of declarations of variables and their types.
For example deci ?v:?t is such a node.
We assume that the source program has been type-checked and that each node of
the abstract tree is annotated with its type. Statement nodes have type void.
With each node n of the abstract tree we associate the following values.
1. V(n): is true iff there are variables that need to be replaced in the subtree
rooted at n.
2. C(n): is true iff there are constants that need to be replaced in the subtree
rooted at n.
3. reprs(n): set of representations of node n.
4. trans(n): transformation of node n or I if n has no transformation.
In a later section we discuss how these values are constructed.
For a node n of the abstract tree, the following functions are used later and are
assumed to be primitive.
1. type?of(n) is the type of node n.
2.			is?var(n)			"n is a variable".
3. i&const(n) --H= "n is a constant".
4. get?var(n) is the variable at node n.
5. get?const(n) is the constant at node n.
6. mk?stmt?node(stmLop,?n) is a statement node that has operator stmt?op and
children n.
7. mk?exp?node(exp?op,?n) is an expression node that has operator exp?op and
children n.
29
8. mk?vannode(v) is a node labeled with variable v.
9. mk?con?t?node(c) is a node that is labeled with constant c.
10. mk?decLnode(?v, t) is a declaration node labeled with variables v that have
corresponding types t.
In the following, the same name is used interchangeably for a node of the abstract
tree and for a subtree of the abstract tree that is rooted at that node.
Transforms
The transforms are represented by a table and three lists of rules. Each transform
rule r is represented by a record that contains the following information.
1. The pattern of r.
2. The replacement of r.
3. An indication if ? is a representation or a transformation rule.
4.
If r is a representation rule, the representation that is constructed (i.e. the
name of the corresponding transform, and the expressions for constructing the
associated parameters).
All representation rules that are not conversion-of-representation rules are kept in
a list 81. Similarly, all conversion-of-representation rules are kept in a list 82 and all
transformation rules form a list 83. Eor a rule r, the following functions are used
later, and are assumed to be primitive.
1. pattern(r) is the pattern of rule r.
2. replacement(r) is the replacement of rule r.
3. representation(r) is the name of the transform whose representation is con-
structed by rule r.
4. parameters(r) is the list of replacements for constructing the parameters that
are associated with representation(r).
5. tran??of(r) is the name of the transform that contains rule r.
For each transform, its parameters, the list of its abstract variables and their
types, and the list of its concrete variables and their types, are kept in a record.
For a transform T, the following functions are used later, and are assumed to be
primitive.
30
1. parameters(T) is the list of parameters of transform T.
2. abs?vars(T) is the list of abstract variables of transform T.
3. conc?vars(T) is the list of concrete variables of transform T
In the sequel, T is the set of transforms that are used to transform a program.
The form of transform-rule patterns that are used in the algorithm is the following.
p = stmt?op p exp?op p Tjajk stmt-s exp-e:t var-v:t const-c(rei:t I(?)
The form of transform-rule replacements that are used in the algorithm is the follow-
ing.
r = stnit?op r exp?op r Tjcjk s e v c Tjpjk
Patterns and replacements are discussed in Section 3.2.
Transform directives
All transform directives are kept in a set V. Each directive of the form
change v using T(?w)
is represented by a record that contains an indication that it is a change directive,
the list of variables v, the name of transform T, and the list of parameters w.
Each directive of the form
default t using T (?w)
is represented as a record that contains an indication that it is a default directive,
the name of type t, the name of transform T, and the list of parameters w.
For a directive D in V, the following functions are used later, and are assumed
primitive.
1. i&change(D) = "D is a change directive".
2. is?defauU(D) = "D is adefault directive"
3. vars?of(D) = v, if D is a change directive.
4. type?of(D) = t, if D is a default directive.
5. trans?of(D) =
6. params?of(D) =
31
Program transformation
The first phase of the algorithm is essentially a front-end that processes the source
program and converts it into an intermediate form [ASU86]. The details are omitted.
The second phase of the algorithm carries out the transformations described by
the transforms, and the transform directives. It performs a bottom-up traversal of the
abstract tree. At each leaf of the tree, the algorithm uses the transform directives to
construct the representation of the node. As each node is visited, the representations
and transformation for that node are constructed.
Let n be an expression, a variable, or a constant node. If ?( V(n) V C(n)), then
the transformation algorithm need not construct any transformations for it (but it
tries to construct representations for the node, if possible, since they may be needed
in the transformation of the program). If V(n) V C(n), then the transformation
algorithm tries to construct representations and a transformation for n, if there is no
directive
default t using T(?w)
in V, where type?of(n)
Let n be a statement node. If ?( V(n)V C(n)), then the transformation algorithm
need not construct any transformation for n. If V(n)V C(n), then the transformation
algorithm tries to construct a transformation for it.
To construct a representation of an internal node n of the abstract tree, the al-
gorithm tries to match the patterns of the representation rules with n. If a match is
successful, the corresponding replacement of the rule is used and the concrete repre-
sentation of the node is constructed as prescribed by the replacement. Constructing
conversions of representation and transformations of a node is done in a similar way,
by using the list of conversions-of-representation rules and the list of transformation
rules, respectively.
After the construction of representations and transformations for the abstract
program is complete, the algorithm checks if all directives in V are satisfied: if all
variables v for which a change directive is given in V have been replaced by new
ones and if the transformed program does not contain any expressions of type t if
a directive "default t using ..." is in V.
Given a program, a set of transforms and a set of transform directives, it may not
be possible to find a transformation for the program. In such cases, the algorithm
returns an indication that no transformation is possible. On the other hand, it
may be possible to construct more than one transformation for the program. In such
cases, heuristic methods can be employed to construct an appropriate transformation.
The complexity of the structure of a pattern, the cost of the operations involved in
a replacement, and the relative order of a pattern with respect to other patterns can
32
serve as some simple heuristics for choosing the most suitable transformation rule to
apply.
4.3 Pattern matching
Let Id be the domain of names and AT be the set of natural numbers. Let AbsNodes
be the domain of abstract tree nodes. A binding is an ordered pair of the form
(X, Y), where X is a member of Id + (Id x AT) and Y is a member of Id + AbsNodes,
i.e. a binding is a member of the cartesian product
(Id + (Id x AT)) x (Id + AbsNodes).
An environment E is a set of bindings that denotes a function, i.e. for each ele-
ment X of Id + (Id x AT) there is at most one pair (X, Y) in E. The domain of
an environment E is the set
dom(E) = : (? Y : (X, Y) ? E)i
and the range of an environment E is the set
rng(E) = ty I: (?X I: (X, Y) ? E)J.
The empty environment is denoted by ?. We distinguish a special environment, the
fail environment, that is denoted by t. The fail environment is different from all
other environments, including $. Its importance will be explained later, when the
definition of pattern matching is given.
In the sequel, notation [X H>E Y] is used for binding (X, Y) in E. If environ-
ment E is obvious from the context, then it is omitted from the subscript of ?.
If E is an environment and X belongs to dom(E), then we write E(X) for the Y
in rn9(E) for which (X, Y) is in E.
Pattern matching is defined to be a function
match: pattern x node x environment H environment.
Intuitively match(p, n, E) is
o+ An environment that augments E by the new bindings that result from the
pattern match of p and n, if p matches n with respect to E,
o+ I, if there is no match between p and n with respect to E.
The definition of match is given in Figure 4.1. ML-style pattern matching is used in
the definition.
Function match makes use of three functions, which we describe informally here.
33
1. has?repr(n, T) =--H "subtree n has a T-representation"
2. match?re(r, s) = "string 5 belongs to the language of regular expression r",
3. rank(??c) = (I i I 0 < i < #?c : c =
Function ha&repr will be described in more detail later, match?re is assumed to be
primitive. There are efficient algoritlims for deciding if a string of characters belongs
to the language of a regular expression [HU79].
4.4 Replacement Instantiation
As explained in Section 4.3, pattern matching is defined to be an environment that
binds names and representation references of a pattern to names and nodes of the
abstract tree. When a pattern p matches a tree node n, the corresponding rule that
contains p can be used to construct a representation or a transformation of n. To con-
struct such a representation or transformation of n, the corresponding replacement
of the rule is used along with the environment of pattern matching.
Let r be a transform rule and n be an abstract tree node. Let also E be
match(pattern(r), n, ?), and assume that E # I. Transform rule r is applicable
with respect to environment E if
1. If 5 appears in replacement(r), where 5 was defined by stmt-s in pattern(r)
V(E(s)) v C(E(s)) ? has?trans(E(s)).
2. If e appears in replacement(r), where e was defined by exp-e:t in pattern(r)
V(E(s)) V C(E(s)) ? has?trans(E(s))
and there is no directive "default t using ..." in V.
3. If v appears in replacement(r), where v was defined by var-v:t in pattern(r),
then there is no directive "default t using ..." in V.
4. If c appears in replacement(r), where c was defined by const-c?re1:t in
pattern(r), then there is no directive "default t using ..." in V.
5. If the syntactic classes of the components that are used in the replacement
instantiation are the same as those that are required for the operator that
appears in the replacement. We distinguish four syntactic classes: stmt, exp,
34
match(p, n, E)
match(p,n,I)			I
match(stmLopi p, stmLop2 n,
case stmLop1 = stmLop2 A #p = #n MatchList(p,?n, E)
otherwise I
match(exp?op1 p, exp?op2 n,
case exp?op1 = exp?op2 A #?p = #W A t?ipe?()i(p) = type?of(n)
MatchList(p,?n, E)
otherwise I
match(Tjajk, n,
case (T,k) E dom(E)AE((T,k)) = n E
case			? dom(E) A
(has?repr(n, T) v (i&var(n) A #abs?vars( T) > 1 A
rank( c, abs?vars( T)) = rank(geLvar(n), get?abs?vars(get?var(n)))))
Eu?[(T,k)
otherwise I
match(stmt-s, n,
case s ? dom(E) A E(s) = n E
case 8 ? dom(E) E U f[s H
otherwise I
match(exp?e:t, n,
case t?ipe?of(n) = t A e ? dom(E) E u ?[e n]1
case t?e?of(n) = t A e E dom() A E(e) = n E
otherwise I
match(var-v:t, n,
case t?p&of(n) = t A v ? dom(E) A E(v) = geLvar(n) E
case t?p&of(n) = t A is?var(n) A v ? dom(E) E u f[v get?var(n)j)
otherwise I
match(const-actrej:t, n,
case tvpe-of(n) = t A is?const(n) A match?re(re, geLconst(n))
E u ?[ac i' geLconst(n)]J
otherwise I
otherwise I
end match
MatchList(?p,?n, E)
if #?p = 1			match(?p0,no, E)
II #p > 1 H MatchList(?p[1..],w[1.i, match(p0,?no, E))
fi
end MatchList
Figure 4.1: Definition of pattern matching.
35
var, and const. Function app', shown in Figure 4.2, is the definition of this
requirement. Its type is
inst: replacement x environment H bool.
kin&of(op, i) is the syntactic class of component i of operator op. We assume
that it is a primitive function.
app'(stmLop r, = (A i 0 < i < #?r : kind?of(stmt?op, i) = kind(r?, E))
app'(exp?op r, = (A i 0 < i < #?r kind?of(exp?op, i) = kind(r?, E))
app'(var v, = true
app'(const v,E) = true
kind(stmLop r, E) = stmt
kind(exp?op r, = exp
kind(Tjcjk,E) = if is?var(geLnrepr(E((T,k)), T,c)) then var else exp
kind(stmt-s, E) = stmt
kind(exp-e, E) = exp
kind(var-v,E) = var
kind(const-c, E) = const
kind(Tjpjk,E) = exp
Figure 4.2: Definition of app.
We write app(r, E) to denote that transform rule r is applicable with respect to
environment E.
Replacement instantiation is defined to be a function
inst: replacement x environment			node.
Intuitively, inst(r, E) is the instantiation of replacement r with respect to environ-
ment E.
For a transform rule r we define inst(replacement(r), E) only for cases in which
E = match(pattern(r), n, ? 1 cand app(r, E)
where n is an abstract tree node. The definition of inst, given in Figure 4.3, makes
use of the following functions.
1. has?trans(n) = "n has a transformation",
2. geLrepr(n, T) is the T-representation of node n,
36
3. geLparam(n, T, p) is the value of parameter p that is associated with the T-
representation of abstract tree node n.
Functions get?param and get?repr will be described in more detail later.
4.5 The main algorithm
We present the main algorithm for processing program transformations. We as-
sume that the abstract program, the transforms and transform directives have been
preprocessed and presented to the algorithm in an internal form, as discussed in Sec-
tion 4.2. We also assume that if there is a directive "default t using .." in D, then
no transform in T has concrete variable of type t.
The abstract program to be transformed is presented to the algorithm as a tree n.
Figure 4.4 contains the transformation algorithm. Later sections discuss parts of the
algorithm, like functions mk?repr, closure, and mk?trans. The algorithm is invoked as
xform(n)
where n is the root of the abstract tree. It returns a tree n', which is the coordinate
transformation of n according to T and D, if such a tree exists, 1 otherwise. Tree n'
is the internal representation of the concrete program.
In several places, the algorithm in Figure 4.4 has the following form.
Definition of variable v;
if "change v using T(?w)'7 c D then
The semantics is the following. T gets bound to the name of a transform at the
conditional expression of statement if and this name is used later in expressions
involving T.
4.6
Representations
variables
and transformation of
The transformation of variables is directed by transform directives. A transform
directive specifies the transform to be used for the replacement of an abstract program
variable. We assume that each program variable has a symbol table entry where
information about the variable is stored. In addition, each concrete variable that is
generated as the result of applying a transform directive to a program variable has
a symbol table entry.
37
inst(r, E)
inst(stmt?op r, = mk?stmt?node(stmt-op, InstList(r, E))
inst(exp?op r, = mk?exp?node(exp?op, InstList(r, E))
inst( Tjcjk, E) = geLnrepr(E(( T, k)), T, c)
inst(s, E) = Comment For 8 defined in pattern stmt-s
if V(E(s)) V C(E(s)) trans(E(s))
II ?( V(E(s)) V C(E(s))) H E(s)
fi
inst(e, E) = Comment For e defined in pattern exp?e
if V(E(e)) V C(E(e)) idtrans(E(e))
II ?( V(E(e)) V C(E(e))) E(e)
fi
inst(v,E) =
mk?var?node (v)
inst(c,E) =
mk?const?node( c)
inst(Tjpjk,E) = geLparam(E((T,k)), T,p)
end inst
Comment For v defined in pattern var-v
Comment For c a constant
InstList(?r, E)
if #?r=O? []
II #?r> 0 inst(?ro, E) InstList(r[1.i, E)
fi
end InstList
geLnrepr(n, T, c)
if #abs?vars(T) = 1 get?repr(n, T)
II #abs?vars(T) > 1
mk?var?node (9et?conc?vars(?eLvar(n)) [rank( c, conc?vars ( T))])
fi
end geLnrepr
Figure 4.3: Definition of replacement instantiation.
38
i??pvt:
Ovtpvt:
Program P, set of transforms T, set of transform directives D.
Program P': the coordinate transformation of P according to T and D
if such a program exists, I otherwise.
xform(n:node)
trav(n);
if check(n) then return mk(n) else return I
end xform
f check(n) checks if the tree rooted at n has been successfully transformed, i.e.
1. For every leaf that is not in a subtree of a node that has a transformation and is
labeled with a variable v, no directive in D is applicable to v,
2. For every node mthat is not in a subtree of a node that has a transformation there
is no directive "default t using ..." in V with type?of(m) =
y
check(n:node)
check(dect v)
return trve
check(var v)
return "change v using ..." ? V v "default t?e?of(n) using ..." E V
check(const c)
return has?trans(n)v "default type?of(n) using ..." Ei V
check(exp?op n)
return has?trans(n)v ?("default t?pe?of(n) using ..." E V) v
(An I nEn : check(n))
check(stmLop n)
return has?trans(n)v (A n n E n : check(n))
end check
Figure 4.4: Main transformation algoritlim.
39
trav(n) traverses bottom-up the abstract tree rooted at n and constructs
the representations and transformations at each node of the tree.
y
trav(n:node)
trav(decl v:t)
if #v = 1 then
if "change v using T(?w)" ? D v "default t using T(w)" E D then
begin
Create new instance Vc having type prescribed by T
and make a symbol table entry for it;
get?abs?vars(v) := v; geLconc?vars(v) := Vc
end else skip
else
if "change v using T(w)" ? D then begin
Create new instances Vc having type prescribed by T
and make a symbol table entry for each one;
foreach v in v do
begin yet?abs?vars(v)			v; get?conc?vars(v) := Vc end
end
trav(var v)
if #abs?vars(geLtrans(v)) = 1 then begin
V(n) := "change v using T(?w)" E D v
"default t?e?af(n) using T(w)" e D;
C(n) := false;
reprs(n) := ? mk?vepr( T, mk?var?node (get?conc?vars (v) [0]),
InstL?st (parameters(T), [parameters( T) H ?w]))1;
ciosure(n); mk?trans(n)
end else
begin V(n) := false; C(n) := false; reprs(n) := ?; trans(n) := I end
trav(const c)
V(n) := false; C(n) := "default t?pe?of(n) using ..." E V;
reprs(n) := ?; closvre(n); mk?trans(n)
trav(exp?op n)
foreach n in n do trav(n);
n n E W : V(n)); C(n):=(V n n E n :
reprs(n) := ?; mk?reprs(n); closvre(n); mk?trans(n)
trav(stmt?op n)
foreach n inn do trav(n); V(n):=(V n n E n :
n n E W : C(n)); reprs(n) := ?; mk?trans(n)
end trav
Figure 4.4: (continued)
40
mk(n) traverses the abstract tree rooted at n and replaces each
node with its transformation if one has been constructed.
mk(n:node)
mk(decl v:t)
if #v = 1 then
if "change v using T(w)? E D v "default t using T(w)" E D then
return mk?decLnode (get?conc?vars(v), conc?t?pe ( T))
else return n
else
if "change v using T(?w)? E V then
return mk?decLnode (get?conc?vars(v), conc?t?pe ( T))
else return n
mk(var v)
if has?trans(n) then return geLtrams(n) else return n
mk(const c)
if has?trans(n) then return get?trans(n) else return n
mk(exp?op n)
if has?trans(n) then return get?trans(n)
else return mk?exp?node ( exp?op, mkList(w))
mk(stmLop w)
if has?trans(n) then return geLtrans(n)
else return mk?stmLnode (stmt?op, mkList(n))
end mk
mkList(?p)
if #p = 1 [mk(p0)]
II #p> `? mk(?p0)?mkList(p[1.i)
fi
end mkList
Figure 4,4: (continued)
41
or
Suppose T transforms vl:tl to v2:t2 and let v:tl be a program variable. If either
change v using T(?w)
default ti using T(w)
is given, then a new variable Vc (say) of type t2 is generated and a symbol table
entry for it is created. The declaration of v is replaced by
var v?:t2
In addition, for every leaf n of the abstract program tree that is labeled with v
true if "change v using T(?w)" is in D, or
V(n) =			"default t using T(w)" is in D
false otherwise
and C(n) = false. In addition, the following statements are executed for constructing
all representations and a transformation for node n.
reprs(n) := ?mk?repr( T, mk?vannode(v?),
InstL?st(parameters( T), [parameters( T) H
closure(n); mk?trans(n)
The T representation of v is variable Vc with associated parameters w. Set reprs(n)
contains initially the T representation of n. closure(n) constructs all representations
that can be derived by using conversion-of-representation rules. Functions closure,
mk?repr, and mk?trans are defined later.
Suppose T transforms vl:Fl to v2:t2.
a directive
As mentioned in a previous section, for
change v using T(?w)
a list of new variables v? (say) of corresponding types 72 is generated and a symbol
table entry is created for each one of them. The declaration of v is replaced by
var ?v?:t2.
For every leaf n of the abstract program tree that is labeled Vj, for 0 < i < #?v,
V(n) = true, and C(n) = false. In addition, the following statements are executed
for constructing all representations and a transformation for node n.
reprs(n) := ?; trans(n) := I
R?ecall that a transform like T that transforms lists of variables does not contain
representation rules for expressions.
42
4.7 Representations and transformations of
constants
Constants of a type are introduced in the type definition. The concrete form of
a constant is described by a regular expression. Constants may appear in a program
and may need to be transformed before further transformation of the program can
proceed. The transformation of a constant c:t can only be directed by a directive
default t using T(?w).
A transform T that transforms vl:tl to v2:t2 may contain rules for the trans-
formation of constants of type ti. The pattern of each such rule, const-id?re):t1,
is a regular expression (re) that describes one or more constants of type ti. The
replacement is an expression that may contain id.
For an abstract tree node n that is labeled with a constant c:t, V(n) = false and
true if "default t using T(w)" is in D
C(n) =			false otherwise.
In addition, the following statements are executed for constructing all representations
and a transformation for node n.
reprs(n) := ?; closure(n); mk?trans(n).
4.8 Representations and transformations of
expressions
If n is an expression node exp?op n, then
V(n) = (Vn n?n :
C(n) = (Vn n?n			C(n))
As mentioned in Chapter 3, each expression may have more than one represen-
tation. A representation rule provides a way of constructing a representation of
an expression. These rules can be classified in two categories.
Rules that provide a way of constructing the representation of an expression
from the representations and/or transformations of its subexpressions. These
rules are kept in a set si
o+ Conversion-of-representation rules, which convert one representation of an ex-
pression into another. All conversion-of-representation rules are kept in a set ?2
43
Application of a transform rule to a node is a function
apply: rule x node repr t I
intuitively, apply(r,n) is
o+ A representation that is constructed for abstract tree node n using rule r.
o+ I, if r can not be applied to node n.
Type repr is discussed shortly. The definition of apply is given in Figure 4.5. Function
apply uses app whose definition is given in Section 4.4.
apply(r, n)
var E: environment;
E			match(paUern(r),n,?);
if  # I cand app(r, E) then
mk?repr(trans?of(r), inst( replacement(r), E), InstList (parameters(r), E))
else I
end appl?
Figure 4.5: Application of a transform rule to an abstract tree node.
Function apply makes use of mk?repr, which we describe here. mk?repr( T, r, rl)
is a T-representation of an expression whose replacement instantiation is r and list of
replacement instantiations ri for the transform parameters that are associated with
the T-representation. Each such representation is implemented with a record that
contains the following information.
1. The name of the transform whose representation is constructed.
2. The representation of the expression according to this transform.
3.
A list of the values of the parameters of the transform whose representation
is constructed. The values of the parameters appear in the same order as the
parameters of the transform in the transform declaration.
We denote [T, r, rl] such a record. Type repr is the type of these records. Functions
has?repr, get?repr, and get?param that were used previously are defined as follows.
1. has?repr(n, T) (? r, rl I: [T, r, rlj ? reprs(n)).
2. getrepr(n, T) = (a rl [T, r, rl] E reprs(n) :
44
3. getparam(n, T,p) =
r [T, r, rlj E reprs(n) : rl[rank(p,parameters(T))j).
Wfth each expression node n of the abstract tree is associated a set reprs(n)
of all representations of n. At each expression node n of the abstract tree, the
transformation algorithm constructs the set reprs(n) of representations of n from
the representations and/or transformations of the subtrees of n. Function mk?reprs
of Figure 4.6 takes a node of the abstract tree as an argument and constructs the
representations of the node.
mk?reprs(n)
var t:repr + I;
for r in 81 do
t := appi?(r,n);
if t # I then
if has?repr(n, representation(r)) then
if (? T, ri t = [r, T, r1? : r) ? geLrepr(n, representation(r)) then
reprs(n)			reprs(n) --H fgeLrepr(n, representation(r))1 u ?t)
else skip
else reprs(n)			reprs(n) U ?t)
end
end mk?reprs
Figure 4.6: Construction of representations of an expression.
If two different patterns match the same node n, then one of the two has to be
chosen for the representation of n to be constructed. It does not matter which one
is chosen. Predicate ? decides which representation is preferable. Since the test for
choosing the appropriate pattern to be used is localized, more elaborate heuristics
may be employed for choosing the most suitable pattern.
The conversion-of-representation rules are like the other representation rules, with
the exception that the corresponding pattern has no subpatterns. These rules de-
scribe the conversion of one representation of an expression to another. Before a con-
version of representation rule can be applied to convert the T1 representation of
an expression to a T2 representation, the T1 representation has to be constructed.
This can be accomplished by maintaining a set S2 that contains the conversion
of representation rules that have not been used yet. As mentioned in a previous
section, all conversion-of-representation rules are kept in set 82. The algorithm
for applying the conversion of representation rules in the appropriate order, when
abstract tree node n is visited is shown in Figure 4.7. If n is an abstract tree
45
node, then closure(n) augments reprs(n) with representations that are obtained with
conversions-of-representation rules.
closure(n)
var S2			52;
var t:repr + I;
do
for r in S2 do
t := apply(r,n);
if t $ I then begin
S2 := S2 --H
if has?repr(n, representation(r)) then
if (? T, ri t = [r, T, ri] r) ? geLrepr(n, representation(r)) then
reprs(n) := reprs(n) --H ?geLrepr(n, representation(r))? u ?ty
else skip
else reprs(n)			reprs(n) u ?ty
end
end
until S2 is unchanged
end closure
Figure 4.7: Construction of conversion of representations.
The transformation of an expression is constructed in the same way as the rep-
resentations of the expression. The only difference is that set 53, which contains the
transformation rules, is used instead. Figure 4.8 shows the algorithm for construct-
ing a transformation of an expression. max?(a, b) is the maximum of a and b with
respect to relation ?. We assume that a ? I for all a. Again, heuristics can be
employed for choosing the most appropriate transformation rule when more than one
rule can be applied to an abstract tree node.
The transformation algoritlim performs the following steps when it visits an ex-
pression node n for constructing its representations and a transformation for it.
reprs(n) := $; mk?reprs(n); closure(n); mk?trans(n)
4.9 Transformations of statements
If n is a statement node stmLop w, then
V(n)			=			(Vn			n?n:
C(n)			=			(Vn			n?n
46
mk?trans(n)
var E:environment;
trans(n)			I;
for r in S3 do
E match(pattern(r),n,?);
if E #1 cand app(r,E) then
trans(n) := max? (insl(replacement(r), E), trans(n))
end
end mk?trans
Figure 4.8: Construction of transformation of an expression.
The transformation of a statement is constructed in the same way as the trans-
formation of an expression. When the transformation algorithm visits a statement
node n, it executes the following statements.
rep?(n)			?; rnk?trans(n)
Again, special heuristics can be employed for choosing the most appropriate trans-
formation rule when more than one rule can be applied to an abstract statement
node.
4.10 Transformations of programs
Let W be the set of abstract tree nodes that are the highest nodes in the abstract
tree for which a transformation has been constructed. The transformation of the
original program is successful if
1. For every leaf that is not in a subtree of a node in W and is labeled with
a variable v, no directive in D is applicable to v,
2. For every node n that is not in a subtree of a node in W, there is no directive
default t using ?...
in V with type?of(n) =
These conditions are checked by function check that was shown in Section 4.5.
The transformed program consists of the original tree where each node in W is
replaced by its transformation. Function mk, which was presented in Section 4.5,
constructs the concrete tree.
47
4.11 Correctness
In this section we show the correctness of the transformation aigorithm. First, we
define validity of a transformation with respect to a set of transforms and transform
directives. Then we show that the algorithm constructs valid transformations of
a program with respect to the transforms and transform directives that appear in
the program.
A program P' is a valid transformation of program P with respect to a set of
transforms `r and a set of transform directives v if
1. For every directive "change v using T(w)" in D, where T is in T, all free
instances of v have been eliminated from P, as prescribed by T.
2. For every directive "default t using T(w)" in D, where T is in T, every
variable v:t for which no change directive is given is replaced using T(w) and
every expression of type t is removed from P.
We write P ?Tv P' to denote that P' is a valid transformation of P with respect to T
and V.
We show that the transformation algorithm produces a program P' such that
P #Tv P' iff such a program exists.
Let n' be a representation of an abstract expression node n or a transformation
of an abstract statement or expression node n. Define properties Pv(n, n') and
Pc(n, n') as follows.
1. Pv(n, n'): If V(n) then n' contains no instances of variables in the subtree
rooted at n that need to be transformed.
2. Pc(n, n'): If C(n) then n' contains no instances of constants in the subtree
rooted at n that need to be transformed.
Let r be a representation of an abstract expression node n and t be a transformation
of an abstract expression or statement node n. During program transformation, the
transformation algorithm maintains the following invariant for each node n.
= Pv(n, r) A Pv(n, t) A Pc(n, r) A Pc(n, t)
Lemma 1 Let n be an abstract tree node. If for every descendent m of n properties
Pv(m, m?) and Pc(m, m') hold (where m' is a transformation or a representation of
node m), then for every rule r for which E = match(pattern(r), n, ?) and app(r, E),
inst(replacement(r), E) has properties ?v and ?c
Proof: Let n be an abstract tree node for which V(n) v C(n). Assume that for
every descendent m of n properties Pv(m, m') and Pc(m, m') hold (i.e. 1m is true),
48
where m' is a transformation or a representation of node m. Let r be a transform
rule and E = match(pattern(r), n,
Since V(n) = (Vn I n E n : V(n)) and C(n) = (Vn n ? W : C(n)), it fol-
lows from the definition of app in Section 4.4 that whenever rule r such that app(r, E)
is used to construct a representation or a transformation of n, the constructed repre-
sentation or transformation does not contain any instances of variables or constants
in the subtree rooted at n. Functions apply and mk?trans construct a representation
and a transformation of a node, respectively. When transform rule r is applied using
environment E = match(pattern(r), n, ?) (i.e. when inst(replacement(r), E) is used),
condition app(r, E) holds.
Hence, for a representation r or a transformation t of n
Pv(n, r) A Pv(n, t) A Pc(n, r) A Pc(n, t)
i.e. I? is maintained during program transformation. 0
Lemma 2 Let n be a leaf of the abstract tree. I? is true.
Proof: We distinguish the following cases.
1.
Let n be a node labeled with variable v:t. If "change v using T(w)" is
in D, then V(n) = true and C(n) = false. In this case v is replaced by a new
variable v' as prescribed by T, and v' is v's T-representation. Hence Pv(n, v')A
Pc(n, v') trivially. In addition, every other conversion of representation r that
is derived from v' can not contain any instance of v, hence Pv(n, r)APv(n, r).
Similarly for a transformation t. Hence I? is true in this case.
2. Let n be a node labeled with variable v:t. If no "change v using ..?` is in D,
but "default t using ..." is in V, then V(n) = true and C(n) = false. The
proof of this case is the same as the previous one.
3.
Let n be a node labeled with variable v: t. If no transform directive is applicable
to v, then v is not replaced by another variable, and V(n) = C(n) = false.
Hence I? is trivially true.
4. Let n be a node labeled with constant c:t. If "default t using ..." is in V,
then V(n) = false and C(n) = true. In this case the representations and
transformations of n are constructed. Hence Pv(n, n') A Pc(n, n') trivially for
every representation and transformation n' of n.
5. Let n be a node labeled with constant ct. If no transform directive is applicable
to c, then V(n) = C(n) = false. Hence I? is trivially true.
49
Li
Hence for a leaf n of the abstract tree I? is true.
It follows from the previous two lemmas that I? is true at every node n of the
abstract tree. This implies that every representation and transformation that is
constructed for a node n of the abstract tree observes all transform directives in V.
In addition, the definition of a variable v on which a transform directive D in V is
applicable is replaced by a new definition according D. At the end, the algorithm
checks if the original tree has any variables that ought to be transformed and they
are not. In this case no rules could be used to transform these variables and the
expressions that contain them so the algorithm returns 1. Hence part (1) of the
definition of validity is satisfied.
From the definition of app it follows that every expression, variable or constant
that is used in constructing a representation or a transformation of a program frag-
ment is not of type t where "default t using .." is in V. At the end, function check
checks if the resulting program contains any remaining expressions of type t where
"default t using ..... is in V. If not, then the transformed program is constructed
by function mk. Hence part (2) of the definition of validity is satisfied and we have
the following soundness theorem.
Theorem 4.11.1 Given a program P, a set of transforms T and a set of transform
directives V, the transformation algorithm produces a program P' such that P ?TD P?
if such a program exists.
Conversely since the algorithm applies all transform rules and constructs all pos-
sible representations for expressions, if there is a program P' such that P ?TD P' the
algorithm will construct it. Hence we have the following completeness theorem.
Theorem 4.11.2 Given a program P, a set of transforms T and a set of transform
directives V, if there is a program P' such that P kTv pI then the transformation
algorithm will construct it.
4.12 Complexity analysis
Let n be the size of the abstract program P. Program P is represented internally by
an abstract tree that has size 0(n). Let also t be the number of transform rules in
all transforms in T, p be the maximum pattern size, r be the maximum replacement
size and k be the maximum number of transform parameters a transform may have.
At each internal node n of the abstract tree, the transformation algorithm com-
putes V(n) and C(n). These values are the disjunction of the corresponding values
associated with the children of node n. Computing V(n) and C(n) takes time 0(w)
where w is a constant and is the maximum number of children a node can have.
50
Constructing a representation or a transformation takes time O(pn + kr) since
both the pattern and the replacement of a rule are traversed and the matching may
require testing equality of subtrees of P.
Since there are at most t rules, the algorithm spends time O(t(pn + kr)). We
assume that predicate ? takes time proportional to the size of the abstract tree. The
time spent by ? at each node of the tree is thus O(tn).
Hence, at each node of the tree the algorithm spends O(tn + t(pn + kr) + w)
time, which is O(t(pn + kr)). Therefore, the total time spent by the transformation
algorithm is O(nt(pn + kr)), which is 0(n2).
Chapter 5
Transforming expressions that
have compound types
5.1 Introduction
We consider expressions that have compound types, i.e. types of the form FU),
where F is a type constructor and t is a list of types. Any type that appears in t
can have a similar form, i.e. it can be a type constructor applied to a list of types.
Type constructor F as well the component expressions of the original expression may
be transformed. We show how to transform expressions that have such types. The
important point that should be emphasized is that no extra transform rules need
be added to the bodies of transforms that transform type constructor F and the
component expressions of the original expression.
5.2 0verview
Assume we want to transform a program variable x of type "sequence of booleans".
Assume also that we have a transform Seq for implementing sequences of any type,
and a transform Bool for implementing booleans. We want to transform x using
these two transforms. We can define x and give a directive for transforming it as
follows.
var x: seq(bool);
change x using Seq(Bool)
Assume that expression x((i? ?x((j? appears in a program, where i and j are integer
variables and ? is an operation on booleans. We want to transform this expression,
51
52
given the directive for transforming x. The transformation of the expression is accom-
plished using the rules in transforms Seq and Boot. No extra rules for transforming
expressions of the form ?((?? need be added to the body of transform Boot.
We illustrate how such expressions can be transformed. Below is part of the type
definition for sequences and the operation for selecting an element of a sequence.
type seq(t)
operations
seq?set exp-s exp-? (s:seq(t) i:int) t as s "((" i ")?"
end
This type definition defines type constructor seq. The name t of the component
type is used in the operations that are defined in the type definition. Identifier t
is a dummy name and stands for any type. Since t can be any type, operation
seq?set is pot?mo?hic. In the type definition, operation seq?set is defined to take two
expressions as operands. The first is s, which is an expression of type seq(t). The
second is i, which is an expression of type int. The type of the result of seq?set is t.
The concrete syntax for the operation is given after keyword as.
We now outline how operation x((i)) ? x((j? is transformed when x is to be
implemented by Seq(Boot). The declaration x:seq(boot) indicates that parameter t
of type seq(t) should be instantiated with boot. Operation (( ? is actually seq?set.
The type of seq?set is
and is implemented as
seq(boot) x int H boot
Seq(Boot) x _			Boot
In other words the definition of seq?set along with the directive to implement x using
Seq(Boot) can then be envisioned to mean that the instance x((i)? of seq?set is
seq?set exp-x exp-i (x:seq(boot)/Seq(Boot) i:int) boot/Boot as x "((" i "`)?"
Thus, we see that, automatically, the result of x[ij is of type boot represented by
Boot. Similarly xtj] is of type boot represented by Boot. Hence, both operands of
operator ? are represented by Boot. An appropriate transform rule of transform
Boot can be applied to transform the original expression x[i] ?
5.3 Transform and Transform Directives
A transform describes the replacement of a program variable of some type by another
variable. A transform directive specifies which transform to use to replace a particular
program variable. In Chapter 4, we give an algorithm for processing transforms
53
and transform directives when the variables to be transformed have base types. As
an example, let Int be a transform that describes the implementation of variables of
type int. A program may contain the following declaration of variable i and directive
for implementing it using transform Int.
var i:int;
change i using Int
We also want to be able to transform program variables that have ground compound
types and operations on such variables. For example, suppose we define type seq(t),
where t can be any type, and transform Seq for implementing variables of this type.
Suppose a program contains the following definition of variable s.
var s:seq(int)
The implementation of $ depends on the implementation of type constructor seq and
the implementation of expressions of type int. We would like to keep the imple-
mentation of the seq and its elements independent. For transforming s, one of the
following transform directives might be given.
change s using Seq(?)
change s using ?(i?tt)
change 8 using Seq(Int)
Change the implementation of variable s using
transform Seg. Do not use any implementation
for the elements of s.
Change the implementation of the elements of
variable s using transform Int. Do not use any
implementation for s.
Change the implementation of variable s using
transform Seq and the implementation of the
elements of s using transform Int.
The expression after keyword using in a transform directive is called a transfonn
express?on (transexp for short). Transexps are defined formally later.
5.3.1 Extensions to transforms
The above kinds of directives do force us to extend the notation we use in transforms.
We need to be able to name arbitrary transforms with transform variables, so that
transforms like Int can be communicated. To this end, we allow the types of variables
in a transform to be annotated. Consider, for example, the following transform.
54
transform Seg;
var s:seq(?t/??T) into var
s s?exp-e:?t/??T into
end
By convention, all transform variables begin with two question marks, while all type
variables begin with one.
When a variable v:seq(?nt) is directed to be implemented using directive
change v using Seq(Int)
type variable ?t in transform Seq is bound to int, transform variable ?? T is bound
to transform Int, and a new copy of Seq is generated to effect the transformation.
transform Seq';
var s:seq(?nt/Int) into var c:C(int/Jnt);
s s exp-e:int/Int into ...
end
The transexp in a change directive may contain symbol --H (as shown in some ex-
amples of the previous section). Symbol --H is synonym for I, the identity transform,
which transforms a variable to itself.
There are several possibilities for transforming the components of a variable that
has a compound type, depending on the transform variables that appear in the
declaration of the abstract variable of the transform used in the transformation.
The following examples show the effect of transform variables in Seq in transforming
a program variable.
55
transform Seq;
var v:seq(int) into ...
end
transform Seq;
var v:seq(?t) into ...
end
Transform program variables of type seq(int).
If a transform is specified for the transforma-
tion of the component expressions (of type
int) of the variable, it has no effect on the
transformation of the component expressions.
transform Seq;
var v:seq(int/??T) into
end
transform Seq;
var v:seq(?t/??T) into
end
Transform program variables of type seq(t)
(for any ground type t). If a transform is
specified for the transformation of the com-
ponent expressions (of type 1) of the variable,
it has no effect on the transformation of the
component expressions.
Transform program variables of type seq(int).
If a transform (in a transform directive) is
specified for the transformation of the com-
ponents of a variable that is transformed with
Seq, it gets bound to ?? T.
Transform program variables of type seq(t)
(for any ground type t). If a transform
(in a transform directive) is specified for the
transformation of the components of a vari-
able that is transformed with Seq, it gets
bound to ??T.
5.3.2 Notation
Consider a transform M defined as follows.
transform M;
var aM:TM into var cM:CM
end
Denote by v TM the type ill T that results from TM when all transform-variable
annotations are removed. As an example, let TM be c(c1(?t1/??T1)/??T2,?t3).
Then vTM is c(c?(?t1),?t3). We also need a notation for the transexp that de-
scribes how an abstract variable is to be implemented; we use A( TM, M) for this
purpose. A( TM, M) is constructed as follows.
Etilly annotate TM, using M for the outermost constructor and 1 for un-
annotated types. In our running example, c(c1(?t1/??T1)/??T2,?13/I)/M
is the full annotation of TM.
56
o+ In the full annotation of TM produced ill the previous step, replace each
type by its annotation and -then remove all annotations to yield the transexp
A(TM,M). In our running example this step yields M(??T2(??T1),I).
We also need a notation for annotating a type in T, given a transexp. Denote by
? t/x the annotated type that is produced when t and all its component types get
annotated by transexp ? and its corresponding components. The definition of ? t/x
is the following.
o+ If t is a base type or a type variable, then ?t/x is t/?
o+ If t is compound type C(t0,..., tn--Hi) and x is X(xo,... , xn--Hi), then ?t/x is
C( ?t0/x0,..., ?tn?1/?n?i)/X. If X is --H, replace it by 1.
o+ If t is C(t0,... , tn?1)/X, then ?C(t0,... , tn?1)/X is C( ....... , ?tn?1)/X.
For example, ?c(c1(?t1),?t3)/?(??T2(??T1),I) is
C( C1(?t1/?? T1)/?? T2, ?t3/I)/I
From now on, we will freely annotate a type t or any of its components and we
will always mean ?t. In particular we will use expressions like vTM/ A (TM, M)
and ? TM interchangeably.
5.3.3
Steps in transforming expressions that have
compound types
There are two main steps involved in the transformation of expressions that have
compound types. First, we need to prepare for the transformation. For this, the
transforms that describe the transformation of variables that have compound types
need to be processed and a new set of transforms that will be used in carrying out the
transformation of the abstract program need to be generated. Second, the newly gen-
erated transforms need to be applied to the abstract program. Section 5.4 discusses
the first step. how to preprocess the transforms to prepare for the transformation.
Section 5.5 discusses how to carry out the transformation.
5.4 Preprocessing the transforms
We show how to preprocess the transforms and prepare for the transformation. In
the following we use the terminology of Chapter 2.
57
5.4.1 Processing transform directives of the form M(x)
A lot of checking must be done to make sure that a directive like
change v using Seq(Int)
is well defined and to determine the transforms to be used in replacing v. To outline
what must transpire, let us view the situation a bit more abstractly. Consider again
transform M of the previous section.
transform M;
var aM:TM into var cM:CM
end
Let v: T be a variable, where T is a ground type, and suppose directive
change v using M(w)
is given for its transformation, where x is a list of transexps. We assume that M(?x)
contains no transform variables. Then, if the following process succeeds, the directive
is valid.
1. Unify T and v TM to yield a substitution a.
2.
TM has an associated transexp A( TM, M), which describes the implementa-
tion of aM. Unify M(x) and A( TM, M) to yield a substitution ? (for transform
variables that appear in TM).
3. Let M' be a new transform that is obtained from M by applying substitutions
a and 6 to M. M' has the following form.
4.
transform M';
yar aM': TM into var cM':CM
end
Process M' to remove all annotations, yielding a transform M.
Let n = #t and let v'?:t? be a fresh variable, for 0 < ? n. Then, recursively,
process each of v'?:?t?, Xj, for 0 ? i < n, to check validity and produce a fresh
transform Nj.
Annotate program variable v with M(N0,... , Nn?i).
58
5.4.2 Processing transform directives of the form 1(x)
Let v: Tct) be a variable, where TU) is a ground type, and suppose directive
change v using (?x)
is given for its transformation, where x is a list of transexps. Each component of
type tj has to be implemented as described by Xj, 0 < i <#t. The directive is valid
if the following process succeeds.
Let n = #1 and let v'?:?t? be a fresh variable, for 0 < i < n. Process each of v'?:?t?,
%, for 0 < i < n, to check validity and produce a fresh transform Nj.
Annotate program variable v with ?(N0,... , Nn--Hi).
5.4.3 Processing transform directives of the form M.
These directives are processed as described in Chapter 4.
5.4.4
An example of preprocessing a transform for
sequences
Let seq(t) be the type of sequences that have elements of type t; t can be any type,
since seq is a polymorphic type constructor of arity 1.
Consider also transform Seq that is used to transform variables of type seq(t).
transform Seq;
var s:seq(?t/??T) into var
end
C is a type constructor. For example, Seq may implement variables of type seq(?t)
with doubly-linked lists, so C could be ptr the type constructor for pointers.
Assume we have the following definitions and directives in a program.
var s:seq(seq(bool));
change s using Seq(Seq(BN))
According to the directive for transforming s, both instances of type constructor seq
are transformed with Seq and the elements of the elements of s are transformed with
BN. Transform BN transforms variables of type bool to variables of type nat (BN
is shown in Chapter 4).
In this example, type T is seq(seq(bool)), transexp TM is seq(?t/??T), vTM is
seq(?t), and A( TM, Seq) is Seq(?? T). The algorithm performs the following steps.
59
Step 1: Unify T and v TM, yielding substitution a= `?` seq(boo1)?.
Step 2: Unify A( TM, Seq) and Seq(Seq(BN)), yielding substitution
6 = t?7T H Seq(BN)?.
Step 3: Apply substitutions a and 6 to Seq to yield transform Seq'
transform 5?q?;
var s:seq(seq(bool)/Seq(BN)) into var r:C(seq(bool)/Seq(BN))
end
Transforming Seq' to remove its annotations, yielding transform Seq
transform Seq;
var s:seq(seq( bool)/Seq(BN)) into var r: C( C(nat))
end
At this point transform ?eq has been generated, and it contains no annotations.
Step 4: Recursively process the components of the original transexp. For this,
consider a fresh variable v':seq( bool) and directive change v' using Seq(BN). We
now give the steps of the recursive call to show the new transform that is generated
as part of the recursion.
For the recursive step, type T is seq(bool), transexp TM is seq(?t/??T), vTM
is seq(?t) and A( TM, Seq) is Seq(?? T).
Step 4.1: Unify T and v TM, yielding substitution a = H booll.
Step 4.2: Unify A( TM, Seq) and Seq(Seq(BN)), yielding substitution
6 =			H BNl.
Step 4.3: Apply substitutions a and 6 to Seq, yielding a transform Seq
transform Seq11;
var s:seq(bool/BN) into var r:C(bool/BN)
end
Transform Seq" to remove its annotations, yielding a transform Seq.
transform Seq;
var s:seq(bool/BN) into var r:C(nat)
end
60
The
Step 4.4: Recursively process the components of the component transexp.
next level of recursion does not yield any new transforms (substitutions a and ? are
empty).
Program variable s gets annotated with S?q(R?q(BN)).
5.5 ?ransforming the abstract program
The transformation of the abstract program proceeds in the same way as described in
Chapter 4, by traversing the tree bottom-up and applying the rules of the transforms
that have been constructed during the processing of the transform directives.
5.5.1 Replacing variables that are transformed
Program variables for which transform directives are given get replaced as follows,
using ctyp(M) to denote the type of the concrete variable of transform M.
o+ A program variable v that is annotated with M(?N) gets replaced by a new
variable v': ctyp(M).
o+ A program variable v that is annotated with ?(N) gets replaced by a new
variable v': T(ctyp(No),..., ct?p(Nn?i)).
o+ A program variable v that is annotated with M gets replaced by a new variable
v': ctyp(M).
In the example of the previous section, program variable s of type seq(seq(bool))
is annotated with Seq(S%q(BN)). It gets replaced by a new variable s': C( C(nat)).
5.5.2 Transforming expressions
When transforming expressions that contain variables that are transformed we dis-
tinguish two cases, depending on how the variable that is transformed is annotated.
Let v be a variable that is annotated with M(N) and assume that a program
contains an operation 0 that involves v. When the directive for the transformation
of v was processed, transforms M, N were generated. Operation 0 gets replaced by
a new one according to the transform rules of M. Representations and transforma-
tions of expressions are constructed the same way as described in Chapter 4. The
only difference is that in pattern matching transexps M and M can match, where M
and M are transforms such that M was constructed from M during preprocessing.
Since types can be annotated, a pattern exp-e:t/ T matches an expression e':t that
61
has a T-representation. The replacement of a rule may contain Tje which is the
T-representation of expression e.
The other case involves transformation of operations that contain program vari-
ables and that are annotated with ?(N); we discuss this case now.
An example
Suppose type T(t1, t2) defines abstract operation
op: T(t1, t2) x ti			t2
with concrete syntax.[.]. Suppose program variable u: T(sl, s2) has been defined and
it has been annotated with ?(81, 82), where 81, 82 are the following transforms.
transform 81;			transform 82;
var a:sl into var c:sl'			var a:s2 into var c:s2'
end			end
The annotation of u indicates that the first component of u (of type si) is to be
implemented by 81 and the second component of u (of type s2) is to be implemented
by 82. The definition of u is replaced by
var u': T(sl', s2').
Now consider a concrete operation u[e:slj, which ill abstract form is
op(u, e) : T(s1, s2) x s1 H s2
This occurrence of variable u has to be eliminated; to do it, we proceed as follows.
The definition of u and the directive for its transformation indicate that t1 of type
T(t1, t2) gets bound to s1, which is implemented by 81, and t2 of the type gets bound
to s2, which is implemented by 82. Variable u: T(s1, s2) with its first component
of type s1 implemented with 81 and its second component of type s2 implemented
with 82 is annotated with (81,82) and has been replaced by u'. The representations
of expression e:s1 have been constructed from the recursion. If expression e:s1 has
an 81-representation, then the previous operation is replaced by
op(u', ?e?s?) : T(s1', s2') x s1' H s2'
which in concrete syntax is t't[e?si] (?e]si is the 81-representation of e), and is
annotated with 82.
62
Replacing operations that contain variables that are transformed
Let the type definition for TU) cdntain operation
op:TFt) xr? rO
where each element of r? and rO may include any of tj.
Let v: T(?s) be a variable that is annotated with (x). Binding a associates type Sj
and transexp Xj with tj.
a=fui O? i?#t : ?tiH?si/xi1
The declaration of v is replaced by
var v':T(ctyp(?xi),...,ctyp(xn))
where, again, ctyp( T) is the type of the concrete variable of transform T.
Let op(v, ?e) be an operation that involves variable v and expressions e:y. An-
notating the components of op with their types and the transexps that implement
them yields
op(v:T(?s)/?(x),...,eiTri?Q...)
(5.1)
The representations for each expression e? have been constructed recursively. In
the last annotated operation, each component that is annotated with /M (say) gets
replaced by its M-representation, if such a representation exists for the corresponding
component. The original operation that involves abstract variable v gets replaced by
I?en?)
where for each expression e?, 0 ? i < #?e, r?? is the appropriate representation that
is required by annotation 5.1. The original operation is annotated with the transexp
that corresponds to rO a.
5.5.3 An example of transforming the elements of
an array
Suppose the following definitions and directive appear in a program.
var x:array [100] of bool;
var
change x using (BN)
63
According to this directive, type constructor array is not transformed, but the ele-
ments of array x are transformed with BN, shown in Chapter 4.
When transform directive above is given for the transformation of variable x, x
gets annotated with ?(BN). The definition of ? is replaced by
var :array of nat.
Assume now that expression x[?] appears in a program. The type definition for
array(t) contains the type for the array-element selector [.j.
array?setector: array(?t) x int
In expression x[ij, array?setector is applied to variables x: array( boot)/?(BN), and
Hence, ?t in the type of the array-element selector is bound to boot represented
by BN.
Element x(i] has a BN-representation, as shown below.
I(x:array of boot/?(BN))?i: int]: boot/BN?
(x':array of nat)[i:int]:nat
Assume now that expression x[i] v xtj] appears in a program. Like x[i], subex-
pression x[j] has type boot and associated transexp BN. Consider the type definition
for boot the contains the type of operator V.
boot x boot H boot.
Consider also transform BN, shown in Chapter 4.
transform BN;
(0) var b:boot
f Coupting
(4)
end
II IBNibilV
into varj:nat
invariant: CI(b,j) = b = j > O?
BNjbj2?			=			BNjjjl t BNjjj2
Rule (4) of BN prescribes the representation of a boolean expression that is
formed using operator v from the representations of its subexpressions.
Pattern BNibil V BNjbj2 of rule (4) of BN matches the original expression x[i] v
x[j], since both x[i] and x[j] are annotated with BN. Rule (4) of BN constructs
a BN-representation; hence it can be applied to x[i] v x[j] to construct its BN-
representation. The constructed representation is of type nat and its associated
transexp is BN.
Chapter 6
`rransfdrming functions,
procedures, and transforms
We show how to transform procedures and functions when they are called with argu-
ments that are transformed. We also show how to transform transforms that contain
directives for the transformation of local variables.
6.1 Transforming functions and procedures
The transformation of programs is discussed for programs that contain calls to func-
tions or procedures, in which one or more arguments are expressions that must be
transformed. An algorithm is presented for transforming such programs. The orig-
inal call is replaced by a new one where the arguments are the transformations of
the arguments of the original call. A new version of the function or procedure that
is called may need to be constructed.
6.1.1 Functions and procedures
We assume that the source language supports functions and procedures. The defini-
tion of a function is as follows.
function f(p:t): t;
expression
Each function has a name (f in this example) and a return type (t). A function may
have zero or more parameters (?p) with corresponding types (t). We write
for a function f that has parameters of types t and returns a result of type t.
64
65
A parameter can be either var or non-var (as in Pascal). For a var parameter,
ally change of its value in the body of f is reflected in an immediate change in the
corresponding argument of the function call. For a non-var parameter, any change
of its value in the body of f is local to the function and is not reflected in the
corresponding argument of the function call. A var parameter is indicated with the
keyword var in front of its name. The body of the function is any expression of type t.
The definition of a procedure is similar to the definition of a function.
procedure p(pFt);
statement
Each procedure has a name (p in this example). It may have zero or more parame-
ters (p) with corresponding types Ct). We write
void
for a procedure p that has parameters of types t. We assume that a procedure returns
a result of type void. Here, the body is any statement.
6.1.2 Examples of transforming function and procedure
calls
We give some examples to illustrate the issues involved when one or more arguments
of a procedure or a function call need to be transformed. We use transform BN,
shown in Figure 3.1, as an example of a transform.
Assume that a program contains a procedure P: boot void and a variable v.
procedure P(var p:bool);
p			p A true
var v:bool;
change v using BN
Then, variable v is to be replaced by a fresh variable Vc (say) of type nat, and the
call P(v) should be changed to P(vc) (note that procedure P has one var parameter
so any argument used for calling P must be a variable). However, the type of the
argument of the call is now incorrect. What is required is to construct a version P'
of P in which parameter Pc and the body of P' are transformed as well.
var v?:nat;
procedure P'(var p?:nat);
Pc			Pc * 1
66
Assume now that a program contains a procedure Q: bool H voidand a variable u,
as follows.
var u:bool;			procedure Q(p:bool);
p			pA true
change u using BN
Then, variable u is to be replaced by a fresh variable Uc (say) of type nat, and the
call Q(u) must be replaced by a new one. Procedure Q has one non-var parameter
of type bool so any expression of type bool can be used as an argument for calling Q.
Since transformation Uc > 0 of u can be constructed using the rules of transform
BN, the original call can be replaced by Q(uc > 0). In this case the type of the
argument of the call is correct. No new version of Q is required to be constructed.
var u?:nat; procedure Q(p:bool);
p pA true
Q(uc > 0);
Assume now that rule (8) of BN does not exist. Hence, no transformation can
be built for u. Then the call Q(u) is replaced by Q'(uc) where Q' is a new instance
of Q. Procedure Q' is defined as follows.
procedure Q'(p?:nat);
Pc			Pc* 1
Procedure Q' has one parameter Pc that is of type nat, since the argument to call
Q'(uc) is variable Uc of type nat. Parameter Pc is a BN-representation of an expres-
sion, hence the rules of transform BN can be used for transforming the body of Q
to obtain Q'.
Assume that the program contains a call Q(uAu), where variable uis transformed
as before. Let T be the following transform.
transform T;
var b:bool into varf:float
?BNjbj1 A BNjbj2? = n2J(BNjjj1) *j n2f(BNjjj2)
end
Transform T transforms a variable of type bool to a variable of type float. Function
n2f converts a value of type nat to a value of type float and *j is multiplication
of values of type float. Now the argument of call Q(u A u) has a T-representation,
namely n2f(uc) *j n2f(uc). Since transform T contains no rules for operators V
67
and :=, the previous representation can not be used for transforming the body of Q.
Finally, assume that rule (4) of transform BN is
(4') I] ?Tjbj1 V BNjbj1? = Tifil + BNijil.
To successfully transform call Q(u A u) we need both BN- and T-representation of
argument u A u. In this case the previous call is transformed to
Q"(ue * Uc, n2f(uc) *f n2f(uc))
where Q11, a new instance of Q, is defined as follows.
procedure Q11(p?:nat, q?:fioat);
Pc			?c + Pc
In the case of a function, the body, in general, is an expression that may have sev-
eral representations. Selecting one of the representations for the result of a function
depends on the context of the call of the function. For example, consider function
call F(u) where F is defined as
function F(var p:bool):bool;
and u is a variable of type boot that is transformed with BN. Function call F(u) is
transformed to F'(uc) where F' is defined as follows.
function F'(var pc:nat):bool;
(if Pc > 0 then 0 else 1) > 0
But if rule (8) of transform BN is missing, then the call is transformed to F"(uc)
where F" is defined as follows.
function F"(var Pc:nat):nat;
if Pc > 0 then 0 else 1
In this case the result of call F(u) is a BN-representation. If F(u) appears in a more
complicated expression, then further transformation may be possible. For example,
expression u A F(u) can be further transformed using rule (5) of transform BN. Its
BN-representation is Uc * F"(uc) and its transformation is Uc * F"(uc) > 0.
6.1.3 Transforming Functions and Procedures
Assume that procedure p has been defined as follows.
procedure p(p7t);
statement
68
For call p(e), the transformation algoritlim creates a new instance
procedure p-x1-...
statement'
ofp where x1, ..., X? are strings, p' are names, and ?t' are types that are generated as
explained below. The body of the new procedure is the transformation of the body of
the original one. The algorithm then replaces the original call with p?1-...
where e' are arguments that are generated as explained below.
1. Suppose p?:t? is a var parameter. Then e? has to be a variable of type tj. There
are two possibilities.
o+ No transform directive is applicable to e?. Then e'? is e?, p'? is p?, and Xj
is I, the identity transformation.
Expression e? is transformed with T, which transforms v:t? to u:t. Then e'?
is (e?)?, where (ei)? is the concrete variable that is generated when trans-
form T is applied to e?, p'? is a var parameter of type t, and Xj is T.
2. Suppose p? is a non-var parameter. There are three possibilities.
o+ Expression e? need be transformed. Then e'?is e?, Pt' is p?, t'j is ti, and Xj
is I,
Expression e? must be transformed, and has a transformation trans(ei).
Then e'? is trans(e?), p'? is p?, t?j is tj, and Xj is I.
Expression e? must be transformed and does not have any transformation
but it has representations (e?)i, ..., (ei)? according to transforms T1,
Tk, respectively. Then the basic transformation algorithm is applied to
the body b of procedure p. If the transformation of b is successful, then
it finds which representations of p? were needed for the transformation
of b. Let (Ci)h1, .., (ei)hr be the representations according to transforms
Th1, ..., Thr? respectively, that were needed for the transformation of b.
Assume that Th1 transforms vh1 : th1 to uh1 : t'h1,..., Thr transforms Vhr : thr
to Uhr:??r Then e'? is [(ei)?1,. . ,(ei)hr]? p'? is [(P'i)h1, ,(P'i)hr]? t'j?5
[t'h1?????t'hr] and Xj is Th1?? Thr
Then, the statement of p is processed like any other program part. If there are
directives for the transformation of any variables that are defined locally in statement
then statement (body of of p) is transformed. The transformed statement is the body
of the newly generated procedure.
Assume that function f has parameters p with corresponding types t and that it
returns a result of type t. The same steps as before are executed for transforming
69
a call to f. The transformation algorithm constructs the representations and transfor-
mation of the result expression. The decision of which representation to use is made
when the transformation of the program that contains the call to f is constructed.
6.1.4 Some theoretical results
When a function or a procedure call appears in a program such that one or more of
the arguments has several representations, a new version of the function or procedure
needs to be constructed. If more than one representation is required for transforming
the function or procedure call, then the algorithm of the previous section uses all
representations that are necessary for transforming the call. An implementation may
choose one only representation for each argument of the call for transforming the body
of the function or procedure. In the case of a function call, the result may have several
representations and an implementation may chose only one for transforming the rest
of the program. Selecting an appropriate representation to use for each argument of
a function call and an appropriate representation for the result of the call is a hard
task. The following theorem characterizes the complexity of the problem.
Theorem 6.1.1 The following problem P is NP-complete [GJ79j
Instance: A set of transforms T = ??.,..., Tk?11, a function f: t t, a list of
expressions e, each having a T-representation, for T in f, and a transform T in T
Question: Does the call f(e) have a T-representation?
Proof: We show that the special case of P in which `r= ? T0, T1? and T = T1
is NP-complete. It follows that the more general case is also NP-complete.
P is trivially in NP. A machine chooses nondeterministically a T0 or a T1-
representation for each argument e?, 0 < i < n and transforms f. If a T1 rep-
resentation can be constructed for the call J then the machine accepts its input,
otherwise it rejects its input.
P is hard for NP. We reduce 3-SAT to P. Let B = (A i 0 ? i < n (l?1 v l?2 v
be a boolean formula which contains literals l?, for 0 < j < m and each literal l?
is either p? or ?p? We construct a set of transforms T = ? T0, T1), a function f
and a list of expressions e such that B is true iff f(?e) has a T1-representation.
70
transform T0;
var a:bool
II Itrue?
II I?Tiiai1?
end
transform Ti;
var a:bool
II ?true?
II I?Toiai1?
II ITiiai1ATiiai2?
II IToiai1vToiai2vTiiai3?
II ITojail v T11aj2 v T0jaj3?
II [Toiai1\ITiiai2vTiiai3?
II ITiiaji v Toiai2 V T0jaj3?
II ITijail v T0jaj2 v Tijaj3?
II ?T1jaj1 v T1jaj2 V T0jaj3?
II ITijail vT1?a?2vT1?a?3?
end
into var b:nat
= 0
= fT1?Th(T1ibi1)
into
var b:nat
fT0?T1(Toibji)
fA(Tljbjl,T1jbj2)
fvi(Tojbjl,T0jbj2,Tijbj3)
fv2(Tojbjl,Tijbj2,T0jbj3)
fv3(Tojbjl,T1jbj2,Tijbj3)
fv4(Tijbjl,T0jbj2,T0jbj3)
fv5(Tijbjl,T0jbj2,Tijbi3)
fv6(Tijbjl,Tijbj2,Tojbj3)
fv7(Tijbjl,T1jbj2,Tijaj3)
Eunction f has n parameters, Pj for 0 < j < n. The body of f is B.
Let each e?, 0 < i ? n, be true. Hence, each e? has a T0 and a T1-representation
and exactly one has to be chosen for transforming the call f(?e).
Each parameter of f can be thought of as a boolean variable, such that its T0-
representation corresponds to false and its T1-representation corresponds to true. It
is easy to show that 23 is true iff f(?e) has a T1-representation.
In practice, the number of parameters of a function or procedure is typically
small, so deciding which representation to choose for an argument is not prohibitively
expensive, in case only one representation must be chosen for each argument.
6.2 Transforming variables in a transform
The transformation of variables that appear in the body of a transform is discussed.
When directives for the transformation of such variables are given, the transform is
expanded and a new transform is constructed automatically. An algorithm is pre-
sented for deciding if a set of transforms that contain directives for the transformation
of variables that appear in their body does not lead to infinite expansion.
6.2.1 Directives for transforming variables of a transform
The declaration of a transform has the following form.
71
transform T(p:t);
var av:?at into var cv: ct
?coupling invariantJ
transform rules
end
The various components of a transform are discussed in detail in Chapter 3. Here we
extend a transform by allowing directives of the form
change c using T'(?w)
in the body of T, where c is a concrete variable of T or a variable that appears in
a rule-replacement and T' is a transform. Such a directive has the following effect.
1.
2.
If c is a concrete variable, then its definition is replaced by a new one Cc (say),
as prescribed by T'. In addition, the replacements of all transform rules that
contain c are replaced by new ones in which c is eliminated,
If c is a variable that is declared in a transform-rule replacement (for example
a block-expression or a block-statement that is part of a transform-rule re-
placement), then its declaration is replaced by a new one Cc (say) as prescribed
by T'. In addition, all instances of c in the transform-rule replacement are
eliminated.
The transformation of a variable that appears in the body of a transform and for
which a directive like the one above is given is accomplished based on transform rules
in T'.
An example
Transform Complex, shown in Figure 6.1, transforms variables of type complex to
tuples of real numbers. Transform Complex contains a directive
change t using Rtuple
for transforming its concrete variable t with transform Rtuple.
Consider now transform Riuple, shown in Figure 6.2. Rtupte transforms a variable
of type rtuple (a tuple of real numbers) to records with two fields of real numbers.
Assume now that directive
change v using Complex
is given in a program. This is equivalent to directive
change v using Complex?Rtuple
72
transform Complex;
var c:complex into var t:rtuple
fCoupl?ng invariant: c = fst(t) + i snd(t)1
?c1 + c2?			=			(fst(t1) + fst(t2), snd(t1) + snd(t2))
[ci * c2?			=			(fst(ti) *fst(t2) --H snd(ti) * snd(t2),
fst(ti) * snd(t2) + snd(ti) * fst(t2))
fst(t)
snd(t)
II Re(c)			into
II Im(c)			into
change t using Rtuple
end
Figure 6.1: Complex implements a variable of type complex with a tuple of real
numbers.
transform Rtuple;
var t:rtuple			into var r:record f, s:real end
?Coupling invariant: fst(t) = r.f A snd(t) = r.s)
II [(exp-ei:real,exp-e?:real)?			=			= el, S =
II fst(t)			into			r.f
II snd(t)			into			r.s
end
Figure 6.2: Rtuple implements a variables of type rtuple with a record.
where transform CompThx?Rtuple is constructed automatically by the transformation
algorithm. Complex?Rtuple is shown in Figure 6.3.
Transform Complex?Rtuple is constructed automatically from Complex when its
rule-replacements are transformed with rules of transform Rtuple. Complex?Rtuple
is used to transform variables of type complex into records that contain two fields of
type real.
73
transform Complex?Rtuple;
var c:complex into var idr:record f, s:real end
?Coupling invariant: c = r.f + i r.s1
Ici +c??			=			=			r1.f+r2.f,s= ri.s+r?.s]
?c1 * c2?			=			=			ri.f * r2.f --H ri.s * r2.s,
s =			r1.f * r2.s + r1.s * r2.f]
into			r.f
into			r.s
II Re(c)
II Im(c)
end
Figure 6.3: Complex?Rtuple implements a variable of type complex with a record.
6.2.2 transform directives for variables in
Processing
transforms
Assume Ti and T2 are transforms like the ones below, where a directive is given in
the body of each one for transforming its concrete variable.
transform Ti;			transform T2;
var vl:tl into var v2:t2			var vl:t2 into var v2:tl
change v2 using T2			change v2 using Ti
end			end
When a directive is given for transforming a variable c that appears in the body
of a transform, a new transform is generated, in which c is replaced according to
the directive. In the example of Ti and T2 above, the expansion procedure never
terminates. Concrete variable v2 of Ti is replaced by a new variable v2' according
to T2, which is replaced by a new variable v2" according to Ti, and so on.
In this section, we give an algorithm that decides if a set of transforms that contain
transform directives for variables that appear in their bodies results in an infinite
expansion.
When directive
change c using T'(w)
appears in the body of T, where c is a variable that appears in T (where T' is a pos-
sibly different transform), the basic transformation algorithm described in Chapter 3
is used to replace c and the replacements of the transform rules. Such directive has
the following effect.
74
1.
2.
If c is a concrete variable, then its definition is replaced by a new one Cc (say),
as prescribed by T'. In addition, the replacements of all transform rules that
contain c are replaced by new ones in which c is eliminated,
If c is a variable that is declared in a transform-rule replacement (for example
a block-expression or a block-statement that is part of a transform-rule re-
placement), then its declaration is replaced by a new one Cc (say) as prescribed
by T'. In addition, all instances of c in the transform-rule replacement are
eliminated.
The definition of concrete variable c is replaced by a new one Cc (say), as pre-
scribed by T'. In addition, the replacements of all transform rules that contain c
are replaced by new ones in which c is eliminated. The transformation of replace-
ments is accomplished based on transform rules in ??
Since, by following blindly the transform directives, the transformation algorithm
may keep expanding forever, we need to know in advance if such a situation may
result.
Let T be a set of transforms that contain directives for the transformation of
their concrete variables and let D be the set of transform directives that appear in
transforms in T.
For T a set of transforms, we define directed graph G = (V, E) as follows. For
every T in T where
transform T;
var ?v:t1 into var u:t2
end
let VT be the set of variables that appear in the replacements of the transform rules
of T (possibly qualified by their scope) for which a transform directive is given.
Define GT = (VT, ET) as follows.
VT = ?vIv??4u?TJutuIu??u1
ET = ?v,T)Iv??4u?(T,u)Iu?4
Assume T transforms ?v:T1 to ?u:72 and T' transforms u:T2 to w:T3. For every
directive D in D of the form
change x using T'(w)
that appears in T, define GD = (VD, ED) as follows.
VD = ?, ED = t(w, T') x ? xJ.
75
Let G be the graph (V, E) where
V U VT, E= ? ETU U ED.
TET			TET			DED
If G has a cycle, then attempting to transform transforms in T results in an infinite
expansion. Conversely, if G has no cycle, then the expansion terminates, producing
a set of transforms whose concrete variables have been replaced according to the
corresponding directives.
The algorithm is linear in the number of transforms. Efficient algorithms exist
for testing if a directed graph contains a cycle [AHU78].
Chapter 7
A second approach to dealing
with compound types
We show a second approach to transforming expressions that have compound types,
which has its advantages and disadvantages with respect to the one of Chapter 5. The
approach is based on the notion of transform parameters, which we explain below.
We allow transforms to have parameters that are other transforms. For example,
a transform whose concrete variable is further transformed can be declared as follows.
transform M[SUB];
var a:tO into var c:tl
change c using SUB
end
Parameter SUB may appear at any place in transform M where a transform name
is expected.
A transform parameter gets bound to a transform name with a transform direc-
tive. For example, directive
change v using M[Nj
creates a new instance M' of M (M' has no parameters) in which SUB has been
replaced by N. The directive for transforming the concrete variable of M' becomes
change c using N.
A mechanism is provided for accessing the type of the abstract variable of a trans-
form (for a transform with exactly one abstract variable). Construct
domain[5UB]
76
77
is the type of the abstract variable of transform SUB. In our running example, in M',
this is the type of the abstract variable of N. Similarly,
range[SUB]
is the type of the concrete variable of transform SUB (defined only if SUB has exactly
one concrete variable).
The main use of having transforms as parameters to other transforms is to allow
for the transformation of expressions that have compound types, where the type con-
structor and the component expressions are transformed independently. For example,
the following transform may be used for transforming sequences.
transform Seq[SUB];
var s:seq(domain[SUB]) into var c:C(range[SUB])
?s?exp-e:domain[SUB]? =			SUBje
end
SUBje is the SUB-representation of expression e. Suppose s:seq(int) is transformed
using
change s using Seq(Int)			(7.1)
where transform Int is defined as follows.
transform Int;
var i:?nt into var 5:b?Lvector
end
Then, a parameterless version Seq' of Seq is created, in which SUB has been replaced
with Int.
transform Seq';
var s:seq(int) into var c:C(bit?vector)
s ? exp-e:int ? = ... Intje
end
In the approach taken in Chapter 5, transform Seq would be defined as follows.
78
transform Seq;
var s:seq(?t/??T) into var
I s ? exp-e:?t/??T = o+. ??Tje
end
When directive 7.1 is given, a new version of Seq is created as follows.
transform Seq;
var s:seq(int/Int) into var c:C(biLvector)
I s ? exp-e:in?Int ? = o+. Intje
end
This version of Seq' is essentially the same as the one shown above.
The approaches of this chapter and of Chapter 5 differ on the amount of control
given to the user of the transform. The approach of this chapter allows, and som&
times requires, the user of a transform to know how the arguments are used in the
body of the transform. For example, if the transform that is passed as argument
is used for transforming the concrete variable of another transform, the user has to
know the type of the concrete variable of the transform.
In the approach taken in Chapter 5, this knowledge is confined within the body
of the transform. Only the author of the transform can d?irect the implementation of
the concrete variables of the transform. The user need only know what operations
the transform implements. To illustrate the point, consider transform RevSeq.
transform RevSeq[SUBl, SUB2];
var s:seq(domain[SUBl])
? Coupling invariant:
I(s,r) = = #rA (V i
II I((??
II I ((exp-e:domain[SUB1j? ?
ll#s>O
II I s((exp-e:int? ?
? Isil cat sj2?
II [s ? e:domain[SUB1]?
III e:domain[SUBl] ? s
change r using SUB2
end
into var r:seq(range[SUBlj)
I 0 < i < #s : s((i')? = r((#r --H i --H
into (()`)
into ((SUB2je')?
into #r>O
= r((#r--He--H1?
= rj2 cat rjl
= SUBije ? r
= r?SUB1je
The specification for RevSeq is the following.
79
1. RevSeq implements a variable of type seq( t) with its reversed version.
2. RevSeq has two parameters, SUBi and SUB2. SUBi is used to transform the
elements of the sequence, and SUB2 is used to transform its concrete variable.
3. RevSeq provides implementations for the following operations.
o+			The empty sequence ((?.
o+			A singleton sequence ((e)'), where expression e is of type t.
o+			Testing if a sequence is non-empty (#s > 0).
o+			Selecting an element of a sequence (s((e)?).
o+			Catenating two sequences (si cat s2).
o+			Prepending an element to a sequence (e ?
o+			Appending an element to a sequence (s ?
This specification reveals more about transform RevSeq than it should. In par-
ticular, the user need not know what the concrete variable of RevSeq is, and how is
to be implemented. This is to be decided by the author of the transform who knows
the operations on the concrete variable that appear on rule-replacements.
Using transform-parameters can lead to certain abuses of a transform. For exam-
ple, the rule for prepending an element to a sequence might have been the following.
I e:domain[SUB2] ? = r ? SUB2?e
This rule can be used only when the elements of a sequence are transformed with
SUB2, the same transform that is used for transforming the concrete variable of
RevSeq. Even though this rule is a bit contrived, it is used to illustrate another point
about this approach: allowing transforms as arguments to other transforms can lead
to tricky implementations.
The main advantage of this approach is its simplicity of implementation. The
transform parameters allow a lot of flexibility but can easily lead to obscure trans-
forms. When parameters are used only for transforming the components of the
abstract variable, the approach is the same as the one of Chapter 5.
Chapter 8
Methodology and examples
We discuss some methodological issues for writing transforms. Then, we give exam-
ples to illustrate the use of transforms in practice.
A working system based on the approach of Chapter 7 has been implemented on
the Synthesizer Generator [RT88]; the examples we give in this chapter are based on
that approach. Since complete type inference is not yet supported by the implemen-
tation, type annotations are required at places of a program where types can not be
inferred. These type annotations have the form e:t where e is an expression and t
is its type. For the same reason, transform directives require type annotations for
the types of the abstract variables they transform. These type annotations have the
form d:: t where d is a directive and t is the type of the abstract variable it is applied
to. For example
change s using Seq(Int)::seq(int)
is a directive for transforming variable s: seq(int).
The examples in this chapter, two well-known algorithms, were written in their
algorithmic form in Polya, automatically transformed into C [KR87], and compiled
and executed.
8.1 Interfering implementations
A goal of the transform approach is to allow algorithms to be written in the problem
domain, using the types of the domain, and then to have the algorithms automat-
ically transformed to use efficient implementations of variables of types. Achieving
efficiency in an implementation may require more interdependency in the implemen-
tation of operations than appears at the abstract level. We explain this as follows.
Independent implementations of operations do not interfere with each other; they
may be combined in unlimited ways in the abstract program, and there will be no
80
81
interference between their corresponding implementations.
On the other hand, operations of an abstract type may be implemented in a de-
pendent fashion. The main reason for this is to optimize the implementation. One
implication is that the transform author cannot consider the implementation of an op-
eration independently of the implementation of other operations. In such cases, spe-
cial transform rules must be written for dealing with such dependencies.
We illustrate dependency of implementations with an example of type dgraph,
which may be defined as follows.
type dgraph
for expg exp-v var-w stmt-s (9:dgraph; v:verte?; w:veflex) (w(s))
as for w adjacent to v in g do s
delete exp-9 exp-v exp-w (g:dgraph; v:vertex; w:vertex)
as delete ??(?? v ????? w ??)?? from ?
end
The two statements we consider here are for and delete. Statement
for w adjacent to v in 9 do s
executes statement s for every vertex w that is adjacent to vertex v in graph 9.
Statement
delete (v			w) from g
deletes directed edge (v, w) from graph 9.
Consider now a program that contains the following statement.
for w adjacent to v in g do
if
... delete (v H w) from g
fi
Consider also transform Graph, shown in Figure 8.1, which implements variables
of type dgraph with adjacency lists. Transform Graph implements operations for
and delete so that there is no interference between them. The drawback of this
implementation is lack of efficiency. The implementation of operation for requires
construction of a new set, and the implementation of operation delete traverses the
adjacency list from its beginning. It would be nice to be able to write a specialized
rule for implementing delete so that deletion of an edge is done "in place" in cases
like the one above, i.e. while operating on vertices that are adjacent to a vertex.
82
transform Graph;
var g:dgraph into var c:array of ptr(vnode)
for id-w:vertex adjacent to exp-v:vertew in 9 do stmt-s into
block
var w:vertex;
var S:set(vertew) := set of vertices adjacent to v in 9;
do w ? 5 H 5 od
end
delete (exp-v:verter exp-w:vertex) from g into
Traverse v's adjacency list and remove w from it
with type vnode = record v:verte, next:ptr(vnode) end
end
Figure 8.1: Graph implements variables of type dgraph.
Transform Graph', shown in Figure 8.2, implements operation for by traversing
the adjacency list of vertex v. It maintains two pointers pw, and ppw during traversal
of the adjacency list: pw points to the node of the list that contains w, and ppw points
to the previous node. Figure 8.3 depicts the situation. It is clear that operation delete
cannot be implemented as in transform Graph. Simply traversing the adjacency list
that is associated with vertex v, and removing the node that contains w would
interfere with the implementation of operation for, since it would invalidate pointer
pw. So, when delete appears in the context of a for statement, its implem???atio?
has to "coordinate" with the implementation of for.
There are various ways to solve this problem. One is to change the abstract
program (perhaps by introducing new abstract operations) so that the dependencies
of the implementations of operations no longer exist. In the previous example, one
may define a new variable s:set(vertex) and change the abstract program as follows.
5 := set of vertices adjacent to v in 9;
for w ? 5 do
if
(1 ... delete (v H w) from 9
fi
So, what was part of the implementation (transform rules) becomes part of the
83
transform Graph';
var g:dgraph into var c:array of ptr(vnode)
for id-w:vertex adjacent to exp-v:vertex in g do stmt-s into
block
var pw, ppw:ptr(vnode);
procedure Del(v', w':vertex) =
if v = v' A w =
end;
Traverse v `s adjacency list and execute statement s
end
delete (exp-u:vertex exp-v:vertex) from g into Del(u, v)
with
procedure Del(v', w':vertex) =
Default implementation of delete
end;
type vnode = record v:vertex, next:ptr(vnode) end
end
Figure 8.2: Defining a local meaning for operation delete.
ppw			pw
Figure 8.3: Implementation of graphs according to transform Graph'.
84
abstract program. Note that the program stays in abstract form, in the sense that
all implementation details are hidden.
There are a few drawbacks with this approach. First, the original algorithm is
modified to accommodate an implementation (for graphs in this case), and one of
our goals is to leave the abstract program unchanged as much as possible. Second,
efficiency of the implementation may be degraded.
Another way to solve this problem is to use already existing mechanisms for
transforming programs. Essentially, we want an implementation of operation delete
that is local to operation for. The scope rules of the language already provide
mechanisms for doing this. We can implement operation delete by a call to procedure
Del (say) and define Del within the implementation of operation for. Figure 8.2
shows a way to do this. For a statement delete (u, w) from 9 that does not appear
within a for statement, procedure Del, which is defined after with in Graph', is
called. If, on the other hand, delete appears in a for statement, procedure Del that
is defined locally in the replacement of the transform rule for for is invoked.
A third approach would be to introduce a new kind of transform rule that is
powerful enough to describe special-case implementations of operations. For example,
we may invent a new kind of transform rule that has one or more local transform
rules as follows.
for w adjacent to v in 9 do s into ...
local
delete (v w) from 9 into ...
end
The semantics is as follows. Whenever operation delete (v w) from g appears
in the body of for w adjacent to v in 9 do s, the local rule will be used for
its implementation. Transform rules that contain local rules may be implemented by
appropriately generating local procedures and calls to them. Since statement local is
not implemented in Polya, in our examples we use the alternative method of defining
local procedures.
8.2
Example:
Algorithm
The Huffman Encoding
We show how to implement the algorithm for constructing Huffman codes [Huf5lj
using transforms. Given non-negative weights w, the Huffman encoding algorithm
constructs a binary tree with #w leaves, such that there is a one-to-one correspon-
dence between its leaves and weights Wj, 0 < i < #w, and 1. w is minimum over all
85
binary trees, where l? is the depth of the leaf labeled ii (a. b is the dot product of
vectors a and b).
8.2.1 The algoritlim
Figure 8.4, a screen dump of Polya's program editor, contains the conventional al-
gorithm for constructing Huffman codes. The details of the Huffman encoding algo-
rithm can be found in [Huf51,AHU85]. Here we focus on how we can implement the
algorithm in Po1?a using transforms.
The code in Figure 8.4 makes use of abstract types set and btree ("binary trees
of values of some type"). These abstract data types are defined with Polya's type
definition editor and are discussed in Section 8.2.2. Procedure rea&set reads integer
values (the weights of the algorithm) from the input (we use C input functions for
reading numbers) and constructs a set of binary trees of integers. Each element of
the set that is being constructed is a binary tree with exactly one node that contains
a weight. Procedure pmnt?btree prints a binary tree of integers.
Variable S:set(btree(int)) of the main program is initialized with the weights
that are read from the input (by calling procedure rea&set) for which lluffman codes
will be computed. Initially, each element of S is a binary tree with no children.
The Huffman code for the input weights is given by the single tree in S when the
aigorithm terminates. The algorithm also uses two variables x, ?:btree(int).
The key here is that the algorithm is written at a high level, in terms of trees and
sets of trees. Implementation details for these types are not part of the algorithm.
8.2.2 Abstract types used in the algorithm
We briefly describe the abstract types for sets, sequences, and binary trees that are
used in the Huffman encoding algorithm of Figure 8.4. Sequences are actually used for
implementing sets, and their use will be shown later when we discuss the transforms
that are used for transforming the algorithm. The types discussed in this section are
defined with Po1?a's type definition editor. Here, we have placed operations on these
types that are generally useful. After some time and use, these would be fleshed out
to types that most people would use, over and over again.
Figure 8.5 contains a screen dump of polymorphic type set(t): the type of sets
having elements of type t, where t can be any type. Most of the operations that are
defined for type set(t) are the "usual" ones. We briefly describe these operations.
o+ Expression ?eo,.... ?n--H1? constructs a set from its elements e0...., ?n--H1.
o+ Expressions compri, and compr2 are two forms of set comprehension.
86
- 0o+ 0
(?--program ?itor?)
procedure read_aet(var ab: aet(btree(int)))
do eof(input) -->
var e: int
read(e)
:--H ab?(<:tni1,e,tni1:>)
od
end
procedure print_btree(t: btree(int), margin: int) -
if t#tnil --H--H>
block
var i: int :--H 0
do i<rnargin --> print)			I := 1+1 od
print(.t: int)
print("\n")
print?btree(?t rnargin+S)
print?btree(?t, margin+5)
end
I t-tnil --> skip
fi
end
var s: aet(btreeCint))
read?aet(S)
do 4s?1 -->
var x: btree(int)
var y: btree(int)
x :-
S :--H s--H(st?)
y :-
S :--H
od
print_btree(s??, 0)
o+ODIRECTIVES00
change 5 into a using 5et?Seq[I]::aet(btree(int)),
seq?Dii[BtreeTrec[I]::btree(int)]::seq(btree(Int))
change x, y using stree?Trec[I1::btree(int)
naim display function :C
Figure 8.4: Huffman encoding algorithm witli directives.
87
o+ Expressions si U s2, si A s2, and s1--s2 are the set union, set intersection, and
set difference, respectively, of sets si and s2.
o+ Expression eE?s (e??s) is true iff e belongs (does not belong) to set 5.
o+ Expression si c s2 (si ? s2) is true iff si is a proper subset (superset) of s2.
o+ Expression si C s2 (si ? s2) is true iff si is a subset (superset) of s2.
o+ Expression s ?? (s II) is a minimal (maximal) element of set s according to
an ordering relation for its elements.
o+ Expression ##s is the size of set 5.
o+ Statement forail ? ?? 5 do b performs statement b on each element i of set 5.
o+ Function choose(s) returns an arbitrary element of set 5.
type set(t)
operations
set_make ([exp-e]) (e: t) set(t) as o+(" ([a)-,) o+)`;
union (s: set(t); t: set(t)) set(t) infix ?
intersection (s: set(t); t: set(t)) set(t) infix n";
minus (s: set(t); t: set(t)) set(t) infix
compri id--Hx exp--He (x: t; e: bool; (x) e) set(t)
as ?(			x			e `I;
compr2 [id-x type-ti] exp-r exp-e
(x: ti; r= bool; e= t; (x) r; (x) e) set(t)
as t			[x			a' ti]--H",			r			e
minimum (s: set(t)) t poetfix o+`t?";
mezimum (s: set(t)) t postfix "tI";
suoset (s: set(t); t: set(t)) bool infix o+`?";
superset (s: set(t); t: set(t)) bool infix o+`?`;
subsetp (s: set(t); t: set(t)) bool infix c
supersetp (s: set(t), t: set(t)) bool infix "?";
member (e: t; s: set(t)) bool infix "e";
not_member (e: t; s: set(t)) bool infix "?";
forall id--Hi exp--Hs stit--Hb (i: t; 5: set(t); (i) b)
as ?ora11' 1 a" 5 "do" b "end"
size (s: set(t)) int prefix "0";
oboose (s: set(t)) t
end
Figure 8.5: Definition of type set(t).
Figure 8.6 contains a screen dump of type seq( t). Type seq( t) is also polymorphic,
it is the type of sequences having elements of some type t; t can be any type. We
briefly describe the operations that are defined in type seq(t).
88
o+ Expression ((eo,... , en--Hi)) constructs a sequence from its elements e0...., ?n?1.
o+ Expression s ? e ? s) appends (prepends) e to sequence s.
o+ Expression si cat s2 catenates two sequences si and s2.
o+ Expression s((i? yields element i of sequence 5.
o+ Expressions s((?..?, s((.4)), s((i.4)) yield a subsequence of sequence 5.
o+ Expression e E 5 is true iff e is an element of sequence 5.
o+ Expression #s is the size of sequence 5.
o+ Expression H5 is the reverse sequence of s.
o+ Statement for e inseq s do st performs statement st on each element e of
sequence 5.
o+ .			.			.			o+o+			0
type seq(t)
operations
seq?make ([exp--He]) (e: t) seq(t) as o+ ([e]--H,") o+`;
sppend (s: seo(t); e: t) seq(t) infix `?";
prepend (e: t, 5: seo(t)) seq(t) infix o+`<";
cat (e: seo(t); 5: seo(t)) sea(t) infix "cst?;
index exp--Hs exp--Hi (s: seq(t), i: int) t as s " I 
initis1?seoment exp--Hs exp--Hi (s: seq(t), i: int) seq(t)
as 5 ??` 1 . .
midd1e?segment exp-s exp-i exp-3
(s: sea(t); i: int; j: int) seo(t) as 5 `<c i . . i "?;
fins1?segment exp--Hs exp--Hi (5: seo(t); i: int) sen(t)
as 5 "<(` . . 1 )>?;
member (e: t; 5: seq(t)) bool infix `e";
not_member (e: t; 5: seq(t)) bool infix o+`?`;
size (s: seq(t)) int prefix 4';
reverse (5: seq(t)) seq(t) prefix "<4";
for id--He exp--Hs stat-st (e: t; 5: seo(t))
as "for" e inseq" s "do" St
end
Figure 8.6: Definition of type seq(t).
Figure 8.7 contains a screen dump of polymorphic type btree(t): the type of
binary trees having elements of some type t. The type definition defines literal Inil,
which denotes the empty binary tree. We briefly describe the operations that are
defined in btree(t).
89
o+ Expression (:tl, e, t2:? constructs a binary tree that has ti as its left subtree,
t2 as its right subtree and e as the value of its root.
o+ Expression ?t returns the value stored at the root of tree t.
o+ Expression t (? t) returns the left (right) subtree of t.
o+			o+o+			0
type btree(t)
literals
btree_nil as `?tnil'
operations
mktree exp-e exo-ti exp-t2
(e: t; ti: btree(t); t2: btree(t)) btree(t)
as `<:` ti e t2 =>";
node?va1 (e: btree(t)) t prefix
isub (e: btree(t)) btree(t) prefix
Figure 8.7: Definition of type btree(t).
Figure 8.8 contains a screen dump of polymorphic type ptr(t): the type of pointers
to values of type t. Type ptr(t) is used for implementing sequences and binary
trees. The type definition defines literal nil, which denotes the empty pointer. The
operations that are defined in ptr( t) are the following.
o+ Expression ?e returns a pointer to expression e.
o+ Expression p dereferences p and returns the value pointed to by it.
o+ Expression dispose p disposes the value that is pointed to by p. This operation
is included because we transform a program to produce C code.
8.2.3 Transforming the algorithm
We want to transform the algorithm in Figure 8.4 into one that uses appropriate
data structures for implementing variables S, ?, and ?. We do this by employing
transforms Btree?Thec, Set?Seq, and Seq?Dll. The formal coupling invariants are not
given in the transforms; instead, they are discussed informally below.
Note that there are general transforms, which could be placed in a library and
used in many situations. Thus, they become "off-the-shelf", reusable parts.
90
o+. . o+
type ptr(t)
1iterals
ptr_nil as `nil
operations
ref (e: t) ptr(t) prefix "s",
deref (p: ptr(t)) t postfix
dispose exp-p (p: ptr(t)) as "dispose"
p
Figure 8.8: Definition of type ptr(t).
Figure 8.9 contains a screen dump of transform Btree?Thec, which implements
a variable of type "binary tree" with a pointer to record trec. The definition of tree is
given after keyword with at the end of the transform. Each node of the binary tree
contains a value and two pointers. one to the left subtree and one to the right subtree.
Figure 8.10 depicts the representation of a binary tree according to Btree?I?ec.
Transform Btree Tree implements the empty binary tree (tnil) and btree expres-
sion (:tl, e, t2:), where ti and t2 are binary trees and e is a value. It also contains
rules for accessing the value at the root, and the left and right subtree of a binary tree.
Finally, it contains rules for comparing two binary trees according to the ordering of
the values at their roots, and assigning one binary tree to another.
(`Btree?Trec implements binary trees with pointers to records )
tranefori fltree?Trec[SUB2];
var b: btree(doo+ain[SUS2]) into t: ptrctrec)
coupling invarlant : (expression?
I I tnil I --H nil
I			<:bjl,exp--H d:(kaain[sUB2],bi2:> I
--H e[left - t?l; dets SUE2?IdI; right = tj2]
I			I			b I --H (t?).left
I			I			I = (t?).right
I exp			o+b			into			t?.dsts
I exp			bjl<bi2			into			t1l?.dsts<tj2'.dst5
I exp			bjl=bj2			into			tjl=ti2
I exp			bjl?bI2			into			tjlo+t12
I stat bil :--H bj2			into			til :--H tj2
with			type trec =
record left: ptr(trec);			date: rangs[SUB2]; right: ptr(trec) end
end
Figure 8.9: Transform Btree?Tree.
91
t
left Idata=di f riy?ht i
Figure 8.10: Implementation of tree (:(:tnil, d2, tnil:?, di, (:tnil, d3, tn?l:):) according
to Btree?Trec.
Transform Seq?Dll implements a variable of type "sequence of elements of some
type" with another variable of type "doubly linked list of elements of the same type
Figures 8.11--H8.13 contain screen dumps of Seq?Dll. According to Seq?Dll, a variable
of type "sequence of elements of some type" is implemented as a record (of type rec;
this type is defined after with at the end of transform Seq?Dll) that contains the size
of the sequence (which is also the length of the doubly-linked list) and two pointers to
a doubly-linked list: one to the head and one to the tail of the list. Each element of
the doubly-linked list (of type cell) contains an element of the sequence. Figure 8.14
depicts the implementation of a sequence according to Seq?Dll.
Transform 8eq?Dll implements an empty sequence, and a sequence having a single
element. It implements expressions for prepending and appending an element to
a sequence, for catenating two sequences, for accessing an element of a sequence,
for extracting a subsequence of a sequence, for membership testing, and for the size
of a sequence. Finally, it provides implementations for assigning a new value to
element i of a sequence, and for assigning one sequence to another.
Transform Set?Seq implements a variable of type set with a sequence. The se-
quence is maintained in heap order, i.e. the first element of the sequence is the smallest
element of the heap. lleaps and heap operations are studied in [AHU78]. Figures 8.15
and 8.16 contain transform Set?Seq. Set?Seq actuaily implements bags, since it does
not check for membership when adding a new element to a set. Transform Set?Seq
implements the size of a set, the empty set, and singleton sets. It also provides imple-
92
o+0			4
( Se?Dii implements sequences wah' doub? linked lists )
transfora Sea_Dll[SUBl];
var s: eeq(do-ain[SUBl]) into C: rec
coupling invariant : (expression?
I			1<0>1 --H			--H 0; hd --H nil; ti --H nil]
I			I exp--H e:doeain(sUBl]:> I			--H			Sing1e(SUEl?IeI)
I			s?exp- e:do?ain[SU?] I			-			Append(c, Suslilel)
I			I o+xp- e:do-ain(SUBl]<s I			-			Prepend(SUEiiIeI, c)
I			I siO cat eji I --H Cat(cjO, cii)
I SUBli I sexp--H i:int I --H lndex(c, i)
I sexp--H i:int.. I --H copytnd(c, i)
I ? sexp--H i:int,.exp--H ):int I --H copy(c, i, ))
I I s..exp--H i:int I --H copy(c, 0, i)
exp exp- e:d:lain[SUSi]es
into fron
var p: ptr(cell) :- c.hd
do panil cand (p').d#SUEiiIeI --> p :- (p')?r cd
yield p#nil
exp exp- e:dc0ain[SU5l]?s
into frca
var p: ptr(cell) c.hd
do ?nil cand ?p').d?UEiiIeI --> p :- (p?).r od
yield p-nil
I exp 45			into c.n
I stat sexp--H il:int, sexp--H i2:int
eexp--H i2: mt, sexp--H ii : int
into block
var j: int :- 0
var pi: ptr(cell) :- c,nd
var p2: ptr(cell)
if ii--Hi2 --H--H> skip
I il#i2 --H--H>
coust max - (il i2): int
const min --H (il i2): int
do jciin -> pi :--H (pl').r ;			:--H j+i cd
p2 :--H pi
do icinax --H--H> p2 :--H (p2').r			j :--H j+l cd
(pi'): ceii.d, (p2,): ceii.d :- (p2')?d: Range, (pi')?d: Range
ii
end
I stat sjO :- Sil			into ajO :- CopyEnd(cji, 0)
Figure 8,11: Wransfdrm Seq?D11, part 1.
93
I stat sexp- i:int :- exp- e:doeain(SU?]
into block
var 3: int := 0
var p: ptr(cell) :- c.hd
do ?<i --H--H> p :- (p?)?r ;			:--H 1+1 od
suBlilel
end
with			type cell -
record 1: ptr(cell); r: ptr(cell); d: range[SuEl] end
type Range - ranqe[SUSl]
type rec - record n: int; hd: ptr(cell); ti: ptr(cell) end
const Single =
fn (e: range[SUSl])
fron
var cp: ptr(cell) :- e[l - nil; r --H nil; d -
yield [n - 1; hd = op; ti - op]
const Index --H
fn (cc: rec, i: int)
frcn
var op: ptr(cell) :- cc?hd
var j: int := 0
do j<i --> op := (op?) .r ; j :--H j+l od
yield (op?).d: ran?(SuEl]
colist Copy =
fn (p: rec, n: int, n: int)
frca
var i: int :--H 0
var t: ptr(cell) := p?hd
var a: ptr(cell)
var b: ptr(cell)
var q: rec
do ici --> t :--H (t').r ; i :--H i+l od
q := [n --H (n--Hn+l)iO; hd --H nil; tl = nil]
a :- nil
b :--H nil
do i<n -->
b := ?[l --H a; r = nil; d =
if a#nil --H--H> (a?),r :--H b I a--Hnil --> q.hd :- b fi
a :- b
i := 1+1
t :--H
od
q.tl :- b
yield q
conat CopyEnd = fn (p: rec, 5: int) Copy(p, n, p.n-1)
Figure 8.12: Transform Seq?D11, part 2.
94
0			-			0o+			0
cojist Append
fn (p: rec, e: ranoe[SUEl))
(if p.n=O tben single(e)
else fro-
var cc: rec :--H CopyEnd(p, 0)
var cp: ptr(cell) :- cc.tl; r = nil, d
(cc?t1?).r := ap
cc.tl :- cp
cc.n := cc.n+1
yield cc): rec
conat Prepend -
fn (e: ranoe[suBl], p: rec)
(if p?n=O tilen Single(e)
else frci
var cc: rec :-- CopyEnd(P, 0)
var cp: ptr(celi) :-			nil, r			cc.hd; d =
(ccbd?).1 :- cp
cc.bd := cp
cc.n := cc?n+i
yield cc): rec
conat Cat
fn (ci: rec, c2: rec)
if cl.n-D -> Copyfnd(c2, 0)
I c2.n-O -> CopyEnd(cl, 0)
I othervise ->
froon
var ccO: rec
var ccl: rec
ccO :- CopyEnd(ci, 0)
ccl := CopyEnd(c2, 0)
cc0.n := cc0.n+ccl.n
(ccl.hd').l :--H ccO.tl
(cc0.tl?).r := ccl.hd
cc0.tl := ccl.tl
yield cc0
fi
end
Figure 8.13: Transform Seq?D11, part 3.
95
c
Figure 8.14: Implementation of sequence ((d1,... , dn? according to Seq?D11.
mentations of operations for selecting the minimum element of a set (recall that, since
the sequence is maintained in heap order the minimum element of the set is the first
element of the sequence), for removing the minimum element of a set (implemented by
removing the first element of the corresponding sequence), and for adding an element
to a set. Since the heap order must be maintained among elements of the sequence,
the sequence must be reorganized after adding or removing an element from it. This
is accomplished by procedures bubb1e?up and bubb1e?down, which are defined at the
end of transform Set?Seq. Finally, transform Set?Seq provides an implementation for
assigning one set to another.
( Set?Seq implements sets ?tn sequences )
traneforn set?seq[sUB, CONT];
var a: set(doea1n[SU?1) into a: seq(range[sUB])
coupling invar lant : (express I on)
I exp o+a			into			o+a
I stat a := a--H(ati)
into			if ta?2 ---H>
block a ata-l<al. .?a-2 bubble_do,n(a) end
I Ia=2 --H--H> a :
I o+a<2 --H--H> a :=
fi
I ( ) I =
I I (exp--H x:doeain[sUB]? I = <csu??IxI
I SU?i I sit I --H
I stat all := ai2 into all := 512
I stat a := a?(exp- x:do-ain?SU?])
into block a :- a?SUBlIxI			bubble?upCa) end
Figure 8.15: Transform Set?Seq, part 1.
96
with procedure bubble_up(ver aa: seg(range[sUB])) -
var i: int :--H o+aa--Hl
do i>O cand aai<aa(i--Hl)/2 --H--H>
aai, aa(i--Hl)/2 :--H aa(i--Hl)/2, aai
i (i--Hl)/2
od
end
procedure bubble?doan(var aa: seg(ranoe[sUB]))
var i: int := -1
vat 3: int :--H 0
var left: int
var right: int
do 3?i -->
left			2?i+i
right			2*i+2
j :--H
(if (left<taa cand aaleft<aai)
then (if (right<?aa cand aaright<aai)
then (if aa<cleft<aa<cright then left elae right)
int else left): int else (if (right<4aa cand aaright<aai)>
then right else i): int): int
aai, aaj :--H aaj, aai
od
end
44DIRECTIVES#4
chenge a into b using coNT::seq(range(SUE])
end
Figure 8.16: Tra?sform Set?Seq, part 2.
97
The concrete variable a of transform Set?Seq is of type seq, which is an abstract
type. The operations on a that are used on rule-replacements of Set?Seq were defined
in type seq( t), shown in Figure 8.6. The directive at the end of SeLSeg requests that
this variable be implemented as a doubly-linked list. This illustrates that variables
in an implementation can themselves be transformed.
The transform directives
The directives for implementing the abstract variables of the algorithm are shown in
Figure 8.4. Variable S:set(btree(int)) is implemented as follows. First, it is imple-
mented with a sequence, and then the sequence is implemented with a doubly-linked
list. The elements of the set (each of type btree(?nt)), and variables r and y are
implemented with pointers to records, using transform Btree Trec.
The transformed program
Figures 8.17 and 8.18 contain screen dumps of parts of the transformed program.
The transformed program is quite long; we do not show all of it here. Variable 5 of
the original program has been replaced by variable s of the appropriate type. The
body of the do-loop has been transformed as well. The size of 5 has been replaced
by field n of record s. The assignment to variable x has been replaced by the code
for accessing the first element of the doubly-linked list. The removal of x from set 5
(recall that x is the least element of 5) has been implemented by code that removes
the first element of the doubly linked list and a call to bubb1e?down to maintain
the heap order. Similar transformations take place for the operations on variable y.
Finally, the union of 5 with the singleton set has been replaced by code that appends
an element to the doubly-linked list and calls bubb1e?up to maintain the heap order
among elements of the sequence.
Naturally, the programmer need not look at the transformed program. But it is
interesting to see how the short algorithm of Figure 8.4 is turned into this expanded
code through the transformation process.
The transformed program is then automatically transformed into a C program
that can be compiled and run. The size of the object code that is produced by the C
compiler is approximately 7 Kbytes. As an example, when the compiled C program
runs on input 1 2 3 4, it produces the output shown in Figure 8.19.
98
(?--H--HPrcaran can be transformed?)
type _?tree_Trec__I__btree_int_trec -
record
Etree_TrecI__btree_int?left: ptr(?Etree?TrecI__btree_int_trec);
Etree_TrecI__btree_int_data: int;
Etree_Trec__I__btree_int?rigbt: ptr(?Etree?Trec			I__btree?int?trec)
end
type s?Dll?Btree_Trec__I__btree_int?a?btree int_cell -
record
sea?Dll?Etree_Trec__I__btree_int?s?btree?int_1:
ptr(?s?Dll__Etree_Trec__I__btree?int s?btree int_cell);
seq?Dll?Etree_TrecI__btree_int?sea?btree?int_r:
ptr(?s?Dll__Etree_Trec__I__btree?int?a?btree int_cell);
sea?Dll?Etree_TrecI__btree_int?seq?btree?int_d:
ptr(??tree?Trec__I__btree_int_trec)
end
type s?D1l?Btree_Trec__I btree_int?seq?btree?int?Range -
ptr(?Btree?Trec I__btree?int?trec)
type seq?Dll?Btree_Trec__I__btree_int?s?btree int_rec =
record
sea?Dll?Etree_TrecI__btree_int?sea?btree?int_n: int;
Seq?Dll?Etree_TrecI__btree_int?sea?btree?int_hd:
ptr(?S?Dll__Etree_Trec__I__btree?int?s?btree int_cell);
seq?Dll?Etree_TrecI__btree_int?seq?btree?int_ti:
ptr(?seq?Dll__Etree_Trec__I__btree?int?s?btree int_cell)
end
const s?Dll__Etree_Trec__I__btree?int?seq?btree int_single -
fn (e: ptr(?Btree_TrecI__btree_int?trec))
fra-
var cp:
ptr(?s?DllEtree_TrecI__btree?int?seg=btree int_cell)
e[?seq?Dll__Etree_Trec__I__btree_int?seq?btree_int_l - nil;
seg?Dll?stree_TrecI__btree_int?aeq?btree_int_r - nil;
seq?D1l?Etree_TrecI__btree_int?aeg?btree_int_d =
yield
[?seq?Dll?Etree_TrecI__btree_int?seq?btree int_n - 1;
sea=Dll?Btree Trec__I btree_int?aeq?btree_int_hd = CD;
Figure 8.17: Transformed program, part 1.
99
prooedLire print_btree Btree_Trec__I__btree_int_I(
Dtree_Trec__I__btree_int?t?t: ptr(??tree_Trec__I__btree_int_trec),
margin: int) =
if _Btree_Trec__I__btree_int_t_t?ni1 -->
block
var i: int := 0
do i<margin --> print)			i := i+i od
print(?Btree Trec__I btree_int t_t?._Btree_Trec I__btree_int_data
int)
print(?Nn?)
print_btree Btree_Trec			I__btree int?I((?Btree_TrecI__btree_int_t
o+_Btree_TrecI__btree_int_le
rnargin+5)
print_btree Btree_Trec I__btree			int?I((?Btree_Trec__I__btree_int_t
o+_Etree_TrecI__btree_int_ri
margin+5)
end
I _Btree_Trec__I__btree_int_t_t=nii --> skip
fi
end
var a: S?D11__Btree_Trec__I__btree?int?s?btree_int_rec
read_set_Set_Seq?I?S?DI1__Stree_Trec__I__btree?int?seq?btree_int__
do s.?Seq?D11?Btree_Trec__I__btree_int?seq?btree_int_n#1 --H->
var _Btree_TrecI__btree_int_t_x:
ptr(?Etree?Trec I__btree_int_trec)
var _Etree_Trec__I__btree?int?t?y:
ptr(?Stree?TrecI__btree?int?trec)
Etree_Trec__I__btree int_t x
Se:,?D11?Etree Trec__I__btree int?seq?btree?int?Index(s, 0)
Figure 8.18: `1ransformed program, part 2.
10
4
6
3
3
2
Figure 8.19: Output of Huffman encoding algoritlim.
100
8.3
Example:
Test Algorithn?i
The Hopcroft-Tarjan Planarity
The Hopcroft-Tarjan Planarity Algoritlim [HT74,GX88] tests whether an undirected
graph is planar and, if it is, constructs a planar embedding for it. The algorithm is
linear in the number of vertices of the graph. The algorithm is quite complex and
subtle, and a clear, precise presentation of it is difficult to achieve. Its presentation in
Polya illustrates very well the usefulness of the paradigm of presenting an algorithm
at a high level of abstraction and then directing the implementation of its variables
using transforms.
The version of the algorithm that we show how to implement is due to Gries
and Xue [GX88]. Although we give some explanations on how the algorithm works,
one should refer to [GX88J for details and a proof of correctness. We also use terms
from [GX88] without repeating the definitions here.
8.3.1 Abstract types used in the algorithm
The algorithm uses directed graphs, sets, and sequences. The type definitions for
sets and sequences were given in Section 8.2. The type definition for directed graphs
that have vertices numbered with natural numbers and no weights on the edges is
given in Figure 8.20.
Throughout this section we use the convention that a graph G is undirected iff
(u, v) E G (v, u) E G, for all vertices u, v.
The type definition of graphs, shown in Figure 8.20, contains the following oper-
ations.
1. Expression newgraph e yields a new graph whose vertices are numbered
0,..., (e --H 1), and has no edges.
2. Statement newedge (vO, vi) in g adds edge (vO, vi) to graph g.
3. Statement deledge (vO, vi) from g removes edge (vO, vi) from graph g.
4. Expression vertnum 9 is the number of vertices of graph 9.
5. Expression edgenum 9 is the number of edges of graph 9.
6. Statement deladjedges of vO from 9 removes all edges in 9 that are adjacent
to vertex vO.
7. Statement for (u, v) edge of 9 do s executes statement s for every edge (u, v)
of graph 9.
101
0			0 .
type dgraph
operations
newdgraph exp-e (e: int) dgrsph as o+newdgrapbo+ e;
newedge expg exp-vO exp-vi (g: dgraph; vO: int; vi: int)
as newedge" "(" vO "," vi ")" "in" g
deledge exp-g exp-vO exp-vi (g: dgraph; vO: int; vi: int)
as "deledge" "(" vO "," vi ")" "from" g
vertnun exp-g (g: dgraph) int as "vertnun" g;
edgenun exp-g (g: dgraph) int as `edgenun' g;
deladjedges exp-g exp-vO (g: dgrapb; vO: int)
as "deladjedges" "of" vO "from" g
ftr?edge id-u id-v exp-g stat-s (u: int; v: int; g: dgrapb)
as "for" "( u vedge" "of" g "do" s
for?edj exp-u id-v exp-g stnt-s (u: int; v: int; g: dgraph)
as "for" v "adjacent" "to" u "in" g "do" a
for?adj?o,nd exp-u id-v exp-g exp-e stat--Ha
(u: int; v: int; g: dgraph; e: bool)
as "for" v "adjacent" "to" u "in" g "cond" e "do" a
end
Figure 8.20: Definition of type dgraph.
8. Statement for v adjacent to u in g do s executes statement s for every
vertex v that is adjacent to vertex u in graph 9.
9. Statement for v adjacent to u in 9 cond e do s executes statement s for
every vertex v that is adjacent to vertex u in graph g, as long as condition e
holds.
The algorithm makes use of an abstract notion of a "distinguished" or "first"
vertex that is associated with a vertex of the graph. This notion is specific to the
algorithm and is not a general operation on graphs. Hence, it is not defined in the
type definition for dgraph. In Section 8.3.8 we discuss how we can implement such
an operation.
8.3.2 Input and output of the algorithm
The planarity test algorithm is given in Figures 8.21--H8.28. Figure 8.21 contains the
definitions of Readgraph and PrintGraph for reading and printing a graph.
The input to the algorithm is an undirected graph, which, by the convention we
have adopted, means that for each edge (u, v), (v, u) is also in the graph. Readgraph
reads a graph having the following format.
o+ Number of vertices of the graph, followed by an equal number of lines.
102
o+ Each line contains a vertex number, the number of adjacent vertices to it, and
a list of the adjacent vertices.
We use C functions for reading numbers.
PrintGraph outputs a list of lines. Each line contains a vertex number followed
by the vertices that are adjacent to it.
The representation of the graph is hidden at this point. Both procedures are
expressed in abstract terms, using the operations of type d?raph.
(?--Prcaram Editor?)
var G: dgraph
procedure Read?raph(var ??: dgraph) =
var ?: int :--H 0
var vn: int
read(vn)
:- nmrdgraph vn
do 3<(vertnwt GG) --?
var v: int
var n: int
read(v)
read(n)
var k: int			0
do k<n --> var w: int			read(w)			im-edge (v,w) in GG			k :=
od
j :--H
od
end
procedure PrintGraph(GG: dgraph) -
var u: int			0
do u<(vertn? ?G) -->
print(u)
print
?r v adjacent to u in GG do block printprint(v) end
print(
u := u+1
od
print(\n")
end
ReadGraph(G)
print('Input Graph:\nNn")
Print?raph(G)
Figure 8.21: Definitions of Readgraph and PrintGraph.
8.3.3 Constructing a directed graph
The planarity test algorithm consists of two parts. First, the undirected graph (which
is actually a directed one in which for every edge (u, v), (v, u) is also in the graph) is
103
converted to a directed one while the vertices of the original graph are renamed. This
is accomplished by procedure RenamGraph, which calls DFS for a depth-first order
traversal of the graph. For each pair (u, v), (v, u) of directed edges, DFS removes
exactly one of them; thus, constructing a directed graph. During the traversal,
a renumbering of the vertices of the original graph is computed. This is accomplished
by maintaining three arrays, L, LL, and N, as follows.
o+ During the depth-first traversal of the graph, for a vertex v, N[v] is the number
of vertices processed before v.
o+ For a vertex v, L[v] is the minimum value of N[w] for vertices w reachable
from v along span-frond paths.
o+ v, LL[v] is the second minimum value of N[w] for vertices w reach-
along span-frond paths (or v if there is no such second minimum
For a vertex
able from v
value).
After DFS traverses the graph, array N contains the map for renumbering the ver-
tices: N[vj will be the new number of vertex v in the renamed graph.
After the depth-first traversal and the construction of the corresponding directed
graph, RenamGraph renames the vertices of the graph, thus constructing a palm
graph. Procedure RenamGraph is shown in Figures 8.22 and 8.23.
8.3.4 Producing an embedding
Procedure Planarity works on the graph that is produced by RenamGraph. It is
given a cycle in the graph (whose lowest-numbered vertex is cstart), the beginning
of a spine (defined by vertices u and v), and a partition of the vertices processed
thus far (sequence b). Parameter b is a sequence of blocks, and each block is a set of
segments. Each element B of b contains two fields.
o+ B.I: the segments of B that are inside of cycle c, and
o+ B. 0: the segments of B that are outside of cycle c.
For each segment B, B.I.S (B. 0.8) is a sequence of segment-numbers for segments
that are inside (outside) of cycle c. For each segment B, B.I.A (B. O.A) is a sequence
of attachments to cycle c.
If the segment defined by u and v can be embedded in the plane with respect to
the segments in b, then x is set to true, and b is augmented with the new segment
resulting in an augmented embedding, otherwise x is set to false. The details of the
algorithm and its correctness are given in [GX88]. Procedure Planarity is shown in
Figures 8.24 and 8.25.
104
var N: array [vertntn GJ of int
procedure Rena?raph("ar GG: dgraph) -
var L: array [vertnia GG) of int
var LL: array [vertn? ?G] of int
block
var i: int :--H 0
do i<(vertnui ?) --> N[i] :- -1			i :- i+1 od
end
var n: int :- 0
procedure DFS(u: int, v: int) -
N[v] :- n
n :- n+1
L[vJ :- v
:- v
for w adjacent to v in GG do if w?uAN[w]>?O?N[v)>N[w] -->
if N[w]<LLv] --> LL[v] :- L[v] L[v] :- Niw]
I N[w]-L[v] --> skip
I N[w]>L(vl ---H> ?(v]
fi
I w-uvN[v]cN[w] --> deledge (v,w) fron GG
I N[w]=?1 -->
DFS(v, v)
if L[w]<L[v]ALtw]CLL(v] --) LL[vJ :- L[vllLL[w] L[v] :- L[v]
L[w]<L[v]AL[w]-LL[w] --> LL[v] :- L[v] L[v] L[w]
I L[w]-L(v]AL[w]<LL[w] --> LL[v] LL[v]?LL[w)
I L[w]-L[v1??[w]-LL[wJ --> skip
I L(w1>L[v] --> LL[vJ LL[v]?L[w)
fi
fi
end
oonst theta -
fn (v: int, v: int)
if N[v]>N[w] --H> 2?N[w]: int
I N(v]<?N[w]?LL[w]-v -> 2?L[w]
I N[v]?N[w]ALL[w)cw -) 2?L(w]+i
fi
type gedge - record vO: int; vi: int end
var Bucket: array [2*(vertnaoa GG)) of set(gedge)
DFs(O, 0)
Figure 8.22: Defluition of RenamGraph, part 1.
105
0			o+0			0
block
var j: int :--H 0
do ?<2?(vertn? GG) --> Bucket[j] j j+1 od
end
for (v,w) edge of GG do block
var th: int theta(v, w)
Buc)cet[th] Bucket[th]?([vO v; vi v]: gedge)
end
block
var v: tnt 0
do v<(vertnei GG) --> deladledoes of v fron OG v :- v+i od
end
block
var j: tnt :- 2*(vertneo+ GG)-i
do j;:0 -->
var e: gedge
do Bucket[?1#() -->
block e ahoose(Bucket(?]) ; I3ucket[3] ?ucket[j]-(e) end
neoedqe (N[e?v0],N[e.vi]) in ?
od
3 :--H i--Hi
od
end
end
Rena?raph(G)
prtnt(Renantng of edges:NnNn')
block
var i: tnt			0
do t<(vertnua G) -->
print(i)
prtnt( -> ")
print(N[i])
prtnt(?Nn)
i i+i
od
prtnt("\n")
end
print('Renaned Directed ?raph:Nn\n?)
prtntGraph(G:)
Figure 8.23: Defluition of RenamGraph, part 2.
106
type Bloc)cT = record A: seg(int); 5: seq(int) end
type partT - record I: BlocicT; 0: Bloc)cT end
var Side: array [(edoenwL G)-(vertn? G)+l] of bool
var N_Side: int := 0
procedure planarity(cstart: int,
u: int,
v: int,
var x: tool,
var b: seq(PartT)) =
var spi: seq(int)
var w: int
const Lace = fn (t: sec(int)) (t*<o> cand t?i>w): tool
procedure Merge =
b=2: partT.I.A :--H b-2: PartT.I.A cat b-l.I.A
b=2: partT.O.A := b?2: PartT.O.A cat b?1.o.A
b-2: PartT.I.S := b<&2: PartT.I.S cat b-l.I.S
b=2: partT.O.S :--H b-2: partT.O.S cat b-i?O.S
b :--H bO.
end
procedure Fizside(var t: seq(int), X: tool) -
do t* --H--H> sid**(t=lJ := X t := ?t--H2 od
end
procedure Deletefrom(var t: sec(int), v: int) =
do t?< cand t?l>y --H--H> t := tD. o+t--H2 od
end
procedure purge(var q: seg(int), y: int) -
var h: tool :=
do h -->
DeletefroI(q<c?l?I?A, v)
DeletefromCq=l?.O.A, v)
if q--HI.I A=Aq?l 0.A= --H--H>
FixSide(q?l.I.S, true)
Fixside(q=l.O.S, false)
q :--H qD. .
b :--H q?o>
I q=l.I.A#<cVq?l.O.A#>> --H--H> h := false
fi
od
end
spi :--H
w :- V
do w>u --> spi := spi>w v := firstv(w, G) od
Figure 8.24: Definition of P1anarit?, part 1.
107
*o+			0 .
block
var v: PartT
if w>cstart --H-> v.I.A := <cw I w=cstart --> v.I.A := <0> fi
v.O?A := <0>
v.I.S :--H N_Side
v.0 S := <0>
N_Side := N_Side+l
b :- b?v
end
do zAtb>l cand Lsce(b-2.I.A) cand tace(b?2?O.A) --> x := false
I xA0b)l cand Lace(b-2. I.A) cand Lace(b=2,O.A) --> Nerge
I xA0b>l cand Lace(b-2.I.A) cand Lace(b=2.O.A) -->
t<&2.I: BlocicT, b?2.O: SlockT
b=2.O: BlockT, b-2.I: ?lockT
?erge
od
var q: seg(PartT)
q := <0>
do xAspi#(< --H--H>
var y: int :--H api=l
spi := spiO. *api--H2
Purge(q, v)
for r adjacent to v in G cond x do if r-firstv(y, G) --> skip
I (r=firstv(y, G)) --> Planarity(w, y, r, x, q)
fi
od
Purge(q, u)
block
var t: seg(int)
t --H <0>
do xAq?s --H--H>
if q?l.I.AteAq--Hl?O.A#<o> --H--H> x false
I q=l.I.A=>>Aq=l)>.O.? --H--H>
q=l.I: ?lockT, q-l.o: ?lockT
q=i.o: Bloc)cT, q<?i.I: ?lockT
I q=ls.O.A=>> --> skip
fi
FixSide(q?1.I?S, true)
Fixside(q-l.o.S, false)
t :--H q-ls.I.A cat t
g :--H qO Iq--H2
od
t--HI.I.A := b=l.I?A cat t
end
end
Figure 8,25: Deflnftiou of P1anarnt?, part 2.
108
8.3.5 Printing an embedding
Procedure PrintEmbed, shown in Figure 8.26, prints a planar embedding of the graph,
if the graph is planar. PrintEmbed is similar to Planarity: it recursively traverses
the graph produced by RenamGraph but it does not process any partitions. It has
three parameters: a cycle c and two vertices u and v that define a spine emanating
from c. First, it constructs spines spi and spine that are defined by vertices u and v.
Spine spi does not contain any vertices of c. On the other hand, spine contains both
attachments to cycle c. In other words
spine = u spi w
where w is a vertex in c.
In the sequel, PrintEmbed indicates if spi is inside or outside cycle c. It then
constructs cycle c2: the cycle that is defined by seam(c, s) spi (where 5 is the
segment defined by the spine that is defined by vertices u and v). Following the
construction of c2, Pm?tEmbed calls itself recursively on all vertices (but the first)
that are adjacent to every vertex of spine spine. Figure 8.27 contains the definition
of procedure PrintSeq, which prints a sequence of integers.
8.3.6 The main program
The main program is shown in Figure 8.28. It initializes variable b to the empty
partition and then calls Planarity. If the graph is planar, (variable ? is set to true)
it calls PrintEmbed to print a planar embedding of it.
8.3.7 Directives
Figures 8.21--H8.28 have shown the algorithm at a very high level, for ease of under-
standing. Typically, to implement this algorithm, one would have to reprogram it in
a language like C, Pascal, or Scheme, a time consuming and error-prone method. We
can do better by using off-th&shelf transforms for implementing the variables and
the operations on them. By doing so, the algorithm is the program, it need not be
changed even if a different implementation of the variables is desired.
The directives for transforming program variables are given in Figure 8.29. We
employ transforms RevSeq for implementing a sequence by its reverse, and Seq?List
for implementing a sequence with a linked list. All sequences that are used by
the algorithm are implemented as reversed linked lists, and sets are implemented
as sequences with transform SeLSeq. We implement graph G using transform Graph.
These transforms are discussed in the next section.
109
procedure printEsoed(c: seo(int), u: int, V: int) -
var spine: seo(int)
var spi: seo(int)
var cl: seq(int)
var c2: seq(int)
var w: int
spine
spi :--H
w := v
do w>u --> spine :- spine?w spi :- spi?v w :- firstv(w, G) od
spi :--H spi?w
print("Seoment: ")
print(N?Side)
print("\n Spine: ")
Printseq(spi)
print(?\n")
if Side(N?Side] --> print(.o+ Inside of cycle: .o+)
I SideN?Side] --> print(" Outside of cycle: ")
fi
Printseo(c)
cl :- Copyseq(c)
do cl--Hl?u --H--H> cl :--H cl0. o+ o+cl--H2 od
cl := clO. o+cl--H2
c2 :--H
do cl-l#w --H--H) c2 :--H cl?l<c2 cl :--H cl0. o+cl--H2 od
if c2#<o? --H--H? c2 := w<c2 I c2":o> --> skip fi
c2 :--H c2 cat spi
print("Nn'?)
N_Side := N_Side+l
do spine?o> --H--H>
var y: int :- spine:<?l
spine :--H spine0..Ispine--H2
for r adjacent to y in G do if r-firstv(y, G) --> skip
I (r-firstv(y, G)) --> printEn?ei(c2, v, r)
fi
od
do spi#<?> --H--H> spi :--H spiO. Ispi--H2 od
do cl?o> --H--H> cl := cl0. Icl--H2 od
do c2?o> --> c2 =- c2<c0 o+1c2-2 od
end
Figure 8.26: Definition of PrnntEmbed.
110
procedure printseq(s: sea(int)) -
var first: bool true
print("<")
for e lnseq s do block
if first --H--H) print(?' `?) I first --H--H> first :--H false fi
print(e: int)
end
print(">')
end
Figure 8.27: Definition of PrintSeq.
var x: bool :- true
var p: sea(PartT)
p :--H
planarity(O, 0, firstv((), G), ?, p)
If x --H--H)
var cycle: seq(int)
cycle :--H 0
cycle :- cycle?0
print("Graph is planar.\nEznbedding:\n\n?)
N_Side :--H 0
printEnbed(cycle, 0, firstv(O, G))
I x --> printcGraph is non-plansr.\n\n?)
fi
Figure 8.28: Main program.
111
t?DIRECTIVE?St*
change RenamGraph;Bucket into Busing Arr(set?seq[I]::setCgedge);
Revseq[I]::seq(gedge); s?LIst[I]::seq(gedge)]::array of set(gedge)
change pianarity;spi into spi using Revseq[Ii::seq(int);
S?List(I] : :sea(int)
change Pianarity;t into T using Revseq[I]::seqcint);
s?List(I1 : :sea(int)
change planarity;q into 0 using ?ev?ea[I]::sea(PartT),
seq?tist[I] =seq(PartT)
change PrintEmbed;spine into SPINE using Revsea[I]::seq(iflt),
S?List[I] : :seq(int)
change PrintEmbed;spi into SPI using RevEeq[I]::seqciflt);
S?List[I] : :sea(int)
change PrintEn?ed;c1 into Cl using RevEea[IJ::seq(iflt),'
Seq?iist[I] : :seq(int)
change PrintEmbed;c2 into C2 using Revsea(I]::seq(iflt);
Seq?List[I] : :seq(int)
change p into P using Revseq[I]::seq(PartT); SeqList[I]::seq(PartT)
change cycle into CYCLE usingRevsec[IJ::Sec(iflt);
S?List[I] : :seg(int)
change A into AA using Revseq[Ii::seq(iflt); SeqListtl]::seqCint)
change 5 into 55 using Revsec[I]::sec(iflt); 5eq?List[I]::sec(int)
change G into g using Graph?AdjList
?in display function :C
Figure 8.29: Directives for trausforming abstract program variables.
112
8.3.8 The transforms used
Figures 8.30 and 8.31 show transform Seq?L?st that implements sequences as lists,
and Figure 8.32 depicts how Seq?List implements a sequence.
Transform Seq?L?st implements operations for testing if a sequence is empty, and
if a sequence has more than one elements. It has representation rules for constructing
an empty sequence, and a sequence that has only one element. It also has rules for
extracting an element of a sequence, for appending and prepending an element to
a sequence, and for catenating two sequences. The constant-time implementation of
catenation is worth noting, since sO cat s1 is destructive on its second operand (s1).
Any changes to s1 after sO cat s1 is evaluated are reflected to sO. If an element is
appended to si, it will automatically be appended to sO. If, on the other hand, the
first element of sO is removed, si will be left with a dangling pointer to it. Finally,
transform Seq?List provides two ways of copying one sequence to another. Function
CopySeq creates a fresh copy of its argument. On the other hand, operator is
implemented by assignment of pointers.
Transform RevSeq of Figure 8.33 implements a sequence with a reversed sequence.
Its coupling invariant i(s, rs) is
#s=#rsA(V? I O<?<#s : s((??=rs((#rs--Hi--H1?).
Transform Set?Seq of Figure 8.34 implements sets with sequences. It is different
from the one that is shown in Section 8.2. Its concrete variable, a sequence, is itself
transformed by a directive at the end of Set?5eq. Transform SeLSeq implements
the size of a set, and provides operations for testing if a set is empty, and choosing
an element of a set. It also provides implementations for constructing the union of
two sets, for constructing an empty set, for constructing a singleton set, for adding
an element to a set, and for assigning one set to another.
Figures 8.35--H8.36 show transform Graph?AdjL?st, which implements a graph with
an adjacency list. A graph of n vertices is implemented as an array that has n entries.
Entry v 0 ? v < n, of the array is a list of vertices that are adjacent to v. Transform
Graph?AdjList provides implementation for most operations of type dgraph, shown
in Figure 8.20.
As mentioned before, the algorithm uses an abstract notion of a "first" vertex.
A vertex of a graph can have at most one "first" vertex associated with it. The
invariant used in transform Graph is that the last vertex added to the adjacency list
of a vertex v of graph 9 is the "first" vertex associated with v. Function firstv(v, g)
is implemented so that it returns the first value on the adjacency list of vertex v in
graph g.
Finally, Figure 8.37 shows transform Arr for transforming the elements of an ar-
The implementation requires such a transform to be used. Arr implements
ray.
113
( Seq?List implements sequences as linked lists and has destrncti?e modff?ers *)
tranefori seq?Liat [SUB];
vat a: aea(doaaln[sUB]) into c: rec
coupling invariant : (express ion?
I exp			a-:o>			into			c,head-nil
I exp			a#<o>			into			c.head?nil
I exp			o+s>O			into			c.head?nil
I exp			?a>l			into			c?head#c.tail
I SUB			I sO I			--H (c,head?)?vv
I SUB			I s<c1 I			- ((c,head)?.next)??vv
I SUB I s?1 I --H (c.tail?) .vv
I I <0> I --H [head --H nil; tail --H nil]
I I exp--H e:doaain[SUB])> I
(ftc-
var ?t: ptr(cell)
:--H ?[vv --H Bushel; next --H nil]
yield [head - ?pt; tail - ?t): rec): rec
I I s?exP- e:do-ain[SUB] I
(ftc-
var pt: ptr(cell)
pt :--H a[vv --H SUBlIel; next --H nil]
if c.head-nil --> c.head :- pt
I c.head?nil --> (c.tail?).next :- pt
fi
c.tail :--H pt
yield a: rec): rec
I exp- e:doaaia[SUB]<s I
(ftc-
var pt: ptr(cell)
pt :- ?[vv - SUBjIel; next - c.head]
if c.head-nil --> c.tail :- pt I c.head?ni1 --> skip fi
c.head :- pt
yield a: rec): rec
I s?fl oat sit I
if c?O.head-nil -> c?l: rec
c?l.hesd-nil -> ajO
I aiO.head#nilAail?head?nil ->
frc- (aO.tail)?.next :--H a?l.head a?O.tail :- a?l.tail yield aID: rec
fi
Figure 8.30: ?ansform Seq?List, part 1.
114
*			0*			o+ *
Isl Is--Hi 1
(fro-
var pt: ptr(cell)
pt :- c.head
c.head := (pt?).next
if c.head=nil --> c.tail			nil I c.head*nil --> skip fi
dispose pt
yield c: rec): rec
I copysen(s) I = ccpyList(c)
I stat Sit :--H Si2 into cii :--H cj2
I stat for id- i:doeain[SUB] inseq ?s do stat- St
into blod?
var i: ran?[SUE]
procedure ForReverse(?t: ptr(cell)) =
if ?t=nil --> skip
I (?t-nil) --) ForReverse(?t next) i :- ?t?.vv stat- at
fi
end
ForReverse(c head)
end
with type rec = record head: ptr(cell); tail: ptr(cell) end
type cell - record vv: ran?[SUD]; next: ptr(cell) end
corist CopyLiSt
fn (1: rec)
fron
var ?t: ptr(cell) := l.head
var ?O: ptr(cell) := nil
var r: rec
r.head := nil
do ?t?nil -->
var 00: ptr(cell) :- ?[vv - (?t?)?vv; next - nil]
if ?O=nil --H--H> r.head := qO I poonil --> (pO?).next := gO fi
pO :--H gO
pt := (pt?).next
od
r.tail := pO
yield r: rec
end
Figure 8.31: Trausform Seq?List, part 2.
115
vv=dl			vv=dn
c
head			tail
Figure 8.32: Implementation of ((d1,...,dn')? according to Seq?List.
( Pevseqreve?essequences )
transtora Revsea[sUs, coNT1;
var 5: sea(doeain[sUs]) into rs: seq(range[sU?])
?oup1ing invariant : (expression?
I exp			s-			into rs->>
I exp			s#			into rs?
I exp			45>0			into 4rs>()
I exp			45>1			into 4rs)1
I SUBi			l sO I --H
I SUB			I s--H1 I = rsO
I SUB			I s=2 I --H rs1
I SUB			I sexp--H j:int I --H			rs4rs--Hi--Ht
I			I >> I --H
I			I exp--H e:do-ain[SUB] I			--H SUBilel
I			I sil cat sj2 I = rsi2 cat rsjl
I			? s?exp- e:doeain[SUB] I			- SUB?IeI?rs
I			? exp- e:(io?ain(SUB]<s I			- rs?SUBiIeI
I			? sO. . 45--H2 I			=			rs1 . . 4rs--H1
I			? s1 . .Is--Hi I			=			rsO trs--H2
I			? copyseg(s) I			-			copySeq(?s)
I stat sji := 5i2			into rsjl := rsj2
I stat for id- i:doo+sin[SUB] ieseq 5 do stat- St
into for i inseg ?rs do stat- St
I stat for id- i:donain[BUB] inseg ++s do stat- St
into ?r i inssq rs do stat- St
4IDIRECTIVES44
change rs into RS using CONT::seq(range[SUS])
end
Figure 8.33: `IYansform RevSeq.
116
*0			0 *
( Set?Seq implements sets using sequences )
transforn set?seq[sUB, COST];
var a: aet(doo+?in[sU5]) into a: sea(range(s1Js])
coupling invariant : (expression)
I exp o+s into Ia
I stat block
exp- v:doaOaim[SU5] :- choose(s)
a :- s-(exp- v:doo+**ain(SUfl])
end
into block
a :--H a<cO.
end
I a I??s 12 I --H a ii cat a 12
I ( ) I --H
I (exp--H x:doeain[SUS]) I --H BUB?I?I
I exp a-I) into a--H
I exp sot) into a#<o>
I stat s :- s'J?exp- x:doIain[SUB]?
into block a :- a?sUslIxI end
I stat a ii : = a 2 into a I : --H a 2
I IDIRECTIVES II
change a into b using coNT::seq(rsnge[SUB])
end
Figure 8.34: Transform Set?Seq.
117
( Graph?AdjLIst implements grephs as adjacency lists )
transfora Graph?AdjList;
var g: dgraph into c: gr
coupling invariant			(expression)
I stat g nswdgraph exp- e:int
into block
var a: array [a] of ptr(vnode)
var _i: int			D
do _i<e --> _a[?i) := nil			i := i+1 od
c.vnun := e
c?enum :- 0
c.ad3 := a
end
I exp fjrstv(exp- v:jnt, g) into ((c.adj[v])').val
I stat i-wedge (exp- v:jnt,exp- v:int) in g
into block
var ?t: ptr(vnode)
?[val = w; next = c.adj[v])
c.ad?[v]
c.enum			c.enun+i
end
I stat doledga (exp- v():int,exp- vl:jnt) front g into Del(vO, vi, c)
I exp vertn? g into c.vnun
I exp edgenin g into c.enun
I stat deladjedges of exp- vO: tnt from g
into block
var y: ptr(vncde)
var z: ptr(vnode) := c?adi[vO]
do z#nii --) v			z			2 :- (z?) .next			dispose v			c.enum			c.enuz-i od
c.adj[vO] := nil
end
I stat for (id- u:jnt,id- v:int) edge of g do stat- 5
into block
var u: int := 0
var v: int
do u<(c.vnun) -->
var 5: ptr(vnode) := c.adj[u]
do z?nil --> v :--H (z').vai			stat- a			z			(z?).next od
u			u+i
od
end
Figure 8.35: Transform Cv(iph?AdjList, part 1.
118
stat for id- v:jnt adjacent to exp- u:int in g cond exp- e:bool do stat- s
into block
var v: int
var _z: ptr(vnode) := c.sdj[u)
do eA_z#nil --> v :- ( z?).val stat- 5 2 :- (_z?).next od
end
I stat for id- v:int adjacent to exp- u:int in g do stat- s
into block
var v: int
var _y: ptr(vnode) : nil
var 2: ptr(vncde) :- c?ad)[u]
var flag: bool
do _z?nil -->
v :--H (_z?).vsl
flag :- false
procedure Del(ul: int, vi: int, cc: gr) -
if u-UlAv-vl -->
flag := true
if y--Hnil --H-> c.adjlu] :--H (?z?).next
I v#nil ---H> (v').next :--H (?z').next
fi
var r: ptr(vnode) :- 2
z :--H (_z?) next
dispose r
cc.enun :- cc.enun--Hl
I u?ulvv?vl --> skip
fi
end
stat- s
if ?flag ---H> y := 2 2 :--H (?2?).next I flag ---H> skip fi
od
end
with type vnode record val.- int; next: ptr(vnode) end
type gr - record vnum: int; enum: int; adj: array of ptr(vnode) end
procedure Del(vO: int, vl: int, cc: gr) -
var y: ptr(vnode) := nil
var 2: ptr(vnode) :- cc,sdj[vO]
do z#nil cand (2?)?val#vl --> y :- 2 2 :- (2?)?next od
var r: ptr(vnode) := 2
if y--Hnil --H--H> cc.adj[vO] := (2?),next I v?nil --H--H> (y?).next := (z?).next fi
2 :--H (2?) next
dispose r
cc.enun :--H cc.enun-l
end
end
Figure 8.36: Transform Graph?AdjList, part 2.
119
selection of an array element and assignment of one array to another one.
o+0 0 .
?- Arr transforms array elements )
tranafora Arr[SUDI;
var a: array [exp- size:int] of dcaain[SUE] into b: array [size] of range[SUB]
coupling invariant : (expression?
I SU?i I a[exp- e:int] I			-			b[e]
I stat a?1 := aj2			into bil :- bj2
end
Figure 8.37: Transform Arr.
8.3.9 Example of execution
The abstract program shown in the previous sections can be transformed according
to the directives for the implementation of its abstract variables. We do not show
the transformed program here; it is quite long. The transformed program can be
automatically transformed into a C program that can be compiled and executed.
The object code that is produced by the C compiler is approximately 24 Kbytes.
Figure 8.38 (a) shows an input graph to the algorithm. Figure 8.38 (b) shows the
palm graph that is produced after renaming its vertices. When run on the input
graph of Figure 8.38, the output that is produced is shown in Figure 8.39.
0			3			0			3
1			2			1
(a)
Figure 8.38: (a) Input graph. (b) A corresponding palm graph.
120
Input Graph:
o			321
1			320
2			310
3			210
Renaming of edges:
o -> 0
1 -> 3
2 -> 2
3 -> 1
Renamed Directed Graph:
01
12
23
30
0
Graph is planar
Embedding:
Segment:			0
Spine:			<0			1 2 3 0>
Outside of cycle: <0 0>
Segment:			1
Spine:			<3			1>
Outside of cycle: <0 1 2 3 0>
Segment:			2
Spine:			<2			0>
Inside			of			cycle: <0 1 2 3 0>
Figure 8.39: Output of the plauarity algorithm.
Bibliography
[AHU78j Alfred Aho, John E. Hopcroft, and Jeffrey D. Uliman. The Design and
Analysis of Computer Algorithms. Addison-Wesley, Reading, MA, 1978.
[AHU85] Alfred Aho, John E. Hopcroft, and Jeffrey D. Ullman. Data Structures and
Algorithms. Addison-Wesley, Reading, MA, 1985.
[ASU86] Alfred Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles,
Tools and Techniques. Addison-Wesley, Reading, MA, 1986.
[BO93j Ronald V. Book and Friedrich Otto. String-Rewriting Systems. Springer-
Verlag, New York, N.Y., 1993.
[CU89j
Wei Chen and Jan T. Udding. Towards a calculus of data refinement.
In Lecture Notes in Computer Science, No. 375: Mathematics of program
construction. 5pringer-Verlag, 1989.
[Dii76] Edsger W. Dijkstra. A Discipline of Programming. Prentice Hall, Engle-
wood Cliffs, N.J., 1976.
[DJ90j
[DM82]
N. Dershowitz and J. P. Jouannaud. Rewrite systems. In J. van Leeuwen,
editor, Handbook of Theoretical Computer Science, Volume B: Formal Mod-
els and Semantics, chapter 6, pages 243--H320. Elsevier Science Publishers,
B.V., 1990.
Luis Damas and Robin Milner. Principal type-schemes for functional pro-
grams. In 9th ACM Symposium on Principles of Programming Languages,
pages 207--H212,1982.
Michael Garey and Steven Johnson. Computers and Intractability: A Guide
to the Theory of NP-completeness. W. II. Freeman and Company, San
Fransisco, CA, 1979.
[GJ79]
121
122
[GP85J
David Gries and Jan F. Prins. A new notion of encapsulation. In Pro-
ceedings SICPLAN 1985 Symposium on Language issues in Programming
Environments, volume 20 of SICPLAN Notices, pages 131--H139, July 1985.
[Gri81] David Gries. The Science of Programming. Springer-Verlag, New York,
N.Y., 1981.
[GV9l] David Gries and Dennis Volpano. The transform--Ha new language con-
struct. Structured Programming, 11:1--H10,1991.
[GV92] David Gries and Dennis Volpano. The Definition of Polya. Technical re-
port, Department of Computer Science, Cornell University, 1992.
[GX88j David Gries and Jinyun Xue. The llopcroft-Tarjan Planarity Algorithm,
Presentations and Improvements. Technical report, Department of Com-
puter Science, Cornell University, 1988.
[HT74] John E. Hopcroft and Robert E. Tarjan. Efficient planarity testing. Journal
ofthe ACM, 21(4):549--H568, October 1974.
[11U79] John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory,
Languages and Computation. Addison-Wesley, Reading, MA, 1979.
?Huf51] D. A. Huffman. A method for the construction of minimum redundancy
codes. In Proceedings IRE Conference, volume 20, pages 1098--H1101,1951.
(Knu63] Donald E. Knuth. The Art of Programming, Vol. 1: Fundamental Algo-
rithms. Addison-Wesley, Reading, MA, 1963.
[KR87] Brian Kerninghan and Dennis Ritchie. The C programming language, sec-
ond edition. Prentice Hall, Englewood Cliffs, N.J., 1987.
tMG90] Carol Morgan and Philip ll.B. Gardiner. Data refinement by calculation.
Acta Informatica, 27:481--H503, 1990.
[Mil86] Robin Milner. The Definition of ML. Oxford Press, Oxford, England,
1986.
[Mor89j J. Morris. Laws of data refinement. Acta Informatica, 26:287--H308, 1989.
?Par90]
Helmut A. Partsch. Specification and Transformation of Programs: A For-
mal Approach to Software Development. Springer-Verlag, New York, N.Y.,
1990.
123
[Pri87] Jan F. Prins. Partial Implementations in Program Derivations. Ph.D.
dissertation, Department of Computer Science, Cornell University, 1987.
[Rob65] J. A. Robinson. A machine-oriented logic based on the resolution principle.
Journal of the ACM? 12:23--H41, 1965.
(RT88j
[Smi91]
Thomas Reps and Tim Teitelbaum. The Synthesizer Generator: A Sys-
tem for Constructing Language-based Editors. Springer-Verlag, New York,
N.Y., 1988.
Geoffrey 5. Smith. Polymorhpic type inference for languages with overload-
ing and subtyping. Ph.D. dissertation, Department of Computer Science,
Cornell University, 1991.
?Str91] Bjarne Stroustrup. The C++ Programming Language, second edition.
Addison-Wesley, Reading, MA, 1991.
