如果您不是在编写程序，请不要使用编程语言

Leslie Lampport是分布式计算基础工作的作者，您也可以通过La TeX中的字母La（“ Lamport TeX”）认识他。 这是他在1979年首次引入一致一致性的概念，他的文章“如何使多处理器计算机正确执行多进程程序”获得了Dijkstra奖（更准确地说，在2000年，该奖项以旧方式被称为：“ PODC有影响力论文奖” ”）。 维基百科上有一篇关于他的文章 ，您可以在其中找到一些更有趣的链接。 如果您热衷于解决事前发生的问题或拜占庭将军 （BFT）的问题，那么您应该了解兰珀特是所有这些背后的原因。

这种哈伯斯汀状态是莱斯利在2018年海德堡获奖者论坛上的报告的翻译。 演讲将重点讨论用于开发复杂和关键系统的正式方法，例如Rosetta空间探测器或Amazon Web Services引擎。 Leslie将在Hydra Conference上举行问答环节 ，查看此报告是必不可少的 -这种哈伯斯坦状态可以节省您一个小时的视频观看时间。 在此介绍完成之后，我们将这个词传递给了作者。

曾几何时，托尼·霍尔（Tony Hoar）写道：“每个大型程序都有一个小型程序，试图逃脱。” 我可以这样改写：“在每个大型程序中，都有一个试图逃脱的算法。” 但是，我不知道托尼是否会同意这种解释。

例如，以欧几里得算法为例，该算法可找到两个正整数的最大公约数 $$$（M，N）$ 。 在此算法中，我们分配 $$$x$ 价值 $$$M$ ， $$$N$ -价值 $$$y$ ，然后从最大值中减去其中的最小值，直到它们相等。 这些的含义 $$$x$ 和 $$$y$ 并将是最大的共同因素。 此算法与实现该算法的程序之间的本质区别是什么？ 在这样的程序中，会有很多底层的东西： $$$M$ 和 $$$N$ 会有某种类型， BigInteger或类似的东西； 有必要确定程序的行为，如果 $$$M$ 和 $$$N$ 非阳性 依此类推。 算法和程序之间没有明显的区别，但是在直观的层次上，我们感到有所不同-算法更加抽象，层次更高。 而且，正如我所说，每个程序中都有一个试图逃脱的算法。 通常这些不是算法课程中所介绍的算法。 通常，这是一种仅对特定程序有用的算法。 通常，它比书中描述的要复杂得多。 这种算法通常称为规范。 而且在大多数情况下，该算法无法奏效，因为程序员不会怀疑它的存在。 事实是，如果您的思维集中在代码，类型，异常， while循环等上，而不是数字的数学特性上， while无法看到该算法。 用这种方式编写的程序很难调试，因此在代码级别调试算法意味着什么。 调试工具旨在查找代码中的错误，而不是算法中的错误。 另外，这样的程序将无效，因为同样，您将在代码级别优化算法。

与几乎任何其他科学技术领域一样，这些问题可以通过数学描述来解决。 有很多方法可以做到这一点，我们将考虑其中最有用的方法。 它可以与顺序和并行（分布式）算法一起使用。 此方法包括将算法的执行描述为状态序列，将每个状态描述为对变量的属性分配。 例如，欧几里得算法被描述为以下状态的序列：首先，为x分配值M（数字12），而y为值N（数字18）。 然后，我们从较大的值中减去较小的值（ $$$x$ 来自 $$$y$ ），这将我们引向我们已经带走的下一个状态 $$$y$ 来自 $$$x$ ，算法的执行从此处停止： $$$[x \ leftarrow 12，\ leftarrow 18]，[x \ leftarrow 12，\ leftarrow 6]，[x \ leftarrow 6，\ leftarrow 6]$ 。

我们将状态行为序列和一对连续状态称为步骤。 然后，可以通过代表该算法所有可能变体的各种行为来描述任何算法。 对于每个特定的M和N，只有一个实施例，因此，一个行为集足以描述它。 更复杂的算法，尤其是并行算法，具有很多行为。

