在工作中使用正式方法

一些人告诉我，他们享受了学习的正式方法，但并不确定如何实际使用它。他们主要在工作中进行短暂的冲刺，并没有从头开始构建新系统。这告诉我有一些关于使规范有用的东西的困惑，并且我们需要在实践中应用它们的资源。这是一个简短的指南，以便以初学者访问的方式在工作中使用规范，适用于许多上下文，并提供实力业务价值。

我必须在这里制作一个主要免责声明：我教正式的方法是为了生活的讲习班。这使我在正式方法上写的一切至少是一点点的广告。我宁愿站在前面，所以你知道你正在进入什么。

如果这是您的第一次遇到正式方法，您可能对我的历史和局限性的文章更感兴趣，或者我对其实际应用的谈话。

我在这里使用正式规格来表达您可以表达高级属性的语言，但正式化，您可以为其进行计算机检查它们。这包括tla +等语言， 合金 和事件 - B，并排除如CoQ，决策表和粗眼的东西。 1

这一切都假定您正在编写“典型的”业务或基础设施系统，无论这是什么意思。有量的小错误是容忍的，但要避免重大错误。这些是粗略的拇指规则，以记住你的规格。酌情打破它们。

考虑收到消息并与之执行某些消息的组件。如果消息有问题，不成熟，交付错误，任何事情，我们都做了别的事情。错误检查，格式化，审核，一切都可以是整个子系统，但如果不是我们关心的那个我们可以将它全部折叠成如此：

这对应于“每条消息都很好”，“每条消息都很好”，“前十条消息很糟糕，其余的好的”等。这些都是规范中的所有有效路径，就像它们都能发生在真实中系统。当我对其运行模型检查器时，它将检查所有这些。

规格无需描述系统的总行为。如果您的系统执行A，B和C，则写入三种不同的规格通常会更快，每个规格都假定两个组件已经正常工作。第四个规范可能会展示所有三个交互，但与每个组件的细节更少，而不是专门规范。

这并不会给您带上一切的详细信息，但它有很多好处。首先，每个部分规范都可以关注您对该组件关注的内容。其次，您可以使用每个部分规格而无需整个系统;这更早是有用的。第三，IT模型需要更快地检查。四，编写规格比写独立规格更难，您通常必须“削弱”一种规格，以轻松剥离组成。 2

前两个的推论。高级规格可以是比实际代码小的数量级。

您投资编写规格的时间越多，它就越全面。但是 - 与一切一样 - 回报率递减。它需要更多的工作来从95％右转到99％，比率从85％到95％。我住在那个最大回报的区域，纯粹是因为它是大多数人最可靠和务实的。在这种情况下，在这种情况下不会让您的软件无窃听，但它将使得其质量远远高于对其进行投射的。

大多数正式的规范语言不能自动精制：您无法轻松验证您的代码行匹配规范。在某些方面，这是一个问题，但它也有一个令人惊讶的好处：除了你的代码之外，规格也不存在，而不是依赖性。这意味着尝试规格，与尝试新语言不同，不带有技术债务的风险或增加任何维护负担。您也不必更改代码以使编写规范成为可能。这一切都降低了FM试验的摩擦。比尝试新的监视器设置更难，但比将Elixir添加到您的技术堆栈或让您的同事才能配对程序。

系统错误有两种：实现错误和设计错误。测试很好地显示您的代码匹配您的期望，但对您的期望符合您的需求非常糟糕。规格是相反的。你需要两者。规格也不是文档，代码审查，代码静态分析或发布后分析。它可能会更容易完成所有这些，但它不会消除对它们的需求。

有些情况下，规格可以消除对代码测试的需要，但是这种规范更难在更专业的域中编写和有用。

（3）是最独特的好处，可以说是提供最明显的商业价值的好处。但所有这些都是非常有价值的。开始应用规格的最简单方法主要是给您（1）和（2）。由于人们没有注意到这些利益，因此他们认为他们必须潜入深渊以获得任何用尽规格。

以下项目采用努力/技能的升序顺序。这是一个粗略的指导，而不是一个课程计划：不觉得有义务以“练习”或任何东西都这样做。您可以使用它来弄清楚您最舒适的位置，以及您最舒适的进步。这也不是有用的升序。甚至记录自己的系统也非常有用。

拿一个你有一段时间的系统，你认为你很好地了解。编写架构的高级规范或其一些功能。不要担心编写规格，只需写出各种兴趣点的断开连接的型号。您不一定正在寻找架构中的错误;目标是让实践练习撰写规格。如果您的规格显示在现有系统中没有看到的行为，则通常是您在编写规范中犯了错误的标志。

通常。您也可能误解了系统的某些方面。这很有用，但不确定性（是翻译错误或理解错误？）可能对提高您的建模技能可能并不重要。这就是为什么你记录一个系统你知道的系统。它只隔离建模实践。

