One of the common problems of using an algorithm written by someone else is knowing exactly what it does and under what conditions it works. These problems are compounded when we use large libraries of programs or complex systems.
One example of the importance of providing better access to libraries is illustrated by the Amphion project at NASA Ames led by M. Lowry [75]. Amphion helps users compose software from SPICELIB, a Fortran-77 library for computations in solar system geometry. Even though the routines in SPICELIB are well documented, users were reluctant to invest the effort required to learn to use the library by reading the documentation. So, Amphion users can pose problems by drawing planets, spacecraft, etc. using a graphical user interface, e.g., they can position Voyager to observe the shadow of the moon Io on Jupiter.
One difficulty with this approach is that Amphion might compose routines without regard for their pre-conditions. To solve this problem, formal methods are being used to synthesize simple routines and ensure that they are correctly connected [107].
A similar example problem arises with the opportunity to synthesize special purpose routines from specifications. For instance, scientific subroutine libraries currently contain a variety of Fast Fourier Transform (FFT) routines. Among the parameters of these routines are the number of points in the FFT, the radix used and how the FFT matrix is factored. However, it is not difficult to synthesize FFT routines directly from a specification [12,90], which leads to more flexibility. In addition, synthesized routines that use various parameters explicitly can often be better optimized than more general, parameterized routines.
A software library that uses synthesized software, as we are suggesting, has rather different characteristics from the existing approaches. In particular, a language is needed to specify the desired parameters of the FFT routine to be synthesized, and some checks need to be provided to ensure that the delivered software matches the specification.