Searching for a Global Search Algorithm.
We report on a case study to assess the use of an advanced knowledge-based software design technique with programmers who have not participated in the techniques development. We use the KIDS approach to algorithm design to construct two global search algorithms that route baggage through a transportation net. Construction of the second algorithm involves extending the KIDS knowledge base. Experience with the case study leads us to integrate the approach with the spiral and prototyping models of software engineering, and to discuss ways to deal with incomplete design knowledge.
Introduction
Advanced techniques to support software construction
will only be widely accepted by practitioners if
they can be successfully used by software engineers
who were not involved in their development and did
not get on-site training by their inventors. Experience
has to be gained how knowledge-based methods can
be integrated into the practical software engineering
process.
We report on experience made with the application
of the approach to algorithm design underlying the
Kestrel Interactive Development System (KIDS) [14]
to the construction of control software for a simplified
baggage transportation system at an airport. In this
paper, we use the term "KIDS approach" to denote the
concepts that have been implemented in the system
The KIDS approach has been applied to a number
of case studies at Kestrel Institute. In par-
ticular, it has been used in the design of a transportation
scheduling algorithm with impressive performance
[15, 16]. We wished to find out if we were
able to use this method based on the available publi-
We did not use the implemented system KIDS in the case
study.
cations and produce satisfactory results with reason-able
effort. A second goal of this work has been to
study how a knowledge-based approach can be integrated
into the overall software engineering process.
As a case study we chose a non-trivial abstraction of
a practically relevant problem to make our experience
transferable to realistic applications.
In the following, we elaborate on two issues: a process
model we found useful to support application of
the KIDS approach, and the merits and shortcomings
we encountered when we explored alternative solutions
to the transportation scheduling problem.
We have integrated the spiral and prototyping models
of software engineering [2] with the KIDS approach.
We developed the first formal specification and a prototype
implementation in parallel. The prototype
served to validate the specification and to improve understanding
of the problem domain.
In the KIDS approach, global search algorithms are
constructed by specializing global search theories that
abstractly describe the shape of the search tree set up
by the algorithm. For the case study, we wished to
explore two alternative search ideas. While we found
a theory suitable for the first one in the literature,
the second one could not be realized with the documented
design knowledge. This lead us to develop a
new global search theory that needs a slightly modified
specialization procedure.
In Section 2, we introduce the baggage transportation
problem. Section 3 provides a brief review of
the global search theory and the KIDS approach. We
present its integration into a process model in Section
4. The design of two transportation schedulers is described
in Section 5. Optimizations are sketched in
Section 6, where we also discuss the resulting algo-
rithms. We summarize our experience with the approach
in Section 7.
Baggage Transportation Scheduling
We wish to develop a controller for the transportation
of baggage at an airport. Pieces of baggage
are transported from check-in counters to gates, from
gates to other gates, or from gates to baggage delivery
points. The controller must schedule the baggage
through the network in such a way that each piece
arrives at its destination in due time.
To simplify the problem, we do not consider on-line
scheduling of a continuous flow of baggage fed
into the system at the check-in counters, but schedule
all baggage checked-in at a particular point in time.
2.1 Domain Model
We model the transportation net as a directed
graph as shown in Figure 1. Check-in counters and
baggage delivery counters, gates and switches are represented
by nodes. We classify these in three kinds:
input nodes, transportation nodes and output nodes.
Check-in counters correspond to input nodes, switches
to transportation nodes and baggage delivery counters
to output nodes. Since gates serve to load and unload
airplanes, we represent them by an input and an output
node.
The edges of the graph model conveyor belts. The
capacity of a belt is the maximum amount of baggage
("total weight") it can carry at a time. Its velocity is
the time it takes to carry a piece from the start to the
node.
gate G2
gate G1 gate G3 gate G4
delivery D1 delivery D2
checkin C1 checkin C2 ceckin C3 checkin C4 checkin C5

Figure

1: Transportation network
A piece of baggage is described by its weight, source
and destination nodes, and its due time. Source and
destination are input and output nodes, respectively.
Weight and due time are positive natural numbers.
Due times are specified relative to the beginning of
the transportation process.
2.2 Problem Specification
Our task is to assign, to each piece of baggage, a
route through the network leading from its source to
its destination node in due time. To keep things sim-
ple, we require an acyclic network without depots at
Function transport plan( g : graph
where acyclic(g)-
returns
dom(q):feasible path(g; b; snd(q(b)))g))