您也有机会犯有任何错误，并且系统实际上是一个微妙的问题。这比你期望的频率更大。我会说如果你刚刚开始仍然考虑这种可能性，而且不是为了使你的第一次假设。

在这样做的同时，专注于您的学习FM，它仍然为商业案例产生足够的有形益处。首先，您拥有系统的规范，具有严格陈述的假设，行为和要求。我发现这在向其他工程师解释某些东西时，这使得补充了一个很好的文档补充。此外，如果您稍后需要修改系统，则已完成模型部分。

采用您修复了复杂错误的系统。编写一个匹配系统破碎版本的模型，并显示它捕获相同的错误。这为您提供了写作不变性的良好练习。它还可以帮助您找到现有系统的不变性：BUG违反的最薄弱的属性是什么？

还有一个难题的理由，也是如此：它很好地展示了写作规范的价值。如果您有关于出现错误的数据以及查找错误需要多长时间，您可以显示“在生产中捕获此错误”和“在模型中捕获此错误”之间的时间差。差异很可能是“几周”与半小时相比的东西。

使用观察到的错误拍摄现有系统，并写出具有错误的模型。这与showcasing一个错误不同，因为您没有实际本地化或修复它的错误。规范的目的是让它更容易找到错误。如果您可以在模型中准确地重现它，它将向您展示导致错误的一系列步骤。然后，您可以确定在规范中开始侧向的位置，并使用它来定向代码本身中的错误。

如果您无法重现错误，则可能会从几个常见的原因中。一个是规范可能太高。您可能会抽象正确处理正确处理，但实际上会错过错误情况。另一个是这个错误可能是一个滑块：你有一些实施细节错误。想想写作合并（f，g）而不是合并（g，f），以错误的顺序放置两行等。这些都是容易潜入规格的所有问题。规格在设计中的漏洞中更好，或者当设计有“正确”但意外行为时。

有时由于模型检查器，您会发现错误。但是，在许多情况下，规范使得错误“显而易见”。在10行的规格中看到比在1,000行代码中更容易。这导致了与正式规格的共同初学者挫折，在完成模型之前已经弄清楚了。这实际上是规范的大益处之一：大多数模型检查都可能发生在你的头脑中。

我工作的一个例子：为什么不是杀手切换工作？经过几天的几天毫不含糊地试图跟踪它，我写了一个规格并立即走了“哦，杀手 - 交换机阻止了我们遏制了工作，没有处理它们。”在规范中显而易见，在Codebase中少得多。

采取您想要更好地了解的系统并为它写模型。规格错误更有可能意味着您误解了某种东西，而不是为您自己的系统意味着的错误。但是甚至在验证之前，写作规范将有助于帮助。您无法在规范中实际手中：您写的一切都必须精确且严谨。这会让奇迹理解一些事情。

它还提供了验证您的知识的好方法。您可以通过模型检查器运行并将其与真实系统的行为进行比较时，查看会发生什么。您还可以将模型显示为域专家，并查看它是否与其对系统的理解相匹配。 3如果没有，您有一个精确的方式来了解您的理解差异。

在我的经验中，您也更有可能通过模拟不熟悉的系统而不是熟悉的系统来找到关键的错误。我不知道为什么。无论您如何决定与某人带来错误，记得要尊重和善意。正如规格不替代测试，规格不替代社交技能。

采取系统，该系统的模型，以及新的要求或期望的变化。表明它不满足要求，然后在它确实之前修改模型。

至少在我的经历中，这最终是在项目上最常使用FM。由于规范高级别，大多数变化将映射到几行修改规范。在进行更改之前，兽医您认为的变化实际上是您想要的。这有助于您了解您正在做的事情。它还有助于查找错误，显示系统的小型变化如何传播到全局不变的违规状态。

您到达的另一个好处：写真理智 - 检查要求。如果我说“至少一个节点必须始终在线”，我的意思是“至少有一个节点在整个时间在线”或“在所有时间点，至少有一个节点在线”？ 4在编写规格时看到差异比keee-Deeple在码Base中的膝盖时，更容易得多。有时客户将能够澄清他们的意思，并且在极少数情况下，客户将意识到他们实际上并不知道他们想要什么。

使用规范从头开始制作新系统。或者，使用规范向系统添加显着的新功能。这需要编写规范的最多技能，并知道何时停止编写规范，但实际上并没有比建模现有系统更难。它还具有最激烈的好处，因为您从一开始就获得所有知识升高和模型检查。

在开始建立它之前，共同初学者错误试图在太多细节中模拟系统。请记住，规格是您的设计。有一个设计是非常有价值的，但这不是代码，您写的大部分代码都不会反映在设计中。对系统无关紧要您拥有的特定类或函数，只是存在他们产生的行为。

您可能注意到的大事之一：这些都是迭代的。在做一天的编码之前，您不会花几个星期和几个月写下详尽的规格。而且您并不盲目地在计划之后：如果现实介入您调整规范并查看后果的结果。规范是在有用于通过设计思考的能力放大，而不是强迫您在刚性路径上。

