There is now widespread agreement that precise specifications can play an important role in software development and maintenance. It is less clear that formal specification, as opposed to precise informal specifications, are worth the extra effort required to create them. Proponents of formal specifications have argued that their susceptibility to machine analysis and manipulation increases their value and reduces their cost. This project is trying to support this claim by building and using tools that aid in the construction of formal specifications for programs and program modules. The specification languages that have been used permit significant assertions about logical properties of specifications--properties related to consistency, completeness, and module independence--to be made. Experience in hand checking specifications has lead to the conviction that such assertions are useful in establishing the validity of a specification. Unfortunately, these assertions cannot be checked completely by machine because they are all undecidable in the general case. Hence, this project will: do the theoretical work necessary to design useful approximations to these checks; implement a specification system that incorporates these approximations, building upon an existing syntax-directed editor and term-rewriting laboratory; evaluate these tools by using them to write specifications; and report on this experience, paying particular attention to the merits of formal vs. precise informal, and definitional vs. operational, specifications.