Figure

2: Problem Specification
the transportation nodes. Thus, the only way to re-solve
scheduling conflicts that arise if capacities of conveyor
belts are exceeded is to delay baggage at source
nodes. A route therefore is a pair of a delay and a path
through the network. A plan maps pieces of baggage
to routes.
Attempting to find a plan for a particular set of
baggage makes sense only if there exists a feasible path
for each piece. This is a path p through the network
g leading from the source to the destination nodes of
a piece of baggage b.
feasible path(g; b; p) ()
is path(g; p) -
(1)
Note that we do not require a punctual schedule
to exist. We wish to find a plan in every case, punctual
and without delaying baggage at input nodes if
possible. Thus, we define a cost function based on
the criteria if all baggage is delivered in time and if
baggage is delayed at input nodes.
cost all baggage
in time no delays
1 yes no
no yes
3 no no
For example, imagine we have a suitcase b 1 at gate
and another one b 2
at C 4
in

Figure

1. Both have
weight 1. They are checked in for the same flight,
starting at gate G 2 . Let the transportation time of
each belt be one time unit and its capacity also be
one unit. As we have to avoid exceeding the capacity
of the belt leading to G 2 , a solution is to delay b 1 by
one time unit. This gives us the transportation plan:
Now we can set up the problem specification as
shown in Figure 2. For each acyclic graph g and set
of baggage bs with feasible paths through the graph,
we are interested in plans q such that all baggage is
scheduled dom(q)), the total amount of baggage
on a belt at any time does not exceed its capacity
(capacity bounded), and all assigned paths are feasi-
ble. From this set, we select a plan p with minimal
cost.
3 Design of Global Search algorithms
The basic idea of algorithm design in the KIDS approach
[12, 14] is to represent design knowledge in
design theories. Such a theory is a logical characterization
of problems that can be solved by an algorithmic
paradigm like "divide and conquer" or "global
search". Algorithm design consists of showing that a
given problem is an instance of some design theory. In
the following, we briefly summarize how global search
algorithms are developed in the KIDS approach. For
a full account, we refer the reader to [13, 14].
3.1 Design Theory
A problem specification is a quadruple
hD; R; I; Oi where D is the input domain and R is
the output range of the function f to synthesize.
The predicate I : D ! Bool describes the admissible
inputs and O describes the input/output behavior
of f . Hence, f : D ! R is a solution to P
design theory extends
a problem specification by additional functions.
It states properties of these functions sufficient to formulate
a schematic algorithm that correctly solves the
problem.
The global search theory of Figure 3 describes the
search for an optimal solution with respect to a cost
function c. The basic idea is to split search spaces containing
candidate solutions into "smaller" ones until
solutions are directly extractable.
The
R is the type of search space descriptors, -
I
defines legal descriptors. For an input x, -
r 0 and Split
describe the search tree for solutions z with O(x; z):
its root is -
r 0 (x), the initial search space; a descendent
relation on nodes is given by Split:
if - s is a (direct) subspace of - r for an input x. The
solutions obtainable by looking at a single node - r of
the search tree are described by Extract(z; - r).
By axiom GS3, Satisfies(z; -
r) describes the solutions
z contained in a search space - r that can be found with
finite effort. There must exist a finite path in the
search tree from - r to a search space -
s from which z
can be extracted. Split   is defined by
Since we wish to find a globally optimal solution,
GS2 requires that all feasible solutions are contained in
Sorts D;R; -
Operations
R
Satisfies
R \Theta -
Extract
Axioms
GSC: - is total ordering on C
Function
where I(x)
returns
Function
returns

Figure

