最近，我的朋友Lars Hupel和我讨论了为什么正式的方法不合作。您可以在此阅读对话。我们主要集中在编写正式验证的代码。我想更多地谈论组合规范的困难。这是一半，因为有趣的原因很难，因为这是来自初学者的常见问题。
初学者到正式规范期望规范应该组织如程序：通过公共接口交互的多个独立模块，其中模块不知道彼此的私有实现。这比单个巨型计划更清晰可辨。我们可以测试各个模块，然后只需要担心它们如何结合。相比之下，大多数规范都被写为单个全局规范，子组件从每个规范从头开始重写。为什么我们不能将我们的规范作为可兼容作为程序？
规格是数学表达式，通常是逻辑的分支。我们使用数学来指定，因为它是精确的，明确和表现力的。该规范表示系统及其可能的行为。规范具有属性，系统所有行为的语句。在许多情况下，我们开始了解我们希望我们的系统拥有的属性，然后写下规范以满足它们。
我将定义编写两个规范，以便以保留两个规范的所有属性的方式加入它们，而无需我们将“挖掘”到任一规范。这里的良好直觉是函数组成：如果f（x）有类型签名a - ＆gt; b和g（x）具有型号b - ＆gt; C，然后g。 f = g（f（x））有类型签名a - ＆gt; C。我们知道g。 F保留类型安全而不知道任一函数内部的内容，只是顶级类型签名。优选地，编写规范应该相同的方式工作：我们不需要更改任一规格的内部，以组合两者。
即使没有“完美”的组成，我们也可以具有“光谱”的可组合性。让我们说一个规格由三个“组件”组成。如果我们只需要更改一个组件以将其与另一个规范相结合，那就比我们需要更改两个组件，“更多”可编译。这更符合我们如何考虑撰写撰写计划。我们可能需要修改界面或在导入周围写一个包装器，但每个模块的内部实现保持不变。
让我们在线性时间逻辑写下我们的规格。在“正常”逻辑中，语句X表示X是真的。在时间逻辑中，x表示初始状态下x为真。在未来的状态下，X不需要真实。要描述系统如何发展，我们添加了三个时间运算符：
NE XT（◯）：◯x表示下一个状态下x为真。
最终（◇）：◇x表示x在某个未来状态下是真的。 全局（□）：□x表示所有未来州的X是真的。 1 “未来国家”包括当前国家。 ◇X是真的，如果x在此状态或以后的状态下是真的。 在所有情况下，我将写“x是真的”，因为x和“x是假”的！x。 所有变量都是Booleans。 让我们举个例子。 X＆amp;＆amp; ◯！x表示X在初始状态下为真，在下一个状态下为false。 X＆amp;＆amp; ◯（！x＆amp;＆amp;◯□x）意味着x最初为true，然后在下一个状态x中是假的，并且在状态后永久呈现。 我们也可以写x＆amp;＆amp; ◯！x＆amp;＆amp; ◯◯□x，这意味着同样的事情。 ◯分发＆amp;＆amp; 和||，□仅分发＆amp;＆amp; 和◇结束||。 出于本次讨论的目的，我们将使用“闪烁器”：
initx = x || ！xblinkx =（x =＆gt;◯！x）＆amp;＆amp; （！x =＆gt;◯x）specx = initx＆amp;＆amp; □Blinkx.
p =＆gt; Q表示如果p是真的，则q为真。所以（x =＆gt;◯！x）意味着如果x现在是真的，那么在下一个状态下，x不是真的。
Specx也是一个布尔公式。这让我们选择任何任意程序行为，并询问SPECX是否为此，即SPECX是其行为的准确描述。它还意味着我们可以像任何其他逻辑陈述一样操纵它。
此规范的一个属性是x始终是真或假的，绝不是任何其他值。 2
specx =＆gt; TypeInVariantx意味着如果Sypex的specx为true - 也就是说，specx是其行为的准确描述 - 然后typeInvariantx也是如此。换句话说，满足specx的任何系统也具有属性TypeInvariantx。
我们将定义一个类似规格的规范，除了它描述了不同的变量之外。 3我们想现在模拟一个具有两个闪光器的系统。这样做的“显而易见”的方式是撰写Specx和Specy，而不是从头开始。到底能有多糟糕？
这将保证两个规范的所有属性都满足。究竟有四种有效行为：
x，y; ！x，！y; x，y ... x，！y; ！x，y; X，！Y ......！X，Y; x，！y; ！x，y ...！x，！y; x，y; ！x，！y ...
两个闪烁器始终同步。一个不能比另一个更快地运行，或者一直眨眼比另一个略要眨眼等。这很少在我们编写规格时我们想要的;考虑与一般工人流程组成心跳协议。一个人应该比另一个更频繁地运行。
我们可以使用可达性属性正式表达此功能：始终可以从任何其他状态达到给定状态。由于没有办法达到X＆amp;＆amp; ！y来自起始状态x＆amp;＆amp; Y，我们的系统不满足可达性属性R（X＆amp;＆amp; y）。
LTL不能正式表达可达性性质。这是使其他（可争议的更有用）特性表达的价格。
我们希望说一个或另一个可以运行。我们可以尝试写这个：
但这实际上并不是我们想要的。这也将使其中一个初始谓词是可选的：我们希望他们两个都是真的。我们只想要||眨眼谓词。我们已经丢失了简单的组合，因为我们需要将规范谓词恢复到他们的子组件中。这样我们可以写
这仍然看起来像“部分”的组成，只要我们的规格是init＆amp;＆amp; □p。但实际上是构成，它还应该保留本地规范的性质。
specx的一个属性是typeInvariantx，即□（x ||！x）。 spec也满足TypeInvariantx吗？
x到x =＆＃34之间的步骤;辣椒粉＆＃34;在blinkx下不是有效的，因此specx不是一个有效的步骤。但规范改为有□（blinkx || blinky），如果blinky是真的，则Blinkx可能是假的。这被称为帧问题。由于Blinky在其“帧”中没有X，因此它不会将X限制为明智的值。
Smarex =（x =＆gt;◯x）＆amp;＆amp; （！x =＆gt;◯！x）spec = initxspec =（initx＆amp;＆amp;＆amp;＆amp;＆amp;＆amp; □（（BLINKX＆amp;＆amp; smary）||（Blinky＆amp; smarx））
我们现在排除了Blinkx和Blinky发生的情况;两个闪烁器无法同步。让我们留下来，现在专注于不同的问题。在我们的原始规范中，我们知道至少有一个点x为真，至少有一个点x是假的。这些属性，即系统被保证最终做我们想要的东西，称为活动属性。
问题是我们只能在Specx中做“一件事”，而在规范中我们可以做两件事中的一个。如果我们继续选择Blinky AD Infinitum，Blinkx从未发生过，X永远不会改变。我们在这里说Blinkx是不公平的：即使它可能发生，它也没有保证发生。我在这里更详细地介绍了公平性。
我们可以通过说“blinkx发生无限的次数”来解决这个问题，AKA“Blinkx总是发生在未来的一点：”
spec =（initx＆amp;＆amp;＆amp;＆amp; □（（Blinkx＆amp;＆amp; sermy）||（Blinky＆amp; smerx））＆amp;＆amp; □◇Blinkx＆amp;＆amp; □◇Blinky
更详细地解释：□◇Blinkx说◇Blinkx总是如此。所以一旦Blinkx发生，◇Blinkx仍然总是如此，这意味着Blinkx必须再次发生在未来。所以我们有一个无限的次。
这不是一个准确的公平表示，因为它缺乏条件性。如果有什么东西可以防止BlinkX发生，我们不应该要求它不确定发生。我在公平帖子中更详细地掩盖了这一点。
我们现在有财产可携带性吗？ SPEC保证一切SPECX吗？好吧，没有。这是Specx的属性：
如果x为true，则在下一个状态下将是假的。由于规范是异步的，我们可以在x为true的行中有两个步骤。
我们撞了一堵墙。 specx需要x来改变每一步，而spec只需要它更改一些步骤。使用◯的属性将破裂。没有办法。这是一个基本问题，允许以不同的速率运行的规范。
如果我们禁止属性，构图会更容易吗？我们可以通过介绍口吃：步骤没有变化的步骤。如果我们可以在不打破规范的情况下在行为中的任何位置插入口吃步骤，我们会说一个规格是不变的。重写specx是feattute - 不变的：
作为简化，我将借用TLA +的盒子表示法：[P] _x相当于“P或STUTT”，AKA P ||不变的x。
我们现在不能拥有任何◯属性。任何关于如何通过口吃的值更改如何更改的财产，AKA不会更改值。此外，默认情况下，规格现在是不公平的。 Blinkx并不能保证发生，因为我们可以口吃无限的次数。我们也必须将其添加到规范中：
这将公平的问题推动到个人规范的编制规范。这给了我们一些合成性的。写作specx＆amp;＆amp; Compy携带每个本地规范的公平性质;如果单个规范是公平的，那么组成的规格也是如此。
这也允许每个规范具有“时间流动”。以下是具有口吃步骤的Specx的一些新行为：
X; ; ！X; ; X; ; ！xx; ; ; ！X; ; ; xx; ！X; ; ; ; ; X
通过口吃步骤，我们可以说，前两个行为代表以不同的速率运行的闪光灯，第三个行为代表一个滞后的闪烁。这自然向我们提供了不同的时间流量的不同规格。较慢的规格只是陷阱更多。
一旦我们制作Specx和Specyy Sturte Invariant，这里就是我们如何编写规格：
通过模态逻辑规则，□（A＆amp; b）=□A＆amp;＆amp; □B
我们已经回来了兼容性！这甚至允许同步和异步闪烁。我们刚刚失去了界限性质，并显着限制了我们的表现力。 h
通常，我们可以将任意数量的口吃不变规范组成，并保留所有个人属性......只要它们是独立的规格。闪光灯不共享任何变量。我们想要撰写共享某些状态的规范的大部分时间，例如共享队列的读者规范和编写器规范。这使得构成显着更加困难。
让我们拍摄闪光灯并添加标志。我们还将以不同方式与其互动。 Specx会在关闭时翻转它，而Spey会在它上面推迟。
在（f）=！f＆amp;＆amp; ◯foff（f）= f＆amp;＆amp; ◯！finitx（f）=（x ||！x）＆amp;＆amp; （f ||！f）重要（f）=（y ||！y）＆amp;＆amp; （f ||！f）nextx（f）= blinkx＆amp;＆amp; （on（f）||（f＆amp;＆amp;◯f））nexty（f）= blinky＆amp;＆amp; （关闭（f）||（！f＆amp;＆amp;◯！f））specx（f）= initx（f）＆amp;＆amp; □[nextx（f）] _ fxspecy（f）= inity（f）＆amp;＆amp; □[nexty（f）] _ fy
我们在f：f上的参数化specx现在是我们可以传入行为的变量。如果我们将F传入两个规格，他们将共享变量。 4将其视为通过引用，不通过参数。
我们必须确保F在NextX的每个步骤中完全定义F，否则我们可以设置F =＆＃34;辣椒粉＆＃34;当编写规范时，我们需要为每一步定义每个变量的下一个状态。
让我们说我们的初始状态是！x，！y，！z。当我们闪烁x时会发生什么？
[nextx（z）] _ zx和[nexty（z）] _ zy需要是真的。闪烁x，nextx（z）是真的（我们不吃）。
由于z开始了false和nextx（z）是真的，因此（z）是真的，我们有◯z。
对于nexty（z）是真的，我们必须有◯！z。但是（2）我们有◯z，所以nexty（z）是假的。
这意味着对于[nexty（z）] _zy是真的，我们需要口吃：y和z不变。
但（2）改变z。如果nextx（z）为true，则z必须更改，并且z不得更改。
通过在两个规范之间共享标志，我们将永久禁用其中一个。问题是每个规范都需要完全描述其所有组件变量的行为，这意味着所作规范只能做出与所有这些的更改。
这甚至是一种良好的依赖性规范，因为麻烦是本地化的共享变量。你可以想象一个y的价值是什么“块”痣和力量口吃。然后，即使specx会以与纳西多的方式改变z，也可以使用纳克西，名表和力z保持不变。我们有一个僵局。
最终，我们必须放弃自动组成，然后返回手动缝合规格。
Next =（NextX（Z）＆amp;相同（Y））|| （Nexty（z）＆amp;＆amp;相同（x））spec = initx＆amp;＆amp; ＆amp;＆amp; □[下一个] _xyz
这也迫使规范总是是异步，并要求我们再次手动地写下公平要求，但至少它是有效的。
撰写规范很难，因为规范需要完全描述其变量如何变化，而组件规格不知道彼此的变量。如果他们这样做，他们可能希望以不兼容的方式更改它。我们可以通过手动将规范集成在一起，但随后我们没有撰写规范，因为我们需要检查每个规范的内部结构。这并不意味着组合规范需要本质上很难：我们可以提出新技术来帮助它们在一起。但这意味着社区中的偏好是写入大全球规范，而不是将较小的规格组合在一起。
“最终”和“全球”术语更普遍称为“有时”和“总是”。所有时间逻辑都是模态逻辑，这是◇和□符号来自的地方。 ◯，据我所知，LTL是独一无二的。 [返回]
我知道我说这里的所有变量都是布尔值，但这只是我在这里关注的一般性。没有什么能阻止我的规格中的数量和字符串，我现在就没有了。稍后这将变得更加重要。 [返回]
我可以制作initx和blinkx采取参数，然后写规格（y）而不是specyy。这是指定时的标准实践，但我硬编码了两个规范，以简化解释。我们将在后面的部分中包含参数化。 [返回]
我们如何知道我们通过一个变量而不是常量或价值？ 在实践中，我们明确声明了我们规范中的变量。 specx的文件可能看起来像vars x，f; specx（f）。 [返回]