首先，通过状态的初始谓词来描述许多行为（谓词只是具有布尔值的函数）； 其次，是状态对的下一个状态的谓词。 一些行为 $$$s_1，s_2，s_3 ...$ 仅当初始谓词为true时，它才会进入许多行为 $$$s_1$ ，并且下一个状态的谓词对于每个步骤都是正确的 $$$（s_i，s_ {i + 1}）$ 。 让我们尝试以此方式描述欧几里得算法。 这里的初始谓词是： $$$（x = M）\土地（y = N）$ 。 下面的公式描述了状态对的下一状态的谓词：

请不要惊慌-里面只有六行；如果您按顺序进行操作，很容易弄清楚它们。 在此公式中，没有笔画的变量是指第一种状态，有笔画的变量是在第二种状态下的相同变量。

如您所见，第一行表示在第一种情况下，x在第一状态下大于y。 在逻辑与之后，指出第二状态下的x值等于第一状态下的x值减去第一状态下的y值。 在另一个逻辑与之后，说明第二状态下的y值等于第一状态下的y值。 所有这些意味着在x大于y的情况下，程序将从x中减去y，而y保持不变。 最后三行描述了y大于x的情况。 请注意，如果x等于y，则此公式为false。 在这种情况下，没有下一个状态，并且行为停止。

因此，我们仅用两个数学公式描述了欧几里得算法-我们不必弄乱任何编程语言。 还有什么比这两个公式更美丽的？ 用一个公式替换它们。 举止 $$$s_1，s_2，s_3 ...$ 仅在以下情况下执行欧几里德算法：

• $$$Init_E$ 适用于 $$$s_1$ ，
• $$$Next_E$ 每一步都是正确的 $$$（s_i，s_ {i + 1}）$ 。

可以将其写为行为的谓词（我们将其称为属性），如下所示。 第一个条件可以简单表示为 $$$Init_E$ 。 这意味着仅当行为对于第一个状态为true时，我们才将状态谓词解释为true。 第二个条件写为： $$$\正方形Next_E$ 。 平方表示状态对的谓词和行为的谓词之间的对应关系，即 $$$Next_E$ 对于行为的每一步都是如此。 结果，公式如下所示： $$$Init_E \ land \ square Next_E$ 。

因此，我们用数学方法编写了欧几里得算法。 从本质上讲，这些仅仅是定义或缩写， $$$Init_E$ 和 $$$Next_E$ 。 整个公式如下所示：

她不漂亮吗？ 不幸的是，对于科学技术而言，美丽并不是决定性的标准，但这确实意味着我们走在正确的道路上。

仅当满足我们刚刚描述的两个条件时，我们写下的属性才对某些行为成立。 在 $$$M = 12$ 和 $$$N = 18$ 对于以下行为，它们是正确的： $$$[x \ leftarrow 12，\ leftarrow 18]，[x \ leftarrow 12，\ leftarrow 6]，[x \ leftarrow 6，\ leftarrow 6]$ 。 但是对于相同行为的较短版本也满足以下条件： $$$[x \ leftarrow 12，\ leftarrow 18]，[x \ leftarrow 12，\ leftarrow 6]$ 。 我们不应该将它们考虑在内，因为这些只是我们已经考虑到的行为的单独步骤。 有一种明显的方法可以消除它们：简单地忽略行为，这种行为以至少可以进行下一步的状态结束。 但这不是正确的方法，我们需要一个更通用的解决方案。 此外，这种情况并不总是有效。

对这个问题的讨论使我们想到了安全性和活动性的概念。 安全属性指示哪些事件有效。 例如，允许算法返回正确的值。 活动属性指示哪些事件迟早应该发生。 例如，算法迟早应返回某个值。 对于欧几里得算法，安全性属性如下： $$$Init_E \ land \ square Next_E$ 。 必须向其中添加一个活动属性，以防止过早停止： $$$Init_E \ land \ square Next_E \ land L$ 。 在编程语言中，充其量只有一些原始的活动定义。 大多数情况下，甚至没有提到活动，这只是暗示程序的下一步必须进行。 要添加此属性，您需要一个相当复杂的代码。 从数学上讲，表达活动非常容易（为此只需一个正方形），但是不幸的是，我没有时间这样做-我们将不得不把讨论局限于安全性。

