The approach advocated in this paper results from the combination
of two research efforts:
- An effort by the first author to build a software archive
as a stratified multidimensional classification structure for
software components.
- An effort by the second and third authors
to investigate various features of the specification process and
the specification product, as well as the construction
and verification of programs.
In a recent joint publication [#!structured92!#] the first and
third authors make a proposal for constructing a database of software
components, based on the following premises:
- Entries of the database have the form of
〈specification, program〉 pairs, where the program component is correct
with respect to the specification component.
- The set of database entries is structured by means of the
refinement ordering between the specification components of the
entries.
- The retrieve key for retrieval operations on the database
take the form of a specification, and seeks to determine all
the programs of the database that are correct with respect to the key,
by matching the key against the specification components of database
entries.
Our design rationale is that by representing database entries with
arbitrarily abstract specifications and by letting the match
between a store key and a retrieve key
be defined by the refinement ordering (rather than strict equality),
we deal effectively with the diversity of software components and the
complexity of organizing such components in a database.
In this position paper we report on our progress in implementing
this software repository, using C under Unix, and an experimental theorem
prover (Otter, ©Argonne National Laboratory).
Among the Functions we have implemented we mention: Storage
of software components; Retrieval of software components;
and Approximate Retrieval of software components, to be
invoked whenever (exact) retrieval fails to produce results.