形式化规范

在计算机科学中，形式化规范是基于数学的技术，其目的是为了帮助系统和软件的实现。它们被用来描述一个系统，分析它的行为，并通过严格和有效的推理工具验证感兴趣的关键属性来帮助其设计。这些规范是正式的，因为它们有一个语法，它们的语义属于一个领域，并且它们能够被用来推断有用的信息。

在每一个过去的十年中，计算机系统变得越来越强大，因此，它们对社会的影响也越来越大。正因为如此，我们需要更好的技术来帮助设计和实现可靠的软件。已有的工程学科使用数学分析作为创建和验证产品设计的基础。形式化的规范是在软件工程可靠性中实现这种曾经预言的方式之一。其他方法，如测试，更常用于提高代码质量。

给予这样的规范，就有可能使用形式化验证技术来证明系统设计相对于其规范是正确的。这使得不正确的系统设计可以在实际实施的任何重大投资之前被修改。另一种方法是使用可能正确的细化步骤来将规范转化为设计，而设计最终会被转化为一个构造正确的实现。值得注意的是，正式的规范不是一个实现，而是可以用来开发一个实现。形式化规范描述了一个系统应该做什么，而不是系统应该如何做。一个好的规范必须具有以下一些属性：充分的、内部一致的、不含糊的、完整的、满意的、最小的一个好的规范将具有。可构建性、可管理性和可进化性可用性可交流性强大而有效的分析对形式化规范感兴趣的主要原因之一是，它们将提供一种对软件实现进行证明的能力。这些证明可以用来验证一个规范，验证设计的正确性，或者证明一个程序满足规范。

一个设计（或实现）不能单独被宣布为"正确"。它只能是"相对于一个给定的规范而言是正确的"。形式化的规范是否正确描述了要解决的问题是一个单独的问题。这也是一个难以解决的问题，因为它最终涉及到构建非正式具体问题域的抽象形式化表示的问题，而这样的抽象步骤是无法进行形式化证明的。然而，通过证明有关规范预期表现的属性的"挑战"定理来验证一个规范是可能的。如果正确的话，这些定理会加强规范制定者对规范的理解以及它与基本问题领域的关系。如果不正确，规范可能需要改变，以更好地反映那些参与制作（和实现）规范的人的领域理解。软件开发的形式化方法在工业界并没有被广泛使用。大多数公司认为在他们的软件开发过程中应用这些方法是不经济的。这可能是由于各种原因，其中一些是。

初始启动成本高，可衡量的回报低灵活性很多软件公司使用注重灵活性的敏捷方法。对整个系统进行正式的规范往往被认为是灵活性的反面。然而，有一些研究表明在敏捷开发中使用形式化规范的好处复杂性它们需要高水平的数学专业知识和分析技能来有效地理解和应用它们解决这个问题的方法是开发工具和模型，使这些技术得以实施，但隐藏基础数学范围有限它们不能捕获项目中所有利益相关者感兴趣的属性它们不能很好地指定用户界面和用户交互不具成本效益这并不完全正确，通过将它们的使用限制在关键系统的核心部分，它们已被证明具有成本效益其他限制。

范例形式化规范技术在不同领域和不同规模上已经存在了相当长的时间。形式化规范的实现会因其试图建模的系统种类、应用方式以及在软件生命周期的哪个阶段被引入而有所不同。这些类型的模型可以分为以下几类