Efficient Specification-Based Component Retrieval.
In this paper we present a mechanism for making specification-based component retrieval more efficient by limiting the amount of theorem proving required at query time. This is done by using a classification scheme to reduce the number of specification matching proofs that are required to process a query. Components are classified by assigning features that correspond to necessary conditions implied by the component specifications. We show how this method of feature assignment can be used to approximate reusability relationships between queries and library components. The set of possible classification features are formally defined, permitting automation of the classification process. The classification process itself is made efficient by using a specialized theorem proving tactic to prove feature implication. The retrieval mechanism was implemented and evaluated experimentally using a library of list manipulation components. The results indicate a better response time than existing formal approaches. The approach provides higher levels of consistency and automation than informal methods, with comparable retrieval performance.
Introduction
The concept of component reuse is fundamental to all engineering disciplines. Components provide levels of
abstraction used to effectively construct increasingly complex systems. Software Engineering is no exception,
where a main focus has been providing languages and methodologies to help software designers create useful
and reusable abstractions. In fact, software reuse was recently described by Mili et al. as the "only realistic
approach" to meet the needs of the software industry [23].
The potential for software reuse is not limited to source code, but includes algorithms, architectures,
domain models, design decisions, program transformations, documentation - virtually every possible aspect
of a software system. In addition, the benefits of software reuse extend beyond the design phase to the
analysis and maintenance phases of development. While this article focuses on functional components, the
methodology presented is compatible with any software reuse artifacts where a refinement ordering exists
between specifications. This includes source code, high-level components [1], software architectures [9, 26],
and program transformations [4]. Note also that component retrieval is not confined to library reuse; it
can also be considered in the context of integrating components into generic software architectures, either
statically [1] or dynamically [27].
While the potential benefits of software reuse are far reaching, in practice software reuse has not flourished.
There are both managerial and technical reasons for this. One major technical barrier has been providing
tools to automate the reuse process. To understand the reason for the technical difficulty in automating
reuse, it is helpful to decompose the library reuse process into three activities:
Retrieval - Specifying a query and locating potential reuse candidates within a software library.
Evaluation - Determining the relationship between a retrieved component and the specification of the
desired component.
Adaptation - Making changes to a component to meet reuse requirements.
Ideally, a reuse tool should provide automated assistance for all three reuse activities. These activities
are interdependent: high reuse potential (from retrieval) should indicate low reuse effort (during evaluation)
with respect to known adaptation methods. However, automation is difficult because each activity requires
different information about a component. Retrieval benefits from an abstract classification of component
function that supports efficient comparison. For automated evaluation to be useful, it must provide a designer
with both a precise relationship and a high level of assurance. Therefore, evaluation depends on a precise
and detailed description of component behavior. Adaptation requires knowledge about the structure of a
component and the functions of its sub-components. Therefore, the choice of a component representation
scheme determines what software reuse activities can be automated effectively.
Source code reuse has been the main focus of most software reuse efforts. However, automation of the reuse
processes requires understanding aspects of a component that are not described in source code. Source code
provides a description of how a component performs its function. For purposes of retrieval, we are interested
in precisely what this function is. The difference between what and how represents a semantic gap that makes
it difficult to understand the function of the code and recognize a potentially reusable component. Source
code is not a sufficient representation to support automation of the reuse processes. Therefore, a method is
required that represents the additional information necessary to automate reuse.
1.1. Specification-Based Reuse
Formal specification languages provide the expressiveness and precision necessary to capture what the function
of a component is. Specification matching [35, 45] applies theorem proving to evaluate relationships
between specifications. Given a formal definition of reusability, specification matching can be used to evaluate
the reusability of a component with respect to a requirements specification. In addition, automated
reasoning can be used to determine what changes are necessary to reuse a component and guide component
adaptation [29, 39].
To illustrate the potential of using formal methods to assist software reuse, we present a sample scenario
of a designer interacting with a specification-based retrieval system. First the designer must develop a
specification for the desired component that will be used as a query to the library. The specification defines
the domain, range, precondition and postcondition of the desired component. The specification can be
abstract and need not be complete. For example, if a designer is looking for list decomposition methods in
a library of list manipulation components, the following query might be used:
PRE true
POST FORALL (x:E)
The result of submitting a query to the component retrieval system is a list of components, a matching,
and any necessary port substitutions. Matching conditions are formal relationships between the component
and query specifications representing conditions under which a component may be reused. The matching
conditions may be associated with a set of rules or automated mechanisms for adapting a component. In
the case of the example, the retrieval system gives the following results:
Component Match Substitutions
removeFirst Weak Post rest 7! output
removeLast Weak Post rest 7! output
split Weak Post left 7! output
split Weak Post right 7! output
The Weak Post match, defined formally as I C -OC ) OP , indicates that a component provides a solution
for part (but not all) of a problem's domain. The designer would like to find a component that covers the
entire domain. However, in this case it is not obvious what should happen in the case of an empty input
list. The designer can strengthen the precondition of the query to eliminate this case:
In response to the new query, the system provides the following results:
Component Match Substitutions
removeFirst Weak Plug-in rest 7! output
removeLast Weak Plug-in rest 7! output
split Weak-post left 7! output
split Weak-post right 7! output
The Weak Plug-in Match is one of several matches that gives a formal guarantee that a component
provides a valid solution for the legal inputs of a problem. Therefore both the removeFirst and removeLast
components can be safely reused to solve the second query.
1.2. Technical Overview
Due to the overhead of automated theorem proving, specification matching is too computationally expensive
to test a large number of components in an acceptable amount of time [7, 21, 43]. To attain practical response
times, specification matching must be limited to evaluating a small number of components retrieved by a
separate mechanism. An alternative to limiting specification matching is to limit the expressibility of the
specification language, making retrieval more efficient [31]. However, this lowers the level of assurance during
evaluation because it takes into account fewer aspects of a component's behavior. Approaches that do not
distinguish retrieval from evaluation will either have inefficient retrieval or weak evaluation.
To effectively separate retrieval from evaluation, it is necessary to maintain consistency between the evaluation
criteria and the retrieval goal. Specifically, the classification scheme used for retrieval should identify
components that will match the query specification with respect to a reusability relationship. Because evaluation
is based on component semantics, classification schemes based upon syntactical measures are not
guaranteed to be consistent with the evaluation criteria.
This paper presents a method for making specification-based retrieval efficient by using the semantic
information provided by the specifications. Figure 1 depicts the flow of design information within the
retrieval system. In the diagram, boxes represent data structures, ovals represent computations and arrows
represent data flow into computations and references between data structures.
In the system, formal specifications are used to model the problem requirements and the function of
the library components. The specifications are based on abstract data types defined in an algebraic domain
theory [14, 42]. In Section 2 we present formal component specifications. Section 3 explains how specification
matching is used to determine component reusability.
Component retrieval is made efficient by layering a classification scheme above the specifications. The
classification scheme consists of a collection of formal definitions representing possible component features
in the domain. These definitions control the classification process in place of a human domain expert.
Formalizing the scheme permits automated classification of the specifications. The semantic classification
scheme is presented in Section 4.
The output of the classification phase is a set of features that are used as a query to the component library.
The library retrieval mechanism returns components that have feature sets similar to the query. Feature-based
retrieval is discussed in Section 5. The similar components are passed on to a more detailed evaluation
that uses specification matching to determine each component's precise relationship to the requirements
specification.
The retrieval system was implemented using the ML programming language [25] and the HOL [12] theorem
proving system. In Section 6 we evaluate the response time and retrieval performance experimentally and
compare it with other retrieval methods. Section 7 compares the experimental results with other published
results. Section 8 discusses the performance of semantic classification in terms of the effects on the retrieval
system. We then discuss related work and conclude.
2. Component Specifications
Software systems can be represented at the architectural level as a collection of interconnected components
[38]. The components of a system are its constituent subsystems that encapsulate part of the system's
Classification
Scheme
Specification
Matching
Classification
Retrieval
Theory
Domain Requirements
Specification
Component
Library
Component
Retrieval
System Similar
Components
Feature
Matching
Components
Domain Modeler Designer