3: Global search theory and algorithm schema
the initial search space. Axioms GS0 and GS1 ensure
that all considered search spaces are legal.
The program shown on the bottom of Figure 3 provides
a schematic algorithm consistent with the global
search theory. The function F computes an optimal
solution z for a given input x by initiating a global
search in the initial search space -
(x). The actual
search algorithm is implemented in f gs. It minimizes
over the solutions that are directly extractable from
the input search space -
r and the ones found by recursive
search in spaces - s obtained by splitting - r.
Necessary filters provide the basis to optimize the
code gained by instantiating the algorithm schema.
A necessary filter \Phi is used to prune branches of the
search tree that cannot contain solutions. It satisfies
the implication
r) (2)
3.2 Algorithm Design
How can we find a global search algorithm for a
given problem specification? We have to find a search
space description -
R and operations -
and Extract such that the global search axioms are ful-
filled. In the KIDS approach this is done by referring
to knowledge about search strategies on concrete data
structures that is formalized in a library of general
global search theories 2 . Examples are theories to enumerate
all sequences over a finite set and to enumerate
all mappings between finite sets. A global search
theory for a given problem is constructed by specializing
a theory from the library. A problem theory
specializes to a problem theory
Constructively verifying the existential quantifier in
(3) gives us a systematic way to find a global search
theory for the problem at hand. In this way, the structure
of the search tree expressed in A is adapted to B
and gives us an algorithm for B that is an instance
of the algorithm schema in Figure 3. In general this
algorithm is very inefficient, but has a high potential
for optimization which can be exploited by deriving
necessary filters, by program transformation, and by
data structure refinement.
4 A Process Model
Our presentation of the application domain theory
and problem specification in Section 2 only describes
the final result of the specification effort. To develop
the domain theory is one of the major tasks if not the
most complex and time consuming one in the KIDS
approach. Much of its complexity stems from two requirements
we demand of the domain theory: it must
not only make precise the informal - usually incomplete
and sometimes inconsistent - ideas about the
nature and context of the problem, but it must also
be formulated so as to aid and not impede the subsequent
design process.
As a consequence, it is very unlikely that a satisfying
domain theory can be built from scratch. This observation
led us to integrate the KIDS approach with
the prototyping and spiral models of software engineering
[2]. One cycle of development, as sketched in

Figure

4, has three phases. The first is concerned with
establishing or enhancing the domain theory, the second
produces code, and in the third phase code and
theory are tested and validated.
We found it useful to build the first draft of the domain
theory in parallel with a prototype. In this early
phase, shaded gray in Figure 4, the domain theory is
not rich enough to apply algorithm design knowledge
from design theories. Building a prototype enables us
to get a deeper understanding of the problem and the
We used Appendix A of [13]
code
prototype
validation / test domain theory
algorithm design
optimization
specification
validation
theory
validation
domain
application
test

Figure

