Specification-Based Browsing of Software Component Libraries.
Specification-based retrieval provides exact content-oriented access to component libraries but requires too much deductive power. Specification-based browsing evades this bottleneck by moving any deduction into an off-line indexing phase. In this paper, we show how match relations are used to build an appropriate index and how formal concept analysis is used to build a suitable navigation structure. This structure has the single-focus property (i.e., any sensible subset of a library is represented by a single node) and supports attribute-based (via explicit component properties) and object-based (via implicit component similarities) navigation styles. It thus combines the exact semantics of formal methods with the interactive navigation possibilities of informal methods. Experiments show that current theorem provers can solve enough of the emerging proof problems to make browsing feasible. The navigation structure also indicates situations where additional abstractions are required to build a better index and thus helps to understand and to re-engineer component libraries.
Introduction
Large software libraries represent valuable assets but the larger they grow, the
harder it becomes to capitalize them for reuse purposes. The main problems are
to keep the overview over the library and to extract appropriate components.
This requires better library organizations and retrieval algorithms than a linear
search through a
at list of components.
Libraries are thus often structured by syntactic means, e.g., inheritance
hierarchies. But this is misleading because it need not to express any semantic
relation between components. Information science oers semantic methods for
library organization and component retrieval e.g., [17, 24], but these methods
are informal because they rely only on the meaning conveyed by words.
As a more exact alternative, the application of formal specication methods
to software libraries has been investigated, starting with [10, 23, 25]. The general
idea is quite simple. Each component is indexed with a formal specication
which captures its relevant behavior. Any desired relation between two components
(e.g., renement or matching) is expressed by a logical formula composed
This work is supported by the DFG within the Schwerpunkt \Deduktion", grant Sn11/2-3.
from the indices. An automated theorem prover is used to check the validity of
the formula. If (and only if) the prover succeeds the relation is considered to
be established. The most ambitious of these approaches is specication-based
retrieval [21, 22, 18, 26, 6]. It allows arbitrary specications as search keys and
retrieves all components from a library whose indexes satisfy a given match
relation with respect to the key.
However, in spite of all research eorts (cf. [19] for a detailed survey),
it is still far away from being practicable. Notwithstanding all progress in
automated deduction, the required theorem proving capabilities remain the
main bottleneck. Here, we investigate a more practical approach, specication-
based browsing of component libraries. Its crucial success factor is that any
time-consuming deduction can be moved into an o-line indexing phase (\pre-
processing") and can thus be separated from navigation. The user works only
on the pre-processed, xed navigation structure which re
ects the semantic
properties of the components with respect to the index.
We show that dierent match relations must be used to build an appropriate
index and how formal concept analysis can be used to build a concept lattice
which serves as navigation structure. Both techniques|specication-based
library organization [9, 18] and concept-based browsing [7, 12]|have been proposed
before, but their combination is new and unique to this research. It thus
combines the exact semantics of formal methods with the interactive navigation
of informal methods.
Experiments show that this approach is feasible. Apart from writing the
specications in the rst place, indexing can be fully automated. Current theorem
provers can solve enough of the emerging problems, even with modest
timeouts. Calculation of the concept lattice is fast enough and navigation works
without delay.
Specication-based browsing is not only useful for reuse but also for analyz-
ing, understanding, and re-engineering component libraries. Although browsing
is dened via specications, they are not actually required for navigation.
Instead, symbolic names can be used which \hide" the actual formulas. An
intelligent choice of such abstractions can thus speed-up and improve under-
standing. The lattice even indicates situations where additional abstractions
are required to build a better index.
Browsing vs. Retrieval
Library browsing and retrieval are closely related but following [19] a clear distinction
can be made. Retrieval consists in extracting components which satisfy
a predened matching criterion. Its main operation is thus the satisfaction check
or matching. The criterion is usually given by an arbitrary user-dened search
or query which is matched against the candidates' indices. Browsing consists
in inspecting candidates for possible extraction, but without a predened
criterion. Its main operation is thus navigation which determines in what order
the components are visited and whether they are visited at all. Browsing
usually works stepwise and we denote the set of all components which can be
visited in the next step as the focus. In contrast to retrieval, it requires no
search key but works on a pre-processed, usually hierarchical navigation struc-
ture. The obvious although not optimal way to compute such a structure is
to order the components by inclusion on their retrieval results using their own
index as query.
In the specication-based case, these dierences prove to be crucial for the
greater practicability of browsing. The pre-processing of the navigation structure
allows us to resort to o-line proving and thus to evade the deductive
bottleneck. Less obvious but equally important, the construction of the hierarchy
via a cross-match of the component library against itself benets the
proof problems. Since no arbitrary user specications are involved, the spec-
ications are much more uniform in style. This allows some obvious prover
tuning; however, the real gain comes from the absence of data mismatches.
Consider for example a graph library where the graphs are represented as map
from nodes to node sets and a query using a representation as a list of node
pairs. Then, the prover must repeatedly, for each candidate, show that both
data representations are equivalent. Although signature matching can mitigate
the data mismatch problem [6], it is still the major source of complexity in
deduction-based retrieval.
Renement Lattices Reconsidered
Formal specications can be used to order components and hence to organize
libraries hierarchically. These hierarchies can then be exploited to optimize
retrieval or to compute a navigation structure. The obvious question is how
to order the components and the obvious answer is by renement or plug-in-
compatibility [21, 6]. Given two components G and S with respective axiomatic
specications (pre G ; post G ) and (pre S ; post S ), S is said to rene G (or to be
more specic than G; S w G, or G to subsume S), i
(pre G ) pre
holds. 1 Intuitively, (1) expresses the fact that S can be plugged into any place
where G is used because it has a wider domain and produces more specic results
than G. Using a relational view (i.e., specications are considered as sets of
valid (input, output)-pairs), [18] show that (1) denes a partial order which
induces a lattice-like structure on the set of all specications. This structure
is generally known as the renement lattice although it is strictly spoken no
lattice.
Turning the renement lattice into a navigation structure for library browsing
exposes, however, some unexpected problems. First of all, libraries do not
oer enough structure, i.e., the renement hierarchies they induce are too shal-
low. While this is a good thing from a design point of view|it simply says
that the library contains only little redundancy|it is a bad thing for browsing.
It can be overcome by the introduction of meta-nodes or abstractions. Such
specications do not represent real, existing components but just factor out
1 For the sake of brevity, we shall omit the quantication over the respective argument and
return variables and their identication via type compatibility predicates. For arguments ~x
and result variables ~y, the full form is
pre S (~x S post G (~x G  ~y G ))).
similarities between some of them. As an example, consider the specication of
an abstract element lter: 2
lter some (l : list) r : list
pre l
post exists l1,
lter some species only that a singleton element is removed from the list (hence
it cannot be empty) but not which one. It is thus via (1) rened by both
components tail and lead:
list lead (l list
pre l pre l
post exists post exists
However, a nave introduction of meta-nodes yields unexpected results. If we
introduce another meta-node segment
segment (l list
pre true
post exists l1, l2 : list &
to capture the property that both components return continuous sublists of
their argument, this does not work: neither tail nor lead rene segment. The
reason for this at rst glance counterintuitive behavior is that segment is specied
as a total function (pre segment
both tail and lead are partial. And
while we can x this particular
aw by setting segment's precondition also to
becomes increasingly infeasible. If the library also contains
components which work on sorted lists only, we have to integrate this property
into the precondition, too. In eect, if we want an abstraction which captures
all segment-like components we have to adjoin all occurring preconditions con-
junctively. If, however, two of them are contradictory the result becomes false
and segment subsumes the entire library.
The solution to this dilemma is easy. While we can use renement to index
components with abstractions, we additionally need a second relation to model
the above situation. Since we are only interested in the eect of the calculation
(i.e., the postcondition post G ) we can drop pre G . We want post G to hold on
the appropriate domain only, hence
pre post G (2)
which is also known as conditional compatibility [6] or weak post match [21]
in deduction-based retrieval. We can then consider G as derived attribute or
feature [22] of holds whenever the execution of S was legal
(pre S holds) and terminated (post S holds.) In our example, segment is a feature
of tail and lead, as expected. It is easy to verify that features are inherited along
with the renement relation, i.e., if R renes S and G is a feature of S, then G
is a feature of R, too.
We use VDM-SL for our example specications. Here, ^ means concatenation of lists, [
the empty list, [i] a singleton list with item i. & reads as \such that".
A similar problem arises when we want to consider preconditions only. While
we can use the abstraction total
list
pre true
post true
to subsume all total functions, it is much harder to index partial functions
properly. The meta-node
requires non empty (l list
pre l
post true
correctly subsumes all functions which work on non-empty lists only but it
is not really appropriate: it also subsumes all total functions and is thus not
discriminative.
Hence, we need a third relation. Since we are now only interested in the
properties of the legal domains, we can drop the postconditions. But in contrast
to renement we want the domain of S now to be more restricted, hence
pre S ) pre G (3)
Again, G is a derived attribute of S|it is a requisite, S w r G|and using (3),
requires non empty now works as index. Requisites are also compatible with
renement but in contrast to features their absence is propagated. If R renes
S and G is no requisite of S, then G cannot be a requisite of R.
top
run lead tail
duplicate
rst
requires
non
empty
segment front
segment
works
on
empty
total lter
some
top
run w w f w f w w
lead
tail w w r w f w
duplicate rst w w r

Figure

1: Example index

Figure

1 shows the index for the examples in this paper. The components
are represented as rows, the attributes as columns; the symbols indicate which
relations have been used to index the components with the respective attributes.
We also see that the library is indeed shallow: each component indexes only
itself.
However, (1-3) are not the only sensible relations we could use. Instead
of indexing a component S with its requisites, we could also index S with all
requisites it does not require, i.e., with all its valid border conditions. In terms
of preconditions, this is formalized by
:pre G ) pre S (4)
and denoted by S w  r G: G is not a requisite for S, or S also works on G.
Hence, we have of course tail 6w
r requires non empty but for a topological sort
function
top list
pre acyclic(l)
post top
we have top sort w
r requires non empty as expected. However, in principle, (4)
is not necessary. We can achieve the same eect using a modied version
works on empty (l list
pre
post true
of requires non empty and renement: top sort w works on empty. 3 However,
this hides the fact that requires non empty and works on empty are complementary
to each other.
We now use (1-3) 4 to compute an appropriately modied version of the
renement lattice but even this variant is not yet adequate for browsing. It
still lacks the single-focus property, i.e., it does not contain enough structure to
represent the focus by a single node. Consider for example lead and tail. Apart
from further renements, they are the only two components which have the
feature segment and are subsumed by lter some at the same time. 5 Yet there
is no meta-node to represent this and a user has to keep his focus on both distinguishing
properties to capture the conceptual similarity of the components.
The deeper reason for this is that even the modied renement lattice has
lattice-like properties only on the set of all possible specications, not on arbitrary
subsets or libraries. True lattices, on the other hand, have the single-focus
property by denition and we will show how to embed the renement lattice
into a true lattice using formal concept analysis.
4 Concept Lattices
4.1 Formal Concept Analysis
Formal concept analysis [30, 8, 3] applies lattice-theoretic methods to investigate
abstract relations between objects and their attributes. A concept lattice
is a structure with strong mathematical properties which reveals hidden structural
and hierarchical properties of the original relation. It can be computed
automatically from any given relation.
3 Notice that this relies on the fact that post works on empty = true|otherwise, the postcondition
part of (1) would not be valid.
4 We still need renement to represent all information of interest. E.g., we cannot split total
into a requisite and a feature which have both the value true because both of them index the
library.
5 By lter some we have to remove an element, but by segment we are not allowed to split
the list. Hence, there are only the two choices to remove the element at either end of the list.
Denition 1 A formal context is a triple (O; A; R) where O and A are sets
of objects and attributes, respectively, and R  O A is an arbitrary relation.
Contexts can be imagined as cross tables where the rows are objects and
the columns are attributes. Hence, the index shown in Figure 1 can also be
considered as a formal context, provided that the dierent relations (i.e., w; w r
and w f ) are merged.
Denition 2 Let (O; A; R) be a context, O  O and A  A. The common
attributes of O are dened by (O) def
Rg, the
common objects of A by !(A) def
Rg.
Objects from a context share a set of common attributes and vice versa.
Concepts are pairs of objects and attributes which are synonymous and thus
characterize each other.
Denition 3 Let C be a context. is called a concept of C
A and
O and A (c) def
are called c's extent and intent,
respectively. The set of all concepts of C is denoted by B(C).
Concepts can be imagined as maximal rectangles (modulo permutation
of rows and columns) in the context table, e.g., (flead, tailg, fsegment, requires
non empty, lter someg). They are partially ordered by inclusion of extents
(and intents) such that a concept's extent includes the extent of all of its
subconcepts (and its intent includes the intent of all of its superconcepts).
Denition 4 Let C be a context, c 1
and
c 2 are ordered by the subconcept relation, c 1  c 2 , i O 1  O 2 . The structure
of B and  is denoted by B(C).
The intent-part follows by duality. As an immediate consequence of the
preceding denitions we get that the strict order corresponds to strict inclusion
of extents and intents, i.e., c 1
and A 1
The following basic theorem of formal concept analysis states that the structure
induced by the concepts of a formal context and their ordering is always a
complete lattice. (Cf. Figure 2 for an example lattice.)
Theorem 5 ([30]) Let C be a context. Then B(C) is a complete lattice, the
concept lattice of C. Its inmum and supremum operation are given by
i2I

i2I
O
i2I
_
i2I

i2I
O i ));
i2I
Each attribute and object has a uniquely determined dening concept in
the lattice. This can be calculated from the attribute or object, respectively,
alone.
Denition 6 Let B(O; A; R) be a concept lattice. The dening concept of an
attribute a 2 A (object is the greatest (smallest) concept c such that
a 2 A (c) (o 2 O (c)) holds. It is denoted by (a) ((o)).
Theorem 7 ([3]) In any concept lattice we have
and
4.2 From Renement Lattices to Concept Lattices
[12] has shown that keyword-indexed components can be considered as a formal
context with the components as objects and the (informal) keywords as
attributes. We now lift this idea to formal specications.
Denition 8 Let be a formally specied library with components
L, requisites R, features F , and abstractions A. Its induced context is
dened by
Again, we consider the components as objects, and, of course, the keywords
are replaced by (the names of) the specications 6 but the context table is
slightly more complicated. To prevent dierent components from \collapsing"
into a single concept if the index is insu-cient, the component specications L
double as objects and attributes. The relations, however, remain original.
works on empty
(i)
segment
@
@
@
@
@
(ii)
requires non empty
total
front segment
(iii)
lter some
top sort
top sort
run
run
(iv)
lead
lead
tail
tail
duplicate rst
duplicate rst


Figure

2: Example lattice
We then calculate the concept lattice from this context. Figure 2 shows the
result for the example context. Each bullet represents a concept. The labels
6 Wlog. we assume that L; R; F , and A are pairwise disjoint.
over the bullet are the attributes dened at this concept. E.g., the concept (iii)
denes the attribute lter some. However, since attributes in this representation
are inherited downwards, its intent A is the set fsegment, requires non empty,
lter someg. None of the attributes are equivalent in the sense that they index
the same set of components. Hence, each concept introduces only one attribute.
The labels under the bullet denote the objects dened at this concept, e.g., lead
at (iv). Since none of the actual components subsumes an other, each concept
introduces at most one object and is atomic if it introduces an object at all.
The concept lattice is not an \extension" of the renement lattice: for two
attributes a 1 ; a 2 with (a 1 )  (a 2 ) it is possible to be completely unrelated,
i.e., neither of the relations (1-3) holds. However, for two reasons, it is an
adequate representation of the index. First, subconcepts preserve renement
of the original components. Second, a superconcept can be distinguished from
any subconcept by an attribute which is not valid for at least one component
in the extent of the superconcept but is valid for all components in the extent
of the subconcept. Formally:
Theorem 9 Let B(CL ) be the concept lattice of the context CL induced by a
library L and c 1
) such that either
1. 9m 2 O
2. 9 a 2 R  a 2 A (c 1
9 a 2 F  a 2 A (c 1
9 a 2 A  a 2 A (c 1
This theorem, which follows from denitions 3 and 4, makes the concept
lattice already suitable for specication-based navigation. However, we can
impose even more structure if we double R and use w  r in addition to dene
the induced context. Then, Theorem 9 holds appropriately and, additionally,
we get
Theorem 10 Let B(CL ) be the concept lattice of the context CL induced by
a library L. Then, for any two complementary requisites a;  a 2 R we have
a and consequently (a) u
Hence, the dening concepts of two complementary requisites are complementary
to each other in the lattice. Moreover, their extents divide the entire
library into two partitions which is not the case for two arbitrary complementary
nodes in the lattice.
5 Navigation in Concept Lattices
[12] has also shown how concept lattices can be used as navigation structure for
interactive and incremental retrieval (i.e., browsing in our terminology). The
focus is represented by (the extent of) a concept. Narrowing the focus is a
downward movement in the lattice and is done in two steps:
1. The user selects an additional attribute. As a consequence of the lattice
structure, the system can support this selection by calculating all
attributes which actually narrow the focus but do not sweep it entirely.
It can thus prevent navigation into dead ends (i.e., an empty focus.)
2. The system calculates the new focus in the lattice as the meet (which
exists due to Theorem 5) of the actual focus and the dening concept of
the selected attribute (obtained by Theorem 7.)
Similarly, the focus can also be widened again by de-selecting an attribute. The
system then calculates the new focus using the join operation.
In the specication-based case, navigation works quite similar. We use the
derived properties (i.e., R; F , and A) as navigation attributes. Since the property
sets are pairwise disjoint, we can even split the set of navigation attributes
into three dimensions. These dimensions are not independent of each other
but can be selected independently because all interdependencies are contained
in the concepts of the lattice. If we use the modied context (i.e., double R
and use (1-4)), we get a fourth dimension. This is still independent but due to
Theorem 10, independent selection from R and
R is not benecial. Instead, we
can toggle between them, in addition to selection/de-selection.
Initially, all attributes are de-selected and the focus concept is >: the focus
is the entire library. Now, for an example, assume that we select segment. This
reduces the focus to O tailg. Further renement is possible
by attributes whose dening concepts have a strictly smaller but non-bottom
meet with the current focus concept. Thus, for (i), any navigation attribute
is possible. If we select requires non empty, the new focus concept is (i) u
the choice of requires non empty eliminates run from the focus.
Moreover, it leaves front segment as the only possible further renement.
This navigation style is attribute-based : the focus is essentially a function
of the selected attributes. Due to their dual nature, concept-lattices also allow
object-based navigation. Here, the user selects or de-selects a single component
and the system calculates the new focus similarly. However, selecting an additional
component widens the focus and is thus realized by the join operation.
While attribute-based navigation depends on the explicit and learned choice
of functional properties and thus is more suited for reuse purposes, object-based
navigation exposes implicit conceptual similarities of components: the intent
of the focus concept contains all properties which are common to all selected
components; its extent also contains all other components which share these
properties, even if they have not been selected explicitly. Hence, it is more
appropriate for library understanding and re-engineering.
6 Practical Aspects
We made a series of experiments to support the claim that browsing is more
practical in the specication-based case than retrieval. For these, we used a variant
of the list processing library which we also used in our retrieval experiments
[6]. It comprises 5 requisites, 31 features, and 86 components and abstractions.
All example specications in this paper are taken from that library.
6.1 Calculation of the Renement Lattice
Even if the calculation of the renement lattice is done in advance and is thus
not time-criticle in principle, it is not obvious that it is feasible at all. Two
questions are of main concern:
1. How high is the computational eort in practice?
2. How di-cult are the proof problems in practice? Are current theorem
provers powerful enough?
The answer to both questions depends on the number and structure of the
arising proof problems.
At rst glance, it seems that we have to check each requisite, feature, ab-
straction, and component against each other to calculate the modied rene-
ment lattice. However, in practice this can be optimized due to three obser-
vations. First, we do not need to compare the components and abstractions
pairwise but can use recursive comparison as in [9] because renement is tran-
sitive. Then, we do not need to check requisites and features against each other
but only against the components and abstractions. Finally, since the former are
compatible with renement, we can \sink them in" once we have the renement
lattice on the other nodes ready. In the worst case, the number of problems is
thus O(jR [ F j  jA [ Lj 2 ). Nevertheless, still too many problems arise to be
handled manually. As in other software engineering applications, a fully automated
system is required which feeds and controls the prover. However, the
sheer numbers become a problem only because most of the proof problems (ap-
proximately 85% in our experiments) are logically invalid and thus not provable
at all. But theorem provers do usually not check for unprovability and are thus
stopped by time-out only. Hence, dedicated disproving lters are required.
Nevertheless, the computation is practically feasible. Using techniques from
[6] we generated the full set of more than 14.000 proof tasks (i.e., \ready-to-
run" versions of the problems which also contain appropriate axioms and prover
control information) and ltered out approximately 6.600 as unprovable. This
took approximately 8 hours on a Sun SparcStation 20. For simplicity, we did not
use the optimizations explained above. This would have reduced the original
number of tasks to about 11.000.
We then used the automated theorem prover SPASS [29] on a network of
PCs to check the surviving tasks. With a time-out of 60 seconds, SPASS was
able to solve 1.250 tasks. For the remaining 6.250 problems, we re-generated
the tasks, using a dierent subset of the axioms. After a third iteration, SPASS
had solved a total of 1.460 or almost 80% of the valid problems. This required
a total of approximately 340 hours runtime, or equivalently, a weekend of real
time.
6.2 Calculation of the Concept Lattice
Concept lattices can grow exponentially in the number of attributes and objects.
In practice, however, the worst case rarely occurs and a polynomial behavior is
usual. [12] contains more experimental evidence for this.
For our example library, the concept lattices from the full (i.e., manually
computed) and the approximated (i.e., computed using SPASS) renement lattices
contained 153 and 180 concepts, respectively. Their computation took
approximately a second and is thus negligible compared to the time required
for proving.
6.3 Navigation
During our experiments it became quickly obvious that neither the modied
renement lattice nor the concept lattice are suitable for presentation because
they are too big and complex. [12] makes the same observation and describes
a simple text-based interface which works on the attribute and object names
only. We are currently adapting this system. The navigation process itself,
however, is very fast: the system responds without noticeable delay, even for
much larger concept lattices than we are currently investigating.
6.4 Knowledge Acquisition
The formal specications of the library components and some initial abstractions
7 must be supplied. Once this seed is available, specication-based browsing
can already support further knowledge acquisition.
Consider for example a seed comprising lter some, segment, tail, lead, and
list
pre true
post exists l1 : list &
list
which computes the longest ordered initial subsegment (i.e., run) of a list. From
this seed, an initial concept lattice is calculated. Object-based navigation conrms
that both tail and lead have a common superconcept, which has the attributes
lter some and segment, and, as expected, no other objects. But it also
reveals that there is no concept which has the extent of lead and run only|
selecting both also causes tail to appear. To disambiguate tail, a feature
front segment (l list
pre true
post exists l1 : list &
must be introduced which factors out the common property of lead and run.
7 Related Work
Most work on applying specication-based techniques to software libraries examines
retrieval only. Relevant for browsing are the investigation of dierent
match relations [21] and their eect on software reuse [5, 6]. [22] introduced
features as indexes to speed up retrieval.
7 Initial requisites and features can be derived automatically by splitting of the supplied
specications. Any resulting indiscriminate attributes are merged into a single concept by
construction of the lattice.
[9] builds a two-tiered hierarchy from the library. The lower level is based on
a modied denition of subsumption which works modulo arbitrary user-dened
congruences on literals and is thus unsound in general. The upper level uses
a similarity metric derived from the normal forms of the specications. This
hierarchy is then visualized to support browsing. [18] only use subsumption to
build a hierarchical representation of a library and exploit that only to optimize
retrieval.
In programming language research, [15] and [16] apply formal methods to
the specication and verication of object-oriented class libraries. There, behavioral
subtyping corresponds to subsumption.
Concept lattices or Galois lattices have been developed as a means to structure
arbitrary observations. They have already been applied to various problems
in software engineering, e.g., inference of conguration structures [11] or
identication of modules [14, 28] and objects [27] in legacy programs. Their
application to software component libraries, however, seems to be obvious only
in retrospect, and there is only little related work. [7] also uses concept lattices
for navigation but presents the entire lattice to the user and oers only a subset
of all possible attributes for selection. As far as navigation is concerned, [12] is
thus most closely related to our own work. But there, object-based navigation,
which is instrumental in knowledge acquisition, is not supported.
Conclusions
Only specication-based methods can provide exact content-oriented access to
software components. Retrieval, however, still requires more deductive power
than current theorem provers and hardware can oer. Browsing can evade this
bottleneck by moving any time-consuming deduction into an o-line indexing
phase.
In this paper, we have shown that dierent match relations must be used to
index a library properly and how this index is turned into a navigation structure
using formal concept analysis. Experiments show that it is feasible to calculate
an approximation of the index which is accurate enough for browsing purposes,
using current theorem provers and hardware (e.g., SPASS on a small network
of PCs.) The computational eort, however, is still high.
The concept lattice reveals the implicit structure of a library as it follows
from the index. It can even indicate situations where a ner index is required.
Due to its dual nature, the lattice allows two complementary navigation styles
which are based either on attributes or on objects. Due to the lattice nature,
both navigation styles automatically have the single-focus property and refrain
the user from dead ends.
In our approach, theorem provers are used to derive formally dened properties
of components. For navigation, these formal denitions are still available
but not actually required|symbolic property names su-ce. However, since
informally dened and derived properties (e.g., reliability) are usually also represented
by symbolic names (e.g., trusthworty), concept-based browsing allows
a smooth integration of formal and informal attributes and thus refutes a conjecture
of [1] that formal and informal methods are incompatible.
Future work especially concerns scale-up. We expect the fraction of non-
theorems to grow further with increasing library size; dedicated disproving techniques
are thus one area of interest. Since the remaining tasks are homogeneous
in style, learning theorem provers [4, 2] can be expected to perform well on them.

Acknowledgments

Christian Lindig's work on concept-based retrieval also triggered this research; discussions
with him greatly improved my own understanding of formal concept analysis.
Comments by Christian, Jens Krinke, and Gregor Snelting improved the presentation
of this paper. Christoph Weidenbach did the actual theorem proving at the MPII.



--R

"Semantic-Based Software Retrieval to Support Rapid Prototyping"
"DISCOUNT: A Distributed and Learning Equational Prover"
Introduction to Lattices and Order.
"Learning Domain Knowledge to Improve Theorem Proving"
"Reuse by Contract"
"Deduction-Based Software Component Retrieval"
"Design of a Browsing Interface for Information Retrieval"
Formale Begri
"Using formal methods to construct a software component library"
"PARIS: A System for Reusing Partially Interpreted Schemas"
"On The Inference of Con guration Structures from Source Code"
"Concept-Based Component Retrieval"

"Assessing modular structure of legacy code based on mathematical concept analysis"
"A Behavioral Notion of Subtyping"
"Speci cation and Veri cation of Object-Oriented Programs Using Supertype Abstraction"
"An Information Retrieval Approach For Automatically Constructing Software Libraries"
"Storing and Retrieving Software Components: A Re nement-Based System"
"A Survey of Software Reuse Li- braries"

"Speci cation Matching of Software Components"
"Classi cation and Retrieval of Reusable Components Using Semantic Features"
"The Inscape Environment"
"Implementing Faceted Classi cation for Software Reuse"
"Speci cations as Search Keys for Software Libraries"
"NORA/HAMMR: Making Deduction- Based Software Component Retrieval Practical"
"Applying Concept Formation Methods to Object caton in Procedural Code"
"Identifying Modules Via Concept Analysis"
"Spass and Flotter version 0.42"
"Restructuring Lattice Theory: An Approach Based on Hierarchies of Concepts"
--TR

--CTR
Katsuro Inoue , Reishi Yokomori , Tetsuo Yamamoto , Makoto Matsushita , Shinji Kusumoto, Ranking Significance of Software Components Based on Use Relations, IEEE Transactions on Software Engineering, v.31 n.3, p.213-225, March 2005
Benedikt Kratz , Ralf Reussner , Willem-Jan van den Heuvel, Empirical Research Similarity Metrics For Software Component Interfaces, Journal of Integrated Design & Process Science, v.8 n.4, p.1-17, December 2004
Ge Li , Lu Zhang , Yan Li , Bing Xie , Weizhong Shao, Shortening retrieval sequences in browsing-based component retrieval using information entropy, Journal of Systems and Software, v.79 n.2, p.216-230, February 2006
Balaji Padmanabhan , Alexander Tuzhilin, On the Use of Optimization for Data Mining: Theoretical Interactions and eCRM Opportunities, Management Science, v.49 n.10, p.1327-1343, October
browsing;software reuse;formal specifications;retrieval;software component libraries