仅适用于数学家的一个小题外话：每个属性都是该属性为真的一组行为。 对于每组序列，都有以下距离函数创建的自然拓扑：

$$$s = 17，\ sqrt {2}，-2，\ pi，10，1/2 \\ t = 17，\ sqrt {2}，-2，e，10，1/$

这两个函数之间的距离是1/4，因为它们之间的第一个差异在第四个元素上。 因此，这些序列相同的部分越长，它们彼此越接近。 该功能本身并不是很有趣，但是却创建了一个非常有趣的拓扑。 在此拓扑中，安全属性是封闭集，活动属性是密集集。 在拓扑中，一个基本定理指出每个集合是一个封闭集合和一个密集集合的交集。 如果我们回想起属性是行为的集合，则根据该定理可以得出，每个属性都是安全属性和活动属性的结合。 这个结论对于程序员也将是有趣的。

部分正确意味着程序只有给出正确的答案才能停止。 欧几里得算法的部分正确性表示，如果完成执行，则 $$$x = GCD（M，N）$ 。 并且我们的算法完成了执行 $$$x = y$ 。 换句话说， $$$（x = y）\ Rightarrow（x = GCD（M，N））$ 。 该算法的部分正确性意味着该公式对于行为的所有状态都是正确的。 在其开头添加符号 $$$\平方$ 意思是“所有步骤”。 如您所见，公式中没有带笔触的变量，因此其真实性取决于每一步的第一个状态。 如果每个步骤的第一个状态都为真，则该语句对所有状态都为真。 欧几里得算法的部分正确性可以通过该算法可接受的任何行为来满足。 正如我们所看到的，只要给出的公式为真，就可以允许行为。 当我们说某个属性满足时，仅表示该属性来自某些公式。 那不是很好吗？ 这是：

$$$Init_E \ land \ square Next_E \ Rightarrow \ square（（x = y）\ Rightarrow（x = GCD（M，N）））$

我们转向不变性。 带方括号的正方形称为不变属性 ：

$$$Init_E \ land \ square Next_E \ Rightarrow \ color {red} {\ square（（x = y）\ Rightarrow（x = GCD（M，N）））}$

平方后放在方括号中的值称为不变式 ：

$$$Init_E \ land \ square Next_E \ Rightarrow \ square（\ color {red} {（x = y）\ Rightarrow（x = GCD（M，N））}）$

如何证明不变性？ 证明 $$$Init_E \ land \ square Next_E \ Rightarrow \ square I_E$ ，您需要证明任何行为 $$$s_1，s_2，s_3 ...$ 结果 $$$Init_E \ land \ square Next_E$ 是真理 $$$I_e$ 在任何情况下 $$$s_j$ 。 我们可以通过归纳证明，为此，我们需要证明以下内容：

1. 来自 $$$Init_E \ land \ square Next_E$ 因此 $$$I_e$ 对国家而言是正确的 $$$s_1$ ;
2. 来自 $$$Init_E \ land \ square Next_E$ 因此，如果 $$$I_e$ 对国家而言是正确的 $$$s_j$ 然后它也
   对国家而言是正确的 $$$s_ {j + 1}$ 。

首先我们需要证明 $$$Init_E$ 暗示 $$$I_e$ 。 因为公式声称 $$$Init_E$ 对于第一种状态为true，这意味着 $$$I_e$ 对于第一种状态为true。 此外，当 $$$Next_E$ 适用于任何步骤，并且 $$$I_e$ 忠实于 $$$s_j$ ， $$$I_e$ 适用于 $$$s_ {j + 1}$ 因为 $$$\正方形Next_E$ 意味着 $$$Next_E$ 适用于任何一对州。 这是这样写的： $$$Next_E \土地I_E \ Rightarrow I'_E$ 在哪里 $$$I'_E$ 那是吗 $$$I_e$ 对于所有带有笔画的变量。