4: Process model
essential properties of the application area. It helps
us to build a complete domain theory and to avoid
dead-end developments.
The way in which the domain model is expressed,
the data structures used, and the properties stated,
can have much influence on the ease with which algorithm
design can be carried out. Thus, what seems
to be one cycle of design in Figure 4, may in practice
require several rounds of refining the domain theory
until the formalized notions smoothly fit with the design
theory we wish to use.
One example from the baggage transportation case
study is the way we modeled delays in routes (cf. Section
2.2). In an early version of the domain theory,
we described them by repetitions of the input nodes
in paths, each occurrence of the input node denoting
a delay of one time unit. This forced us to introduce
predicates to characterize legal routes, and we could
not use an acyclic graph model. When we decided to
reformulate the theory and make delays explicit the
theory became much more elegant and further design
was much easier.
The process of theory refinement perpetuates as we
derive filters and optimize code. The validation and
test phases also serve us to validate the code with respect
to properties that are not captured by the design
knowledge put to our disposal in the KIDS approach.
5 Two Ways to Find Transportation
Plans
Looking at the sort of transportation plans,
nat \Theta seq(vertex))
suggests two strategies to search for solutions to our
scheduling problem.
1. Domain Extension. Start with the initially empty
map and successively extend it by assigning possibly
delayed feasible paths to baggage.
2. Image Modification. Start with the map that assigns
their source nodes and no delay to all bag-
successively modify the assigned routes by
extending paths or increasing delays.
Both strategies enumerate all feasible transportation
plans. In the KIDS approach, search strategies
are provided in a library of general global search the-
ories. Algorithm design proceeds by specializing one
of these to the problem at hand. The first condition
in (3), RB ' RA , suggests to match the output domains
of the problem specification with the ones of the
library theories to find candidates to specialize.
When we began algorithm design for the transportation
problem, our initial idea was to use the
image modification strategy, but there is no general
global search theory documented in the KIDS library
[13] that models image modification. Instead, we
found a theory that describes domain extension. This
motivated us to explore both approaches.
5.1 Domain Extension
The global search theory gs finite mappings enumerates
all maps from a finite set U to a finite set
.
F 7! gs finite mappings
R 7! map(ff; fi)
I 7! -hU; V i:jU
O 7! -hU; V
R 7! set(ff) \Theta set(ff) \Theta map(ff; fi)
I 7! -hU; V
Satisfies 7!
Extract 7!
A search space is described by a partition of U into
two sets S and T , and by a map M from S to V . M
can be completed to a map from U to V by assigning
elements of V to all elements of T . Split performs one
of these assignments: it picks arbitrary elements a and
b of T and V , respectively, and extends M by a 7! b.
We find instantiations for the type variables in
gs finite mappings by unifying its output domain
with the one of transport plan.
ff 7! baggage
route
We can specialize gs finite mappings to
transport plan if we can constructively verify
(3) for these theories, i.e. we must find expressions in
and bs for U and V to prove
dom(M):feasible path(g; b; snd(M(b)))
The predicate Map is defined by
Comparing the right hand side of this definition with
and the definition (1) of feasible paths
suggests to use the sets
U 7! bs
to specialize gs finite mappings.
The use of the upper bound md(g; bs) on delays
makes the set of routes finite, and thus ensures termination
of the algorithm. We discuss termination
further in Section 7.
Since there are feasible paths for all baggage in
bs (cf. the precondition of transport plan in Figure
2), we can assign to md(g; bs) the sum of the times
needed to traverse a feasible path for each piece of
baggage. Applying the substitution for ff, fi, U , and
V to gs finite mappings gives us a global search theory
for transport plan.
R 7! set(baggage) \Theta set(baggage) \Theta plan
I 7!-hg;
Satisfies 7!
Extract 7!
The resulting search strategy assigns complete
routes to one piece of baggage after another. Without
further optimization, Split assigns arbitrary routes to
pieces of baggage and only when a complete plan can
be extracted is tested whether the assigned routes are
feasible. An obvious way to prevent infeasible assignments
in the first place is to develop a necessary filter.
Instantiation of (2) and the fact that capacity bounded
is monotonic in domain extensions of M gives us
5.2 Image Modification
There is no global search theory documented in
[11, 13, 14] that supports searching for maps by image
modification. So we developed a new theory for this
purpose.
Abstracting from the concrete scheduling problem,
the image modification strategy can be sketched as
follows: The images of a given map (the initial sched-
ule) are increased along the various degrees of freedom
that are given by the range type of the map. A suitable
successor relation on the elements of the range
type can be used to describe the "direction" in which
to increase the images of the map. This idea is formalized
in gs parallel mappings 3 .
F 7! gs parallel mappings
D 7! map(ff; fi) \Theta set(fi \Theta fi)
R 7! map(ff; fi)
I 7!-hM;Si:
O 7!-hM;Si; N:
R 7! map(ff; fi) \Theta set(fi \Theta fi)
I
Satisfies 7! -N; hM;Si:(8x 2 dom(M):M(x) S   N(x))
Extract 7! -N;
The inputs are a map M and a successor relation
S. The search enumerates all maps with the same
domain as M and images that are extended "along"
S, i.e. they are in the reflexive and transitive closure
S   of S. The domain of M must be finite, and S must
be non-dense to ensure that GS3 holds. The relation S
is anti-reflexive to ensure progress in the search. Note
that the search spaces (of sort -
R) do not only contain
the map built so far but also the relation S. This
is necessary to describe (in Satisfies) if a solution is
contained in a search space.
5.2.1 Data Type Driven Specialization
Having captured our search idea in
gs parallel mappings, we want to specialize this
theory to the transportation planning problem. It
turns out that the corresponding instance of (3)
does not help much in systematically finding M and
S, because we cannot refer to the structure of the
3 x S y is a notation for hx; yi 2S.
range type fi in gs parallel mappings. Still, it is not
desirable to develop a global search theory for the
specific structure of the range type of the transport
schedules because the newly developed theory should
be sufficiently abstract so as to be applicable to a
broad range of problems. To solve this dilemma, we
propose to specialize gs parallel mappings in two
steps. The first step determines a suitable successor
relation S while the second step finds a substitution
for M .
To determine S, we first find substitutions for the
type variables ff and fi. For the transportation problem
we get
ff 7! baggage
Now we can analyze the range type nat \Theta
seq(vertex) to find a canonical successor relation on its
elements based the basic types it is composed of. We
know the usual successor function on natural numbers,
and a canonical way to extend sequences is to append
an element. In analogy to lexicographical orderings on
pairs, we construct a successor relation by extending
either element of a pair. Thus, we define S by
hn;
We substitute (5) for S in (3). After simplification we
get
capacity
As in Section 5.1, we can now easily determine a substitution
for M and get the map that assigns to each
b in bs the non-delayed path only consisting of the
source node of b.
Like the algorithm of Section 5.1, the one working
with image modification has a high potential for
optimization and its development proceeds by filter
construction and optimization.
6 Optimization and Results
The algorithms resulting from the instantiation of
the scheme in Figure 3 are so inefficient that optimization
is absolutely necessary. The efficiency of the
resulting code heavily depends on the adequate choice
of filters and program transformations.
Important optimizations on the resulting algorithm
are the introduction of a priority queue on search
spaces and simplifications on often used predicates,
such as capacity bounded. We have also eliminated
common subexpressions and introduced an analysis of
the transportation net with respect to the input baggage
to eliminate vertices that do not lie on feasible
paths.
The ordering on search spaces used in the priority
queue encodes a heuristic to determine which node of
the search tree to consider next. We have used one
based on cost, total delay, and length of the paths in
a plan.
Test runs of the algorithms show that, despite the
optimizations, performance of both is still poor. They
also reveal that the algorithm based on image modification
is about a factor of two faster than the one
based on domain extension.
The size of theories and programs are summarized
in