Figure

1. Overview of Specification-Based Retrieval with Semantic Classification
RecordList
includes Record, List(Rec)
introduces
defined
asserts 8 l:List[Rec], r:Rec, k:Key
9 r (contains(l,r) - k=r.key);
r.key ? first(l).key
assumes TotalOrder(Key)
introduces
asserts
Rec partitioned by .key
prepend
first
rest
last
contains
asserts
List[E] partitioned by empty, first, rest
append(-,e) == prepend(e,-);

Figure

2. Larch Shared Language specification of a list of records
functionality. Each sub-system is, in turn, composed of a collection of sub-systems resulting in a hierarchical
system structure. Decomposition continues in this manner until reaching components that are not
implemented by component composition but by actual source code.
Formal specifications provide benefits over informal specifications and source code descriptions. First,
because the specifications are formal, they provide a precise, unambiguous description of the component's
function. Second, the description is declarative as opposed to operational in nature, meaning that it describes
what a component does without reference to how it does it. This is important issue for reuse because
dependency upon unspecified or unintended functionality can cause problems in the context of evolving
requirements and implementations.
A formal specification can be broken into two levels of abstraction: domain theories and interface specifications
[14]. The domain theory defines the vocabulary used in the specification by providing models of
the data types and operations used in the domain of interest. Interface specifications define the behavior of
system components in terms of the domain theory.
2.1. Domain Theories
We use algebraic specifications to build domain theories. An algebraic specification defines a set of abstract
data types and operations. For example, Figure 2 contains a Larch Shared Language [14] specification for a
list of records. The RecordList specification (called traits in Larch) includes both the Record specification
and a parameterized List specification. In the List specification, operators are defined for appending,
COMPONENT search IS
IMPORT RecordList;
END search;

Figure

3. Example Interface Specification
prepending, concatenating, and computing list membership and list length. The generated by clause defines
the operators that can be used to recursively construct all values of the type. The partitioned by clause
identifies a set of operators that can be evaluated to deduce the equivalence of two values of the type. Once
a domain theory has been developed for a certain problem domain its data types and operations can be
referenced by interface specifications.
2.2. Interface Specifications
An interface specification defines the behavior of a component in terms of a domain, range, precondition and
postcondition. For example, Figure 3 shows an interface specification for a search component. The domain
and range define the input and output types of the component, respectively. The precondition specifies the
set of inputs that the component's operation is defined over, called the legal inputs. The postcondition defines
the relationship that must hold between an input and a valid output. If the precondition is true when the
component begins executing, the component is guaranteed to terminate in a state where the postcondition
is true [13]. There are no restrictions or guarantees on the behavior of the component when the precondition
does not hold.
Formally, a component specification, P , can be translated into the following predicate logic axiom:
where DP and RP are the domain and range of the component and I P (x) and OP (x; z) are the precondition
and postcondition, respectively.
3. Reusability
Using formal specifications to evaluate reusability requires a formal definition of the relationship that must
exist for a component to be reused to solve a new problem. We stress this point because existing literature
on specification-based component retrieval is not consistent in the choice of evaluation conditions. We first
consider the case where a component completely satisfies a problem or query specification. Then we discuss
other relationships that may indicate components that can be adapted and reused.
A component completely solves a problem if it results in one of the problem's valid outputs for each of the
problem's legal inputs. Formally, component specification C satisfies problem specification P if the following
condition holds:
The first conjunct states that the component will accept all legal inputs to the problem. The second conjunct
states that all valid outputs of the component for a legal problem input are valid outputs of the problem.
The behavior of a component outside of the legal problem inputs is of no concern in determining its ability to
solve the problem. We assume ignoring potential subtype substitutions. Subtypes
can be supported implicitly using predicates, such as Integer(x) ) Real(x), or explicitly for more efficient
reasoning [36].
Plug-in
Weak Plug-in
\Gamma\Psi
Plug-in Post
@
@R
Satisfies
\Gamma\Psi
Weak Post
I C - OC ) OP
@
@R
\Gamma\Psi
Stronger
Weaker

Figure

