Automated Semantic Analysis of Formal Specifications

精确的规格说明在软件开发和维护中扮演着重要的角色，这一点现在得到了广泛的认同。相对于精确的非正式规范来说，正式规范是否值得花费额外的精力去创建它们，这一点还不太清楚。正式规范的支持者认为，它们对机器分析和操作的敏感性增加了它们的价值，降低了它们的成本。本项目试图通过构建和使用工具来支持这一说法，这些工具有助于构建程序和程序模块的正式规范。所使用的规范语言允许对规范的逻辑属性（与一致性、完整性和模块独立性相关的属性）进行重要断言。手工检查规范的经验使我们确信，这样的断言对于建立规范的有效性是有用的。不幸的是，机器不能完全检查这些断言，因为它们在一般情况下都是不可确定的。因此，本项目将：做必要的理论工作来设计这些检查的有用近似值；在现有的语法导向编辑器和术语重写实验室的基础上，实现一个包含这些近似的规范系统；通过使用这些工具编写规范来评估它们；并报告这一经验，特别注意正式的与精确的非正式的，定义的与操作的，规格说明的优点。

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.