Table

1.
Document Lines
Library of Specifications 490
Domain Theory 240
Algorithm Theory 350
Implementation 920

Table

1: Size of theories and programs
All specifications are written in the specification
language SPECTRUM [3]. We use an existing library
of basic spectrum specifications such as natural
numbers, sets, sequences, directed graphs and
others. Based on these modules, the domain theory
comprises about 240 lines. The algorithms extend the
domain theory by 110 lines. Both schedulers are implemented
in the functional language OPAL [10]. The
translation of specifications into executable code and
its optimization produces about 920 lines of code for
the OPAL program. The code is well-structured and
highly reusable. Both implementations share most of
the code which facilitates exploring alternatives.
The case study required an effort of approximately
9 person months. We spent about one third of that
time to learn the KIDS approach. Approximately 75%
of the remaining time were devoted to building the
domain theory.
There exists a number of approaches to algorithm
design and program synthesis, e.g. [1, 4, 8, 9]. We have
chosen the KIDS approach for our case study because
it provides design steps that reflect significant design
decisions of programmers and are described precisely
by logical theories. In this way, they are good reference
points for software engineers who wish to learn and
use them. However, we did not use the KIDS system
because we wanted to have full control over the design
process and adapt it to our needs if necessary.
Transportation scheduling. Our case study relates
to the research on design of transportation schedulers
at Kestrel [15, 16]. They study schedulers that
assign trips to resources like planes, ships, and trucks
to meet movement requirements. In this setting, trips
fully occupy resources for an interval of time, i.e. the
load of a resource cannot be extended during a trip.
Furthermore, a trip changes the availability of a re-
source: the destination of one trip becomes the source
of the next one. In baggage transportation, how-
ever, load of resources can continually change as baggage
flows through the net, but source and destination
points of a resource remain fixed in time.
Another difference lies in the focus of our work. For
several years, a highly specialized theory on transportation
scheduling has been developed at Kestrel
with the aim to produce extremely efficient schedulers.
Recently, this has even led to a refinement of the abstract
global search theory [16]. The purpose of our
case study, in contrast, has been to study in how far
the KIDS approach as documented in the literature
can support programmers who have no particular experience
with the approach, to design algorithms for
a non-trivial problem.
Process model. The steps in designing a global
search algorithm: specializing a theory, deriving fil-
ters, and applying optimizing program transforma-
tions, provide a clear separation of concerns during
design. Specialization determines the basic structure
of the search, necessary filters exploit properties of
the application domain, and only the final program
transformations and data type refinements eliminate
redundancies in the code and "fuse" filters with the
basic search structure to gain efficiency.
Each of these tasks corresponds to one cycle in the
process model that we introduced in Section 4. Thus
the model helps programmers to focus activities on a
particular task and to avoid introducing certain design
ideas at the "wrong" time into the development. In
early attempts to design the algorithm of Section 5.2,
we tried to introduce optimizations too early - trying
to generate delayed routes only if necessary - which
totally messed up our design.
The first phase of the development, before a sufficiently
complete application domain theory is avail-
able, is the most complex part of the process. We
found prototyping useful to understand the problem
domain, but techniques to guide theory development
remain to be established.
With a domain theory at hand, the KIDS approach
is well suited to construct prototypes in little time.
This supports exploring alternative designs.
Termination. In the global search theory we have
used, the issue of termination of the constructed algorithms
is not addressed. This lead us to the somewhat
unnatural introduction of the upper bound md(g; bs)
on delays (cf. Section 5).
Termination of global search algorithms can be
spoiled in two ways. There may be branches of the
search tree with infinite length, or there may be nodes
with infinitely many children. In [14], a well-founded
ordering is introduced into the abstract global search
theory to prevent infinite chains of Split-operations.
Kreitz [7] has formalized global search in the Nuprl
type theory [4]. He prevents infinite branchings of
the search tree by using only finite sets in his for-
malization. He introduces wf-filters to prune infinite
branches and proposes to provide a collection of wf-
filters for each theory.
There are methodological reasons not to require
termination of all global search theories. Both theories
used in Section 5 enumerate an infinite number
of maps. Still, we would appreciate a systematic way
that relieves programmers of dealing with termination
on-the-fly.
Dealing with incomplete design knowledge. As
we have seen in Section 5.2, it is not unlikely that the
knowledge expressed in design theories fails to support
a particular design idea. Although we are not aware
of systematic support for constructing new theories in
KIDS, it is still worthwhile to stick to the approach
and develop a new design theory that describes the
desired search strategy in an abstract way. In [5], we
decided to construct the problem specific algorithm
theory of Section 5.2 in one step and to manually verify
it against the abstract global search theory. This
decision was mainly due to lack of experience and increased
the complexity of the task considerably. More-
over, it led to a less efficient algorithm.
It seems to be unlikely to find "practically com-
plete" knowledge bases for software construction sys-
tems. Such systems should be designed to ease routine
extension of their knowledge bases. In [6], a generic
system architecture based on the notion of strategies
is proposed. Strategy modules have a clearly defined
interface to the system kernel, so new ones can be
integrated into the system in a routine way. The system
Specware [17] under development at Kestrel also
seems to allow for a modularized and easily extendible
knowledge base.
Constructing a new global search theory is a non-trivial
task and deserves support if the approach shall
be applied routinely. A starting point may be the
observation that search strategies often seem to derive
from the structure of the output domain R.

Acknowledgement

. We would like to thank David
Basin, Maritta Heisel and Burkhart Wolff for fruitful
discussions. Klaus Didrich and Maritta provided
comments on a draft of this paper.



--R

Artificial Intelligence
A spiral model of software development and enhancement.
The requirement and design specification language Spectrum.
Implementing Mathematics with the Nuprl Proof Development System.
Eine Fallstudie zur Entwicklung korrek- ter Software: Steuerung einer Gep-ackf-orderanlage
Tool support for formal software development: A generic ar- chitecture
Deriving Programs that Develop Programs.
Automating Software Design.
A deductive approach to program synthesis.
The programming language OPAL.
Kestrel Interactive Development System
Algorithm theories and design tactics.
Structure and design of global search al- gorithms
KIDS: A semiautomatic program development system.
Transformational approach to transportation scheduling.
Synthesis of high-performance transportation schedulers
Specware: formal support for composing software.
--TR
program synthesis;KIDS;scheduling;formal methods