满足我们刚刚证明的两个条件的不变式称为归纳不变式 。 部分正确性不是归纳的。 为了证明其不变性，您需要找到隐含它的归纳不变性。 在我们的例子中，归纳不变式如下： $$$GCD（x，y）= GCD（M，N）$ 。

算法的每个后续操作均取决于其当前状态，而不取决于过去的操作。 该算法满足安全性，因为其中包含了感应不变式。 欧几里得算法可以计算出最大的公分母（即直到达到它为止才停止） $$$GCD（x，y）= GCD（M，N）$ 。 要了解该算法，您需要了解其归纳不变性。 如果您研究过程序验证，那么您就会知道，刚刚给出的不变性的证明不过是证明顺序Floyd-Hoare程序的部分正确性的一种方法。 您可能还听说过Hoviki - Gris 方法 ，它是Floyd-Hoar方法对并行程序的扩展。 在这两种情况下，都使用程序注释编写归纳不变式。 而且，如果您借助数学而不是借助编程语言来执行此操作，则此操作非常简单。 这就是Hoviki Gris方法的核心所在。 数学使复杂的现象更易于理解，尽管现象本身当然不会变得更简单。

仔细看看公式。 如果在数学中我们写了一个带变量的公式 $$$x$ 和 $$$y$ ，这并不意味着其他变量不存在。 您可以添加另一个公式，其中 $$$y$ 相对于 $$$z$ ，它不会改变任何东西。 只是公式对其他任何变量都没有说明。 我已经说过，状态是变量的值赋值，现在您可以添加以下内容：从所有可能的变量开始 $$$x$ 和 $$$y$ 以伊朗人口为结尾。 我必须承认：当我说公式 $$$Init_E \ land \ square Next_E$ 我撒谎描述了欧几里得算法。 它实际上描述了一个宇宙，其中的意义 $$$x$ 和 $$$y$ 表示欧几里得算法的执行。 公式的第二部分（ $$$\正方形Next_E$ ）声称每一步都在变化 $$$x$ 或 $$$y$ 。 换句话说，它描述了一个宇宙，在这个宇宙中，只有意义改变了，伊朗人口才能改变 $$$x$ 或 $$$y$ 。 因此，在欧几里得算法执行完成之后，在伊朗没有人可以出生。 显然，事实并非如此。 如果我们有有效的步骤可以纠正此错误 $$$x$ 和 $$$y$ 保持不变。 因此，我们需要在公式中再增加一部分： $$$Init_E \ land \ square（Next_E \ lor（x'= x）\ land（y'= y））$ 。 为简便起见，我们将其编写为： $$$Init_E \ land \ square [Next_E] _ {<x，y>}$ 。 此公式描述了包含欧几里得算法的Universe。 必须对不变量的证明进行相同的更改：

• 我们证明： $$$Init_E \ land \ color {红色} {\正方形[Next_E] _ {<x，y>}} \ Rightarrow \正方形I_E$
• 在以下帮助下：
  
  1. $$$Init_E \ Rightarrow I_E$
  2. $$$\ color {red} {\ square [Next_E] _ {<x，y>}} \ land I_E \ Rightarrow I'_E$

此更改负责欧几里得算法的安全性，因为现在可能出现以下行为： $$$x$ 和 $$$y$ 不要改变。 必须使用活动属性消除这些行为。 这很简单，但我现在不再赘述。

讨论实现。 假设我们有一台像计算机一样实现欧几里德算法的机器。 它表示数字为32位字的数组。 为了进行简单的加减运算，她需要很多步骤，例如计算机。 如果您尚未触摸活动，那么我们也可以通过公式来想象这样的机器 $$$Init_ {ME} \ land \ square [Next_ {ME}] _ {<...>}$ 。 当我们说欧几里得机器实现欧几里得算法时是什么意思？ 这意味着以下公式是正确的：

不要惊慌，我们现在将按顺序检查它。 它说我们的机器满足一些特性（ $$$\ Rightarrow$ ） 此属性是欧几里得公式。 $$$（Init_E \ land \ square [Next_E] _ {<x，y>}$ ，点是包含欧几里得机器变量的表达式，以及 $$$与$ 是替代品。 换句话说，第二行是欧几里得公式，其中 $$$x$ 和 $$$y$ 用点代替。 在数学中，没有普遍接受的替代表示法，因此我必须自己提出。 本质上，欧几里得公式（ $$$Init_E \ land \ square [Next_E] _ {<x，y>}$ ）是公式的缩写：

