The research proposed here addresses the mechanization or sortware specification; specifically, the construction or formal specifications from a general, domain-independent, implementation independent language. The current non-mechanized development or such specifications presents several problems:

Completeness

The large amount of low level detail necessary in a formal specification makes completeness a signicant problem.

Consistency

The development (creation, refinement, modi6cation) or a formal specification must adhere to certain consistency constraints, which are often difficult to maintain manually.

Mundane details

During the development of a specification, the user must be concerned with both high level strategic decisions and the low level manipulations necessary to implement them.

Integration

The integration of automated software tools relies on a common data base that contains a rationalized history or the development process. A non-mechanized specification process makes no contribu­tion to this data base. That is, the development or the specification is done outside or the computer (except for the lowest level editing steps) leaving the process informal and undocumented.

The goal or this research is to address each of these specification problems: completeness, consistency, automation of details, and documentation and integration. The research will build on two prior efforts in the area of mechanization of soltware development: 1) the formal specification language Gist, and 2) Glitter, a system for automating the transformational development or software. The general approach centers on two keys ideas: 1) the effort expended in constructing a complete, consistent formal specification can be at least partially reused, 2) development steps can be mechanized, and hence automated and documented.