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.