October 11, 2007, 6:15 pm, Hudspeth Hall 100
The automated construction of computer software takes many forms. In one form, deductive synthesis, a program is developed from a formal specification. The specification is given in first-order logic in the form "i$o(P0 Pn), where i is a set of inputs, o is a set of outputs, and the Pis are propositions relating inputs to outputs. A proof of this conjecture is conducted in classical logic but is restricted to be constructive. Not only do we prove that the required o exists, but we must also indicate how it is constructed. This gives the basis for constructing a computer program from the proof.
Amphion is a general purpose, deductive, program synthesis system that facilitates reuse of domain-oriented software libraries. It assists a user in constructing the statement of a problem in an abstract, domain-oriented vocabulary using a graphical notation. Amphion automatically generates a program that implements a solution to the problem specification. The generated program consists of assignment statements and calls to subroutines from the software library. It takes significantly less time for an experienced user to develop a problem specification with Amphion than to manually generate and debug a program. More importantly, a novice user does not need to learn the details of the components in the library before using Amphion to create useful programs. This removes a significant barrier to the use of software libraries.
Amphion/NAIF, the most mature of the Amphion applications, has generated programs that are in use by space scientists, including programs that perform geometry calculations and construct animations to assist in planning for the Cassini mission to Saturn. In this talk I will introduce Amphion and discuss several areas of active work based on the Amphion system.