这里最大的差距是，这是基于个人的，而不是基于团队的。 Enterprise FM仍然是一种练习，因此我们没有关于它如何适应更大的团队工作流程的扎实信息。有一些不同的公司更广泛地采用FM，我很高兴看到它是如何为他们工作的。

有一些项目，详尽的规格有意义。我们大多数人都没有这样做。有一些项目根本没有意义。我们大多数人都没有这样做。我们在某种形式的规格有助于很多的甜蜜点，但绝大多数我们都不使用它。

但是一些使用的东西的一部分是何时适用。因此，制作规格有用，我们也应该知道它们的时间。

当它不值得书写规范时，您不会写规格。当然，这是通函，我们对什么不值得书写规范更感兴趣。实际上有两个方面是这个问题：什么时候不能编写规格，并且当不向现有规范添加更多较低级别的细节时。两者都是由相同的约束驱动。

有一些东西使规格不太有用。即使这些持有，仍然可能是值得的，但你可能会投入更少的时间和努力。此外，这对我的经验偏见了规格：可以在那里有语言对这些问题有好处。

如果出现错误，很明显，易于隔离，并导致一些问题。这并不意味着您不想要错误，这意味着您可以快速找到并修复它们。一个示例是一个批处理作业，它看起来低量的数据并构建一个报告：大多数错误都会在生产中显而易见的错误，并且一旦您修复它，您就可以轻松地重新运行旧数据。理想情况下。规格仍然可以帮助这里，但它们的正确性效益不太有价值。

并非所有代码都是一些抽象设计的投影。有时，基本理念位于代码级别，在这种情况下，规格缺少森林的树木。

很多颈部和数据管道都是这样的。拍摄一个击中十个API的程序，提取信息并将其拼接在一起。那里有一些更高级别的设计，错误处理和重试行为和所有，但大多数工作都在于原始数据的实现级转换。设计规格太远了，从中取消了很多帮助;你想要一些更近的​​东西。

任何类型的数值计算都是正确的。大多数规格语言都可以表达整数，但很少有可能模拟 - 检查它们。我看到的唯一工具可以处理任何类型的实数是棱镜，它有......其他问题。 5您将不会在设计级别验证您的数学运算。

随着敏捷的民间喜欢说，了解人们需要的最佳方式是看他们如何与现有系统互动。但这并不一定意味着系统必须完整：通常是原型就足够了。需求经常变化，我们对早期阶段所需的了解通常是最小的。系统可能不应该有一些属性，例如“随机崩溃”或“爆炸”。但这些不是原型的必需属性！如果一个人使用系统来了解他们想要的系统，那么系统“工作”的重要性不太重要。我们正在收集数据。

从某种意义上说，原型在这个阶段取代了规范的位置：您可以在迭代原型以查找客户端问题的规范中迭代。

这个比其他人更乱。我的一个软件信念是，大多数程序都是写入自动化的东西，所以人类没有对它做的，或者增加一个人，所以他们可以做得更好。 Graydon Hoare称之为批处理和交互式计算之间的差异。两者之间的线路没有清除：是一个计算器，自动化死记硬背计算或增加您的计算能力吗？一点两人，真的。但我仍然找到这个有用的模型。

在我的经验中，对自动化的规格比增强更有用。在自动化中，人类可能会开始它但是之后不一定做任何事情，因此它更重要的是它满足不变性。增强代码在循环中不断地具有人类，谁可以调整系统和自我正确。

好的，你已经读过这一点，时间的时间。正式方法是一个非常强大的工具。在我看来，使用它们的最大障碍是教育。 FM需要不同的思维思想，有时人们有困难构建直觉。还有一个含有隐含的数学技能集，很容易学习，但很难意识到您需要学习。我写了一本书来帮助人们，但没有任何经验丰富的老师则没有任何措施。

您可以聘请我做公司研讨会，或向您公司人员提供1-ON-1培训。我有客户通过写作规格，每年节省六位数节省，因为您节省了金钱写作测试。您可以在此与我联系或在此处阅读更多关于我的服务。

非常简单：CoQ更多用于验证代码而不是设计，这是一个更专业的域名。决策表是Flyweight方法：易于学习和使用，适用于聚焦，狭窄的上下文。 gherkin是非正式和代码级，而不是设计级别。 [返回]

这有很多原因。一个是框架问题：X没有说y的规范中的值和反之亦然的结果，所以组成的规范是没有定义的，除非你仔细定义它们的编写方式。 [返回]

当然，这需要他们了解规范语言。但是我发现了如果您通过规格漫步，您可以完全解释他们需要相对较快的信息。学习读取规格比学习写给它们更容易。 [返回]

更正式地，这是∃n∈节点之间的区别：□在线（n）和□∃n∈节点：在线（n）。 [返回]

喜欢缺少数组。和字符串。和功能。棱镜是一个有趣但极其利益的建模语言。 [返回]