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.