补充资料：形式规约

形式规约
formal specification

x ingshi guiyue形式规约(fo~1 51冲cification)用具有坚实数学基础的语言和方法给出的软件的功能描述。软件的规约既指对最终产品的功能描述、实时特性、运行效率及安装与运行的时空要求等等，也指对开发过程的各种要求，比如交货期限、工程预算等等。它是软件设计与研制工作的出发点，也是衡量最终产品是否合格的依据。形式规约只关心软件产品的功能性质，即“做什么”，而不关心其功能是怎样实现的。 形式规约的最主要特点是具有严格的数学基础，因此有可能讨论它的一致性与完备性等性质。一致性指的是自身无矛盾，这是任何规约都应满足的基本要求。自相矛盾的规约在理论上是没有意义的，在实践上是有害的。因为它将导致人力与财力的浪费。完备性是指规约是否完全、无遗漏地刻画了它所要描述的对象。完备的规约具有许多良好的性质，比如语义模型的唯一性等。 形式规约的一个重要应用是程序正确性验证。只要所用的编程语言同样具有严格的数学语义，就可以形式地论证程序是否满足所给的规约。如果满足，就说明程序具有规约所刻画的性质。也就是说，程序相对于该规约是正确的。验证程序的正确性需要进行大量的推理和计算，因此出现了许多支持程序正确性验证的软件工具，即程序证明器。这些工具既有自动的，也有交互式的。按所依据的数学理论，形式规约可以分为基于集合论的，基于逻辑的与基于代数的;按所适用的程序类，又可以分为面向顺序程序的与面向并发程序的。以下对常用的形式规约方法作简要的介绍。 前后断言方法可以说是最早的形式规约方法，出现于60年代后期，首倡者是C.A.R.H匕盯e。其基本思想是在程序语句间插人刻画程序状态(即程序变量的取值)的一阶谓词公式，称为断言。插在语句之前的断言指明执行此语句之前程序变量所应具有的性质，称为前断言;插在语句之后的断言则刻画了语句执行结束时的程序状态空间，称为后断言。后断言可以看作是对程序所应实现的任务的描述;前断言则可看作是正确执行程序的前提。一对前、后断言即是对程序的规约。如果用S，P和Q分别表示程序、前断言和后断言，则程序S满足由P，Q组成的规约这一事实可用三元组P{S}Q来表示。C，A.R.H阳r日是出了一套公理系统用于推导这样的三元组，如果P{S}Q可由该系统推出，则S就是相对于P，Q正确的。考虑到程序是否终止，这种正确性又可分为部分正确性与完全正确性两类。 形式规约是对程序“做什么”的数学描述，这种描述主要体现在后断言中，因此后断言往往包含了关于程序结构的重要信息。基于这种认识，E.W.伪地tra提出了一个推导正确程序的形式系统，称为录肠贡里条件演算。

说明：补充资料仅用于学习参考，请勿用于其它任何用途。