公式中红色突出显示的部分允许 $$$x$ 和 $$$y$ 在 $$$（Init_E \ land \ square [Next_E] _ {\ color {red} {<x，y>}}$ 保持不变。

所描述的表达式不仅说明机器实现了欧几里得算法，而且还考虑了指定的替换方式来做到这一点。 如果您仅使用几个程序，并说这些程序的变量与 $$$x$ 和 $$$y$ -说所有这些“实现欧几里得算法”是没有意义的。 有必要确切说明算法将如何实现，为什么在所有排列后公式将变为真。 现在，我没有时间证明上述定义是正确的，您必须相信我的话。 但是，我认为您已经意识到它的简单和优雅。 数学真的很漂亮-通过它我们能够确定一种算法实现另一种算法的含义。

为了证明这一点，有必要找到一个合适的不变式 $$$I_ {ME}$ 欧几里得的汽车。 为此，必须满足以下条件：

1. $$$Init_ {ME} \ Rightarrow（Init_E，WITH \ Thinspace x \ leftarrow ...，y \ leftarrow ...）$
2. $$$I_ {ME} \ land [Next_ {ME}] _ {<...>} \ Rightarrow（[Next_E] _ {<x，y>}，WITH \ thinspace x \ leftarrow ...，y \ leftarrow。 ..）$

我们现在将不再研究它们，只是要注意一个事实，尽管它们不是最简单的，但它们是普通的数学公式。 不变的 $$$I_ {ME}$ 解释了为什么欧几里得机器实现欧几里得算法。 实现是用表达式代替变量。 这是非常常见的数学运算。 但是在程序中，无法执行这种替换。 您不能在赋值表达式x = …中用a + b代替x ，这样的记录将毫无意义。 那么，如何确定一个程序实现了另一个程序呢？ 如果仅考虑编程，则不可能。 在最好的情况下，您会找到一些棘手的定义，但是更好的方法是将程序转换为数学公式，并使用我上面给出的定义。 将程序转换成数学公式就是要赋予程序语义。 如果欧几里得机器是一个程序，并且 $$$Init_ {ME} \ land \ square [Next_ {ME}] _ {<...>}$ -她的数学符号 $$$（Init_E \ land \ square [Next_E] _ {<x，y>}，WITH \ thinspace x \ leftarrow ...，y \ leftarrow ...）$ 向我们展示了这意味着“程序实现了欧几里得算法”。 编程语言非常复杂，因此将程序翻译成数学语言的过程也很复杂，因此实际上我们不这样做。 简单来说，编程语言并非旨在在其上编写算法。 , , , : , x y , . , , , .

- : , , , . , . — . . , . , — , . :

. $$$DecrementX$ ：

— $$$DecrementY$ ：

, :

.

. Rosetta — , . Virtuoso. . TLA+, . , , . , (Eric Verhulst), . , TLA+, : « TLA+ . - C. TLA+ Virtuoso». . . , , , . . TLA+. , .

. Communications of the ACM ] , - Amazon . Amazon Web Services — , Amazon. , — TLA+. . -, , . , , . -, , . , — , , . -, , Amazon , . , 10% TLA+.

— Microsoft. TLA+ 2004 . 2015 TLA+, . . Amazon Web Services. Microsoft , , . : « , ». , Microsoft - . : « ». 2016-17 . TLA+, 150 , Azure ( Microsoft). Azure 2018 , , . : « , . , ». , , . - : , . , , .

, TLA+ . , TLA+, TLA+ Azure, , TLA+. , . , TLA+ , . Microsoft Cosmos DB, , . , . TLA+, , , TLA+.

TLA+ — . . TLA+ . , , . TLA+ , . : TLA+ , .

, . , , . , . Amazon Microsoft , . , .

, . — , . , Hydra 2019, 11-12 2019 -. .