4. A lattice of specification matches used for evaluating reusability
It is not always the case that a component completely satisfying the problem will exist in the library.
Therefore, it is desirable for a query to match components that can be adapted or combined to solve the
problem. Zaremski and Wing [43, 45] have identified a collection of specification matches that can be useful
in comparing specifications. Figure 4 shows a subset of these matches that we think are of interest in
determining reusability, with the addition of Satisfies match. 1 Following Zaremski and Wing, matches are
arranged in a lattice, where an arrow between two matches indicates that the match at the base of the arrow
is stronger than (logically implies) the match at the head of the arrow. The formal notation is abbreviated
by dropping the quantifiers and variable arguments for the predicates.
The three matches on the left-most path all require that the precondition of the problem be stronger than
the precondition of the component. They differ in the set of inputs that require a valid output from the
postcondition relation of the component: Plug-in match checks the whole domain, Weak Plug-in restricts the
check to the legal component inputs, and Satisfies further restricts this to the legal inputs of the problem.
Because of the logical relationship between these matches, any components matching under Plug-in or Weak
Plug-in will match under Satisfies. However, Plug-in and Weak Plug-in will cause the disregard of useful
components if used as a retrieval condition.
The Plug-in Post and Weak Post matches differ from the others by not requiring all legal problem inputs to
be legal component inputs. If a component matches a problem in one of these ways, there could be problem
inputs that cause unspecified behavior in the component. However, we do know that for any legal problem
input that is also a legal component input, the component provides a valid problem output. Therefore,
components that match in these ways can be used as a partial solution to the problem. A collection of
such components can be composed to provide a complete solution to the problem. These matches are also
useful for finding components with non-trivial preconditions without having to specify a precondition in the
query [43].
Because the specification matches are formally defined, they can be checked using an automated theorem
prover. However, due to the complexity of automated theorem proving, specification matching is too computationally
expensive to test a large number of components [7, 21, 43]. Practical specification-based retrieval
requires an efficient way to identify components that will match the query specification with respect to a
reusability relationship. The next section presents a method for doing this by classifying components using
the semantics of their specifications.
4. Semantic Classification
The efficiency required for specification-based retrieval can be achieved using a feature-based classification
scheme. Feature-based retrieval is efficient because it relies only on the syntactic matching of attribute-value
pairs, or features. The similarity of two components is measured by the number of features they have in
common.
When applying feature-based classification by hand, library components are assigned a set of features by
a domain expert. To retrieve a set of potentially useful components, the designer translates (classifies) the
problem requirements into a set of features and the corresponding class of components is retrieved from the
library. Queries can be generalized by relaxing how the feature sets are compared.
A potential problem with feature-based classification is maintaining the consistency of the classification
process [24, 33]. Effective retrieval requires the domain expert and the developers to have a common understanding
of the intended semantics of the features. It would be desirable to systematize and automate
classification to increase the confidence that classification is consistent among the domain experts and the
developers. Automatic indexing based on semantics 2 is not practical from a code reuse standpoint because it
would require a massive re-engineering effort. However, formal component specifications provide an explicit
semantic representation that can be used as a foundation for component classification.
Automation of feature-based classification requires answering two questions [17]: how do we automatically
generate features from a specification and what are the possible features that a component can have? We
answer the first question by describing a framework for assigning features to components in a way that
assists the search for reusable components. We then discuss how we define the set of possible features used
to classify components.
4.1. Feature Set Generation
The classification scheme used for retrieval should identify components that will match the query specification
with respect to the reuse matches identified in Section 3. Inspection of these specification matches reveals
a general pattern: in each case part of one specification logically implies part of another specification, such
as I P . The search for these situations can be guided using necessary
conditions.
A necessary condition for a predicate P is another predicate \Phi logically weaker than P , i.e. P ) \Phi. For
two predicates, P and Q, such that P ) Q, every necessary condition of Q will be a necessary condition of
Therefore, we can commonly describe P and Q by the fact that they both logically imply \Phi.
Necessary conditions can be used in this way to assist the search for reusable components. More specifically,
they can identify components that cannot match a specification and therefore should not undergo detailed
analysis. Both the component and query specifications are classified based on a given set of necessary
conditions. A classification scheme associates a feature with each necessary condition. A feature is assigned
to a component if its associated necessary condition is logically implied by the component's specification:
The general result of this semantic classification method is that if a component has a feature set similar
to that of the query then there is the potential for a reuse match to hold between the component and query.
Conversely, components that do not have features in common are less likely to be reusable. Therefore,
syntactic comparison of feature sets can be used to efficiently approximate the semantic relationships between
components.
In general, semantic classification cannot be guaranteed to eliminate only non-matching components. The
behavior of the system depends upon the set of necessary conditions used in the classification scheme and
which reuse matches are being approximated. In effect, approximate reasoning based on feature sets is
unsound and incomplete. However, this should not be considered as a critical flaw until it is clear what
its effects are on the practical performance of the system [5]. The impact of unsound and incomplete
classification is evaluated by experimentally measuring its effect on retrieval performance (Section 6).
4.2. Feature Definitions
The classification process is controlled by a collection of feature definitions that determine the set of necessary
condition/feature pairs used. The feature definitions capture the knowledge a domain expert would use to
classify components by hand. By formally defining the classification features and the feature assignment
process, classification can be fully automated.
Filter(T

Figure

5. Sample feature definitions for a data-flow abstraction
To characterize aspects of interface specifications, the features must represent abstract relationships between
component inputs and outputs. The feature definitions link the feature names and values to logical
predicates which specify the associated concept. Feature definitions have the following format:
The feature name provides a syntactic label for a concept. The feature value (Type1; Type2) represents
data type parameters that are instantiated based on the domain and range of the specification. If two
components perform a similar function over different data types, they will have a feature with the same
name, but different values. The variables x and y are actually metavariables that range over the set of input
or output variables for a component. The isIO() predicates, either isInput() or isOutput(), determine
which of these sets a metavariable ranges over and associates the type of the variable with the feature
value parameters. The Condition() predicate is the necessary condition associated with the feature. A
feature definition is instantiated by substituting in all combinations of input and output variables from the
component being classified. Instantiation is restricted by type checking any operators which are used when
specifying Condition().
The set of features used to classify a reuse library is domain dependent; the necessary conditions in the
feature definitions are specified in terms of the formal domain theory. This allows specific abstractions to
be made about operators that provide similar functionality over different types in the domain. For example,
the containment operator (contains()) is used to describe containment in many different situations. By
referencing this operator in a feature definition, we can draw similarities between components whose function
is specified in terms of containment. Figure 5 shows a subset of the features that are currently defined that
provide a data-flow style abstraction for the list processing domain. For example, the Select feature represents
the case where an output is an element of an input variable. Because the definition is parameterized on the
datatypes, Select is a possible feature whenever the containment operator exists between an input and output
type. This set of feature definitions is used in the following example.
4.3. Classification Example

Figure

6 shows the classification of the search component from Figure 3 based on the first two feature
definitions from Figure 5. First, the domain and range of the interface specification are substituted into the
feature definitions to create the set of feature/necessary conditions used for classification. For example, the
Domain
Theory
Instantiate
Feature/Goal
Pairs
Definitions
Feature
Proof Tactic
Specialized
Feature
Assignment
Requirements
Specification


Figure

6. Example: feature-based classification of a search component
Select and NonMember feature definitions:
are instantiated with the input variables and types from the domain (input :
(Rec) of the specification, giving:
The second and fourth instantiated definitions are eliminated due to type checking constraints, because the
Bool is not defined in the domain theory.
Next, the specialized proof tactic is used to check that the necessary conditions are implied by the specifi-
cation. For example, the following proof obligation is generated for the first instantiated definition:
In this example, the proof for the term contains(input; item) succeeds. Therefore, its associated feature,
Select(List[Rec]; Rec), is assigned to the component.
5. Retrieval
Given the feature set representation for a problem, we wish to retrieve components that match the problem
in terms of the formal specification matches. Because the features are assigned to the components based on
necessary conditions, the less features that a component has in common with a query, the less likely it is
that one of the reusability matches holds between the two. Therefore, we are interested in components that
have features in common with the query.
Because identical specifications will have identical feature sets, the initial query is for components having an
identical feature set to the problem. If there are no such components, the query is generalized by loosening the
feature comparison constraints to include a larger class of components. In the prototype, query generalization
is automated and continues until the number of retrieved components reaches a user-supplied threshold.
The first step in generalization is to weaken the requirements for feature value equivalence. Because
the feature values represent types that the component operates over, this identifies components performing
similar operations on different types. The second step is to reduce the number of the problem features
that the component must contain. This allows retrieval of components that may be partial solution to the
problem. Finally, the two types of generalization are combined to find components having any features in
common with the query. The following sample retrieval session provides an example of each type of query
generalization.

Figure

7 shows two problem specifications and a set of component specifications, all with their associated
feature sets. The specifications have all been classified using the feature definitions in Figure 5 and the
resulting feature sets are listed below each specification. Components are displayed beneath the problem
specifications for which they were retrieved. To exhibit the relationship between the feature sets and the
specification matches, the strongest match that exists between the problem and a component is listed under
the component specification.
In the first example, we wish to find the record with a specified key within a list. The component is
expected to perform correctly only if there is such a record in the list. Two components are retrieved
that have identical feature sets to find. The first, search, matches under Plug-in (and therefore Satisfies)
meaning it can be used to solve the problem. The second, binarySearch, only matches under Plug-in Post
because it requires the input to be sorted. It is possible that the input list is known to be sorted, but the
designer did not include that information in the query. Therefore, binarySearch is of possible use in solving
the problem. A third component, treeSearch can be retrieved by weakening the constraint that feature
values must be equal. The treeSearch component has both the Select and Build features, however with
different type values. This component may be useful after substituting List[Rec] for Tree and Rec for
Bucket.
The second example problem is specified more abstractly than the first. The designer is looking for
components that take a list and return a smaller list composed of elements from the first list. The manner of
selecting the elements for the new list is unspecified. This query is useful for finding the existing options for
decomposing lists. The first two components that are returned, removeFirst and removeLast, both match
the query under Weak Plug-in. This is because the precondition of the components, NOT empty(input), is
required to be true to ensure that the output list is smaller than the input list. Technically, for these two
components and this query, Weak Plug-in and Satisfies are equivalent matches because the preconditions are
logically equivalent. The third component, split, only matches under Weak Post because the component
precondition is stronger than query precondition. The split component provides a valid solution to the
problem, except in the case where length(input) = 1.
6. Empirical Evaluation
Component retrieval based on brute force specification matching attempts to match a query with every
component in the library. Therefore, it involves many individual proof attempts, most of which will fail [37].
The goal of semantic classification is to eliminate components that will lead to unsuccessful proof attempts
during evaluation, saving time and effort. The number of (matching and/or non-matching) components
eliminated depends upon the performance of the retrieval system. There were several experiments performed
to evaluate the retrieval system performance.
6.1. Implementation
The semantic classification system was implemented using the the ML programming language [25] and
HOL [12] theorem proving system. Several precautions were taken to reduce the overhead of automated reasoning
during classification [28]. First, the feature sets for the library components are calculated beforehand
and stored in an index. Second, a special purpose proof tactic was constructed in HOL to solve theorems
in the form of feature implication proofs. The proof tactic is parameterized on the set of domain axioms it
applies, making it domain independent. Finally to speed up inference, inductive proofs were eliminated by
burying the induction into proofs of lemmas and adding the lemmas to the domain theory. These precau-
2Problem Specifications:
COMPONENT find IS
IMPORT RecordList;
END find;
Features: Select(List[Rec],Rec),Build(Key,Rec)
Component Specifications:
COMPONENT subSet IS
POST FORALL (x:Rec)
IMPORT RecordList;
END subSet;
Features: Filter(List[Rec],Rec)
COMPONENT search IS
IMPORT RecordList;
END search;
Features: Select(List[Rec],Rec),Build(Key,Rec)
COMPONENT binarySearch IS
IMPORT RecordList;
END find;
Features: Select(List[Rec],Rec),Build(Key,Rec)
COMPONENT treeSearch IS
IMPORT BucketTree;
END find;
Features:
COMPONENT removeFirst IS
first : Rec;
IMPORT RecordList;
END removeFirst;
Features: Select(List[Rec],Rec),Filter(List[Rec],Rec)
COMPONENT removeLast IS
last
IMPORT RecordList;
END removeLast;
Features: Select(List[Rec],Rec),Filter(List[Rec],Rec)
COMPONENT split IS
POST NOT isEmpty(left) AND NOT isEmpty(right)
IMPORT RecordList;
END split;
Features: Split(List[Rec],Rec),Filter(List[Rec],Rec)

Figure

7. Example Problem Specification and Component Specifications with Feature Sets
tions result in an incomplete proof procedure. One goal of the experiments was evaluate the impact of this
incompleteness on retrieval performance.
6.2. The Library
The component retrieval evaluation was done using a library of specification for list manipulation components.
This library has been used in experiments with other specification-based component retrieval systems [37],
providing an opportunity for direct comparison of results. The library was designed to test whether the
specification-based retrieval can handle variation in the way that components are specified and the way that
queries are posed to the system. For example, there are 3 different specifications for a head component that
takes a list and returns a list containing only the first element of the original list.
6.3. Evaluation Method
The two traditional measures of component retrieval performance are recall and precision [23]. Recall is the
ratio of the number of relevant items retrieved to the total number of relevant items in the library. High
recall indicates that relatively few relevant components were overlooked. Precision is the ratio of the number
relevant items retrieved to the total number of items retrieved. High precision means that relatively few
irrelevant components were retrieved. In general, there is a tradeoff between precision and retrieval. The goal
is to find a practical balance between the two. The relevance condition is fundamental to the evaluation of
a retrieval system. As discussed below, experiments were conducted with two different relevance conditions.
It was also informative to observe the number of components retrieved by the system. This number
can help estimate the load that would be placed on the designer to interpret the results of a query in
an interactive system, or similarly, the search space that would be faced by an adaptation system when
considering component compositions [28].
The response time of the system was also measured to determine the practicality of the method. For each
measured quantity, the minimum, maximum and median was calculated for each of the scenarios in the
experiment.
6.4. Design of the Experiments
The experiments were designed to compare the way that several factors affected the performance of the
retrieval system. The first and foremost was the ability of the automated classification system to derive
classification features. Second, we were interested in the performance of retrieval in the context of both exact
retrieval and approximate retrieval. Finally, the nature of the library raised questions about determining an
appropriate query set for experimentation. Therefore, two different query sets were used.
6.4.1. Feature Generation The retrieval system as a whole can be separated into the classification scheme
(as defined by the feature definitions) and the classification mechanism (the specialized proof tactic and
domain theorems). In a sense, the mechanism attempts to implement the scheme. Both aspects of the
retrieval system can affect precision and recall. The classification scheme affects precision by the size and
consistency of component clusters. It affects recall because a scheme may not always contain a feature that
can be inferred from a relevant components.
The incompleteness of the classification mechanism (the specialized proof tactic is incomplete) could cause
it to generate fewer features and subsequently retrieve fewer components than intended. If the missing
components are relevant it will lower both recall and precision. The classification mechanism is sound (it is
implemented in terms of sound constructs in HOL) so it will only derive implied features.
In each experiment three scenarios were tested:
1. Signature Matching [44]: retrieval based on component signatures
2. Expected Features: retrieval based on features that would be assigned by a complete proof procedure.
3. Derived Features: retrieval based on features assigned by the implemented system.
Signature matching retrieves components with identical signatures. For this library, all of the components
have identical signatures (list ! list). Therefore, the performance of signature matching provides a profile
of the composition of the library in terms of relevant components. The expected features determine the
performance that the classification scheme, if implemented perfectly, would allow. Expected features were
determined by inspection with the aid of the lattice of specifications for the library. The implemented
retrieval mechanism (i.e., the domain theory axioms together with the feature derivation tactics) was used
to generate the derived features. The results were evaluated to see how close it comes to implementing the
classification scheme.
6.4.2. Relevance Conditions The choice of a relevance condition is fundamental in determining the significance
of precision and recall measures [22]. In our experiment, we evaluated the performance of the
system with respect to two relevance conditions. First, we use Satisfies match to be consistent with standard
specification-based retrieval experiments [21, 37]. Second, we consider a relevant component to be one
that matches the query specification with respect to any of the reuse matches identified in Section 3. This
relevance condition is important in the context of the adaptation, where a relevant component is one that
can (potentially) be adapted by the system [28, 29].
6.4.3. Query Set Following the experiments done by Schumann and Fischer [37], the library components
themselves are used as the set of queries to test the performance of the system. Using the components as
the query set makes two assumptions: (1) the component specifications represent a good sample of queries
that may be asked and (2) these queries all have the same probability of being posed to the system. To get
results that would predict the performance of the tool in a realistic setting, it would be necessary to have
a distribution of queries that represents how the tool would be used. There is no study in the component
retrieval literature that would provide this information.
The library used in the experiment has several groups of functionally equivalent specifications that would, in
practice, all point to a one component. This raises a question about what should define a unique query in the
experiment: a specification or a component with potentially many specifications. Therefore, the experiment
was run once with duplicate specifications in the query set, and once without. The difference between the
results for the two cases was negligible, indicating that the system does not favor the components with
multiple specifications [28]. We present only the results from the experiment including equivalent queries
here.
6.5. Experimental Results
The experiment involved a library of list manipulation components all having the signature list 7! list. The
library contained 63 specifications for 45 functionally unique components. The experiment was divided into
two parts. For the first part, the classification scheme of Figure 5 was used. Due to the limited signatures,
only the following features applied:
Filter(T
For the second part of the experiment, the classification scheme was extended. The extension of the scheme
was guided by placing the library components into a lattice based on the Satisfies matching condition.
The domain theory theorems that were used as parameters to the classification mechanism are shown in

Figure

8. These theorems were selected by observing the failed proofs of expected features and determining
Normalization Rules:
Normalization Implications:
Rewrite Rules:
Expansion Rules:

Figure

8. Domain Theory for List Library Experiment

Table

1. Retrieval for Satisfies Match Using the Initial Classification Scheme
Scenario Retrieved Precision Recall
Signature Match 63.00 (63 - 63) 0.11 (0.02 - 0.64) 1.00 (1.00 - 1.00)
Expected Features
Exact Match 22.71 (3 - 31) 0.20 (0.03 - 0.74) 0.84 (0.05 - 1.00)
Relaxed Match
Derived Features
Exact Match 22.27 (3 - 31)
Relaxed Match 43.57 (12 - 51) 0.12 (0.02 - 0.65) 0.86 (0.10 - 1.00)
the theorems necessary to make the proofs succeed. The theorems mainly deal with reasoning about containment
(which is used to define the feature definitions) in terms of the list type constructors CONS, APPEND
and [].
6.5.1. Satisfies Match The results of the initial part of the experiment for Satisfies match are shown in

Table

1. The table entries denote the average value with the minimum and maximum in parenthesis. The
retrieval mechanism comes very close to implementing the classification scheme: the expected feature sets
were derived for 61 of the 63 specifications. The failed classification was due to the use of a three way
conditional in the specification that was not supported directly in the domain theory. The domain theory
could be extended to support these conditionals, however an effort was made to not over-specialize the
domain theory toward supporting classification application. Therefore, this extension was not made.
The distribution of expected feature sets for the library is show in Table 2. This shows that the classification
scheme does a questionable job of clustering components in the library; nearly half of the components are
only assigned the Filter feature. In fact, the 3 features are not independent but represent a generalization
hierarchy: Route ) Permute ) Filter. While it is useful to have features that specialize other features, it
would also be useful to have other orthogonal features to provide better coverage of the library.
Table

2. Distribution of feature sets for initial classification
scheme.
Feature Set No. Specifications No. Components
fFilterg
some_total
last_total1,2
tail1,3
swap id_segment
id_front
run_max_eq
segment_ne_total
id
segment_front
id_single
segment
swap_outer
swap_outer_total
swap_total
perm_r1,2
run_max_bracket
run_eq1,2,3
run_bracket1,2
lead_total1,2
lead
segment_rear
segment_ne
perm_lr1,2
id_nil
elim_dup_lr
rot_r1,2
rot_r_total1,2,3
rot_l_total1,2,3
rotate_total
rotate
rot_l1,2
tail_total1,2
elim_dup_unique_l
elim_dup_r
last head1,3
some
id_rear
elim_dup_unique_r
perm_l1,2
elim_dup_l
no_dup
elim_dup_unique_lr
FILTER

Figure

9. Lattice of Specifications for the List Component Library
The partial-order lattice induced by the Satisfies Match on the library is a useful aid for discovering
potential features. This lattice is shown in Figure 9 with the areas covered by the Filter, Permute and Route
features shown with dashed lines. As hoped, the features tend to group components that are related in the
lattice. The lattice can be used to identify groups of components that are closely related, and then their
specifications may be inspected to identify a logical feature that they share. 3
For example, the some component is the root of a tree containing last, head, some total, last total
and head total. The some component has the following specification:
POST EXISTS(i:Rec) mem1 mem2 .
This specification is very similar to the definition of the Select feature, only Select looks for an element as
an output, not a singleton list. Therefore, if the definition of Select is modified to identify a singleton list,
it should be an expected feature of all of these components.
Other useful feature can be identified using the lattice. For example, associating a feature with the id nil
component:
and its descendants provides coverage for the id segment tree an and also divides the components with the
Filter feature roughly in half in a fairly orthogonal manner. As a complementary feature to IdNil, a feature
NoNil could be defined stating that a component does not accept an empty input, with the intention that a
component could not imply both of these features.
These three features were formalized as follows:
They were added to the feature definitions and the experiment was rerun. On inspection of the derived
feature sets, it was immediately obvious that there were two problems: (1) the Some feature was never
derived and (2) many components were assigned both IdNil and NoNil, which was not the intention of the
scheme.
The source of the first problem was that the proof tactic failed to handle existential goals. This problem
was solved by extending the tactic to attempt to solve a goal by substituting in free variables from the goal
for the existential variable. Additionally, the expected results were wrong: as defined, the Some feature
will not hold for some total and its descendants. The components named * total are total functions that
map an empty input list to an empty output list. In this case, the output does not contain an element and
therefore, these specifications will not imply the Some feature.
The second problem with the extended scheme was that IdNil and NoNil were not complementary as
thought. In fact, NoNil implies IdNil because, in the case where the input is not empty, assuming it is empty
(which is be the first step in proving IdNil) allows the proof of IdNil to succeed trivially. This results in the
coverage of the IdNil feature to be nearly identical to the Filter feature, making it a useless extension. Taken
together, these experiences indicate the need for tools to support the construction of classification schemes,
as discussed in the future work section.

Table

3. Distribution of Feature Sets for Extended Classification Scheme.
Feature Set No. Specifications No. Components

Table

4. Retrieval for Satisfies Match Using the Extended Scheme
Scenario Retrieved Precision Recall
Signature Match 63.00 (63 - 63) 0.11 (0.02 - 0.64) 1.00 (1.00 - 1.00)
Expected Features
Exact Match 13.64 (1 - 23)
Relaxed Match
Derived Features
Exact Match 14.05 (3 - 23) 0.29 (0.04 - 1.00) 0.69 (0.05 - 1.00)
Relaxed Match 43.57 (12 - 51) 0.12 (0.02 - 0.65) 0.86 (0.10 - 1.00)

Table

5. Approximate Retrieval Using the Initial Classification Scheme
Scenario Retrieved Precision Recall
Signature Match 63.00 (63 - 63) 0.14 (0.02 - 0.81) 1.00 (1.00 - 1.00)
Expected Features
Exact Match 22.71 (3 - 31) 0.27 (0.03 - 1.00) 0.84 (0.06 - 1.00)
Relaxed Match
Derived Features
Exact Match 22.27 (3 - 31) 0.28 (0.03 - 1.00) 0.81 (0.06 - 1.00)
Relaxed Match 43.57 (12 - 51) 0.16 (0.02 - 0.96) 0.85 (0.07 - 1.00)
The experiment was run again, this time without the IdNil feature and with the expected results more
throughly evaluated. The distribution of feature sets is shown in Table 3. The extended scheme does a better
job of breaking the components into clusters. Nearly 1/3 of the components that were initially assigned only
the Filter feature are now assigned additional features.
The results of evaluating the system with the extended classification scheme are shown in Table 4. Compared
to the results of the previous classification scheme, there was a noticeable drop in the average number
of components retrieved along with an increase in precision. This was accompanied by a slight decrease in
recall. Once again, the classification mechanism came very close to implementing the classification scheme.
6.5.2. Approximate Retrieval The experiments were repeated while considering a relevant component to
be one that matches the query specification with respect to any of the reuse matches identified in Section 3.
Because this relevance condition is logically weaker than the Satisfies match (it is the disjunction of Satisfies
and Weak Post) the relevant components for a query will be a superset of those relevant to Satisfies.

Table

6. Approximate Retrieval Using the Extended Scheme
Scenario Retrieved Precision Recall
Signature Match 63.00 (63 - 63) 0.14 (0.02 - 0.83) 1.00 (1.00 - 1.00)
Expected Features
Exact Match 14.97 (1 - 25) 0.32 (0.04 - 1.00) 0.57 (0.04 - 1.00)
Relaxed Match
Derived Features
Exact Match 14.05 (3 - 23) 0.31 (0.04 - 1.00) 0.54 (0.06 - 1.00)
Relaxed Match 43.57 (12 - 51) 0.16 (0.02 - 0.96) 0.84 (0.07 - 1.00)
The results of the experiment using the initial classification scheme are shown in Table 5. The precision of
this experiment was higher, because more of the retrieved components are relevant. Recall remained the same
indicating that the same percentage of new relevant components is retrieved. The implementation of the
classification scheme continues to come close to the performance of a complete and consistent implementation.
The results of the experiment using the extended classification scheme are shown in Table 6. For the exact
match there was an increase in precision over the initial scheme comparable with the increase seen in the
Satisfies match experiment. However, there was a larger drop in recall. This is caused by the exact match
not retrieving many of the new relevant components. This means that the exact feature match using the
extended scheme does not approximate the relevance condition very well in terms of recall. The relaxed
match results remain consistent with the other experiments. The results indicate that relaxed feature match
is more appropriate for approximate retrieval than exact feature match.
6.5.3. Response Time The response time of the classification system during the experiments ranged from
0.15 to 0.66 seconds with an average of 0.35 seconds on a 200MHz PentiumPro processor running Linux.
Database access accounted for only 0.025 seconds, on average, therefore the bulk of the time was spent
classifying queries. This is well within the acceptable response time for an interactive system.
7. Comparison of Results
7.1. Specification-Based Retrieval
Most specification-based component retrieval systems are in the "proof of concept" stage and therefore have
not been evaluated over a sizable component library. A notable exception is the NORA/HAMMR system of
Fischer and Schumann [37]. The NORA/HAMMR retrieval system is set up as a chain of filters. The initial
filter is signature matching and they become more restrictive as they progress. The final filter in the chain
is full scale specification matching. The NORA/HAMMR system was evaluated using the same library as
our experiments using all of the specifications (with duplicates) as the query set.
As an intermediate filter, they use the MACE model checker in several configurations to select a subset
of components from the library to undergo specification matching. Using a 20 second time limit for model
checking computation, they observed average recall rates between 74.7% and 81.3% with precision between
18.5% and 16.5%. This is comparable to the results achieved with the initial classification scheme in our
experiments, however, our response time was 0.66 seconds in the worst case.
They have experimented with several automated theorem provers to do specification matching as the final
stage of retrieval. For example, using the SETHEO prover and a time limit of 20 seconds, the results were
a recall rate of 61.2% and precision of 100%. The high precision is due to the fact that SETHEO's proof
procedure is sound. The loss in recall is due to a lack of completeness that comes from a technique for
approximating induction, restricting the set of axioms available for inference and the 20 second time limit.
Lowering the time limit to 1 second causes the recall to drop below 50% [6]. Using semantic classification as
a filter prior to specification matching could reduce the load on specification matching and allow this time
limit to be raised, increasing recall.
7.2. Information Retrieval Methods
The majority of component retrieval tools used in practice are based on information retrieval methods.
Frakes and Pole conducted an extensive study of representation methods for reusable components [8]. They
did comparison of the retrieval performance of attribute-value, enumerated, faceted and keyword based
representations. The relevance determination was made by two domain experts. There is no mention of
the (manual) method used to classify the components. The recall and precision measurements were in the
30-40% and 50-100% ranges, respectively for all of the methods. Statistical analysis showed no significant
difference among the methods. Our retrieval results are consistent with these numbers.
The benefit that semantic classification provides over these methods is consistency and automation of the
classification process. While the uses have to be familiar with the specification language, they do not have to
be familiar with the organization of the component library. In addition, specification-based retrieval provides
a precise relationship that exists between a retrieved component and a query, increasing the utility of the
retrieval results. All of this is achieved with similar performance results.
Girardi and Ibrahim [10, 11] evaluate a method based on syntactic and semantic analysis of natural language
descriptions (ROSA). They use normalized versions of the precision and recall formulas because the system
returns ranked results. They used a library of 418 general purpose Unix commands and 20 queries derived
from user descriptions of frequently used commands. They report recall values in the 99-100% range with
precision values in the 90-92% range. However they do not state their relevance condition, making the results
rather non-informative. Their selection of the query set is also important because it does not evaluate the
method in the less frequent cases.
8. Discussion
8.1. System Wide Effects
The retrieval performance of semantic classification must be considered in the context of its role in the retrieval
system. The results of retrieval are passed on to an evaluation phase (based on specification matching)
that has perfect precision and recall, assuming a sound and complete proof procedure is used. The point is
that relevant components cannot be added, but only removed by specification matching. This means semantic
classification acts as a filter that sets an upper bound on the recall of the combined retrieval/evaluation
system. Limiting recall will shrink the design space that can searched, potentially lowering the quality of
the designs created by the system.
In contrast, the precision of the retrieval phase has no effect on the precision of the combined system. The
precision effects the number of proofs that must be attempted during specification matching, and therefore
has an effect on the system response time. Therefore, the recall/precision tradeoff in the feature-based
retrieval phase translates into a design quality/response time tradeoff in the context of the entire retrieval
system.
8.2. Limitations
In the experiments, the major reason for feature generation failure was due to specification that was broken
into cases based on conditions that were not supported by rules in the domain theory. In these specifications
the postcondition has the form:
To prove that a feature is implied by a specification of this form requires a proof by cases approach. To
facilitate this, there must be an axiom in the domain theory of the form:
If there are no rules in the domain theory to support the specific case decomposition used in the specification,
the feature proofs cannot succeed. This can be fixed by either guiding the user during specification to use
a set of conditions that are supported by the domain theory, or by allowing conditional features that are
assigned if a feature holds under any (rather than all) of the conditions specified.
Feature derivation runs into a similar problem in the case of partial specifications, where component
behavior is not defined for all legal inputs. A feature is only assigned to a component if it can be derived in
terms of the behavior of the component for every legal input value. Partial specifications are too logically
weak to allow a feature to be derived in the case of the undefined behavior. This can be fixed by (1)
disallowing partial specifications, (2) strengthening the postcondition for the purposes of feature generation,
or (3) allowing conditional features as described above.
There was also a problem where two components we specified in such a way that their specifications cause
non-termination of rewriting. For example, a head component with input l and output m can be specified
as:
If this statement is used as a left-to-right rewrite rule, the rewriting system will not terminate. One possible
solution is to build a timeout option into the rewriting system, similar to that used by Schuman and
Fischer [37].
Finally, it should be noted that, in general, specification-based component retrieval is susceptible to loss
of recall due to the semantic gap between a component and a specification [22]. A component is associated
with a specification if the component correctly implements a specification. However, there is a gap that
a query may fall into: it is possible that a component may satisfy a query that its specification does not
satisfy. The effects of this situation cannot be evaluated in the experiments because we are working only
with specifications. However, it should be noted as a potential limitation of the method.
8.3. Building Classification Schemes
Discovering features is not an easy process. Formalizing an abstract concept that is shared among several
components is difficult and picking a collection of useful ones is even harder. Several times during this
investigation, the intuitive concept of a feature was disproved by the system. Recognizing the utility of
hierarchical and complementary features is a good start toward building better schemes. However, tool
support would be necessary to scale the method to larger libraries and more sophisticated classification
schemes.
There are several ways that the formalized classification framework provides a foundation for automated
tools. The formal definitions of the necessary conditions can support analysis of the scheme. For example,
a set of features can be proven to be mutually exclusive while their disjunction is a tautology. Therefore,
every component would be assigned exactly one of these features. These features would provide coverage
similar to the "facets" in faceted classification [34].
It is also possible to provide support for extending classification schemes within the framework. For
example, if two distinguishable components are classified identically, it may be possible to identify the parts
of the specifications that are distinguishable and automatically derive a new feature that represents this
difference.
8.4. Signatures vs. Semantics
In most specification-based component retrieval systems, the first filter used to reduce the library is signature
matching [7, 43, 44]. Signature matching uses the types from a component's interface to determine its
compatibility with a query. The guiding assumption is that if the types do not match there is no reason to
further examine a component's behavior. We believe there are two cases where semantic classification has
potential for greater recall than signature-based approaches.
The retrieval performance of signature matching degrades when considering relevant components that could
be combined or adapted to satisfy a query. Standard signature matching will eliminate relevant components
with partial matches to an interface. Allowing partial matches would allow too many component to match,
greatly decreasing the retrieval precision of signature matching. Because feature definitions are not required
to constrain all inputs and outputs in a component, semantic classification does not have this problem. In
fact, components are retrieved that provide slices of the appropriate behavior, independent of the type used.
The type information (the feature values) is used to identify type substitutions before evaluation.
Using signatures has been suggested to discover combinations of components in a library that match a
query signature [15, 23]. We take a semantic approach to the problem of combining components [28, 29].
classification assists this approach by retrieving components that provide pieces of the appropriate
behavior. Therefore, it can locate partial solutions even when the remainder of the solution is not in the
library.
9. Related Work
The use of formal specifications to assist software component retrieval has been widely proposed projects [3,
37, 16, 21]. 4 Zaremski and Wing [45] provided a foundation for studying the more general activity of specification
matching, the verification of logical relationships between specifications. There are many approaches
to making specification-based component retrieval more efficient. However, only a few of these methods
make use of the semantics provided by formal specifications.
The NORA/HAMMR deductive retrieval tool built by Fischer and Schumann uses a series of filters to
identify reusable components [37]. This tool is novel in its use of model checking as one of the search
filters. Before running the theorem prover to check the match condition, the conditions are checked by
searching for a model in a small part of the specification theory. Since it is necessary for such a model
to exist for the conditions to hold, only those components that pass the model checking stage need to be
checked in the entire theory. They also use various techniques to improve the performance of the theorem
prover during specification matching, such as reducing the set of axioms used and parallel proof attempts.
Evaluation of prototype implementations on libraries of list manipulation functions showed very encouraging
results. However, the recall (retrieved components/useful components) of the prototype was limited by
signature matching. The notion of using filters to restrict the search space is consistent with our use of
necessary conditions to eliminate non-matching component. Because a semantic-based classification scheme
can provide better recall than signature matching, it could be used as a preliminary filter and potentially
increase recall.
The Inquire retrieval mechanism [32] within the Inscape [31] environment supports retrieval based on
component specifications. Preconditions and postconditions for components are formulated in terms of a
given set of formally defined logical predicates. An inference mechanism is used during the retrieval process
to retrieve components that provide the various predicates. The formal predicate definitions are useful as
unambiguous descriptions of the predicate vocabulary. The prototype implementation is reported to work
very well, but with a restricted specification language. The restricted language reduces the inference power
necessary for component retrieval. The methodology presented here uses a reversed approach from Inscape.
Interface specifications are defined in full first-order logic. The formally defined features (predicates) are then
assigned to the specifications if they are logically implied by the specification. In this case, the predicates are
not the complete specification of the component, but represent various aspects of the component's function.
Because feature predicates do not have to be useful as specification predicates, they can be more abstract,
allowing more flexibility in the types of similarity that can be represented. In addition, the more expressive
specification language allows precise evaluation of reusability.
Deductive program synthesis [20, 40] also makes use of formal methods to automate software reuse. For
example, the Amphion system [18, 41] successfully uses deductive synthesis to construct software from a
subroutine library for solar system geometry. In these systems, components (language primitives or sub-
routines) are represented as mathematical functions and their behavior specified via axioms. A program
is synthesized by proving that, for any valid input, there exists an output that satisfies the specification.
The occurrence of a primitive function in the proof constructed during deductive synthesis corresponds to a
call to the associated subroutine. Therefore, a component is effectively "retrieved" when its corresponding
axioms are used during the proof process. This means that the domain theory axioms and the tactics used in
decomposing proofs will determine which components are used. Ongoing research is exploring the integration
of architectural decomposition tactics with our current component retrieval system to support automated
component adaptation and integration [28, 29, 30].
10. Conclusion
Software reuse and formal specification are two methodologies that show high potential impact on software
productivity and reliability. Used together, they permit increased automation and assurance in the reuse
process. We presented how component reusability and similarity can be described formally as logical relationships
between the problem specification and a component specification. However, it is too computationally
expensive to formally verify these relationships in the quantities required for practical component retrieval.
Therefore, specification-based retrieval would benefit from a method to approximate these relationships and
identify a subset of the library to undergo verification.
In this paper, we described a method for classifying components based on their formal specifications.
Features are assigned to components based on specific necessary conditions that are implied by the component
specifications. The logical form of the specification matches determining reusability ensures that components
with similar feature sets are more likely to match. The collection of necessary conditions that controls the
classification scheme is defined formally to allow automated classification. The theorem proving required
during classification is applied in such a way that complexity of component classification is much less than
that of applying multiple specification matches. Once classified, components are retrieved via syntactic
comparison of feature sets.
The results of empirical evaluation on a library of list components show that the method can provide
retrieval performance comparable to existing methods. The benefits are a faster response time than other
formal approaches. The method improves upon informal methods by providing higher levels of consistency
and automation.
Our future work will focus on integrating specification-based component retrieval with support for automated
component adaptation and integration [28]. A long-term goal is to develop support for run-time
component integration in high-assurance component-based systems [19]. We are also investigating tools to
support development and maintenance of formal classification schemes.

Acknowledgments

We would like to thank Bernd Fischer, Gary Leavens, Amy Moormann Zaremski, Ali Mili, Santos Lazzeri
and Dale Martin for helpful comments on the development and evaluation of this research. We also thank the
anonymous reviewers of the current and earlier versions of this work for their suggestions for the presentation
and evaluation of the work. Support for this work was provided in part by the Advanced Research Projects
Agency and monitored by Wright Labs under the RAASP Technology Program contract number F33615-
93-C-1316 and the CEENSS Technology Program contract number F33615-93-C-4304.
Notes
1. We do not use Zaremski and Wing's method for identifying reuse matches based on syntactic
patterns. We select matches based on formalization of intuitive notions of reusability, and their
utility in component retrieval.
2. As opposed to free text indexing of source code and/or comments, which would not satisfy the
high level of assurance required in this application.
3. It should be noted that distances in the lattice are meaningless; the lattice was arranged by
hand to minimize the crossing of links.
4. For a general overview of component retrieval methods for assisting software reuse, see the
survey by Mili et al [23]


--R

Validating component compositions in software system generators.
Perlis, editors. Software Reusability - Concepts and Models

Program development as a formal activity.
Two theses of knowledge representation: languages restrictions

NORA/HAMMR: Making deduction-based software component retrieval practical
An empirical study of representation methods for reusable software components.
Formal Foundations for the Specification of Software Architecture.
Automatic indexing of software artifacts.
Using english to retrieve software.
HOL: A proof generating system for higher-order logic
The Science of Programming.
Languages and Tools for Formal Specification.
Generalized behavior-based retrieval
Using formal methods to construct a software library.

A formal approach to domain-oriented software design environments

Fundamentals of deductive program synthesis.
A refinement based system.
A survey of software reuse libraries.
Reusing software: Issues and research directions.
Another nail to the coffin of facated controlled-vocabulary component classification and retrieval
The Definition of Standard ML.
Correct architecture refinement.

Automated Component Retrieval and Adaptation Using Formal Specifications.
Toward automated component adaptation.
Declarative specification of software architectures.
The Inscape environment.

Rub'en Prieto
Rub'en Prieto
Specifications as search keys for software libraries.
Automated deduction and formal methods.
NORA/HAMMR: Making deduction-based software component retrieval practical
Software Architecture: Perspectives on an Emerging Discipline.
Derived preconditions and their use in program synthesis.

Deductive composition of astronomical software from subroutine libraries.
Algebraic Specifications in Software Engineering: An Introduction.
Signature and Specification Matching.
Signature matching
Specification matching of software components.
--TR

--CTR
David Hemer, Semi-Automated Component-Based Development of Formally Verified Software, Electronic Notes in Theoretical Computer Science (ENTCS), 187, p.173-188, July, 2007
Robert G. Bartholet , David C. Brogan , Paul F. Reynolds, Jr., The computational complexity of component selection in simulation reuse, Proceedings of the 37th conference on Winter simulation, December 04-07, 2005, Orlando, Florida
Sofien Khemakhem , Khalil Drira , Mohamed Jmaiel, SEC: a search engine for component based software development, Proceedings of the 2006 ACM symposium on Applied computing, April 23-27, 2006, Dijon, France
Brandon Morel , Perry Alexander, SPARTACAS Automating Component Reuse and Adaptation, IEEE Transactions on Software Engineering, v.30 n.9, p.587-600, September 2004
component retrieval;formal specification;software reuse