A Study of the Specification of Large Programs

点击翻译按钮获取中文摘要

The objectives of this project are: to define a model of a specification of large programs, and to design a language useful for writing specifications of large programs. Toward the long-term goal of putting formal specifications to productive use, the ability to specify large programs is needed, not just small ones. It is intended to study behavioral properties of large programs, and how to specify these properties; relationships among program module specifications that constitute specifications of large programs; and language constructs that facilitate putting together specifications. It is planned to use formal mathematics to define the model and language. The research will simultaneously be guided by more practical objectives: to develop a specification approach, and to demonstrate the utility of the work by applying it to realistic examples.