这是斯坦福工作室的翻译文章。 但是在她之前是一个简短的介绍。 僵尸是如何形成的？ 每个人都陷入一种情况，您想将朋友或同事提升到您的水平，但效果不佳。 而且，“解决不了”对您的影响不如与他对您的影响：一方面，薪水是正常的薪水，任务等等，另一方面，是思考的需要。 思考是不愉快和痛苦的。 他迅速放弃并继续编写代码，完全不用动脑筋。 您想像一下您需要花费多少精力来克服学习型无助的障碍，而您却没有这样做。 僵尸就是这样形成的，看似可以治愈，但似乎没人能做到。
当我看到莱斯利·兰普波特 （是的，教科书中的那个朋友） 来俄罗斯而不是发表报告，而是进行问答时，我有点谨慎。 以防万一，莱斯利是举世闻名的科学家，是分布式计算的基础著作的作者，您也可以通过LaTeX中的字母La（“ Lamport TeX”）认识他。 第二个令人担忧的因素是他的需求：每个来访者都应该（完全免费）事先听取他的几份报告，提出至少一个问题，然后才来。 我决定去看Lampport在那广播的节目-太好了！ 这正是那个东西，一个治疗僵尸的神奇链接药。 我警告您：从文字上来说，超灵活方法论的爱好者和不热衷于测试所写内容的人可能会特别厌倦。
实际上，在哈勃罗卡特之后，研讨会的翻译开始了。 祝您阅读愉快！
无论您执行什么任务，都始终需要完成三个步骤：
这也适用于编程。 在编写代码时，我们需要：
- 决定程序应该做什么；
- 准确确定应如何完成任务；
- 编写适当的代码。
当然，最后一步非常重要，但今天我将不讨论它。 相反，我们讨论前两个。 每个程序员在开始工作之前都要执行它们。 如果您尚未确定要写的是浏览器或数据库，就不要坐下来写作。 必须有明确的目标构想。 而且，您一定会考虑该程序的确切功能，而不是以某种方式编写该程序，以希望代码本身可以以某种方式变成浏览器。
对代码的这种初步思考是如何发生的？ 我们应该为此付出多少努力？ 这完全取决于我们要解决的问题有多困难。 假设我们要编写一个容错的分布式系统。 在这种情况下，我们应该在坐下来阅读代码之前适当考虑所有内容。 如果我们只需要将整数变量增加1？ 乍一看，这里的一切都是微不足道的，不需要思考，但随后我们回想起可能会发生溢出。 因此，即使要了解问题是简单的还是复杂的，您也首先需要思考。
如果您想出解决问题的办法，则可以避免错误。 但这要求您的思路必须清楚。 为此，您需要写下您的想法。 我真的很喜欢迪克·金登（Dick Gindon）的话：“写作时，大自然向您展示了您的思维多么草率。” 如果您不写，那么您似乎只是在想。 您需要以规范的形式写下您的想法。
规范可以实现许多功能，尤其是在大型项目中。 但是，我仅谈论其中之一：它们帮助我们清晰地思考。 清楚地思考是非常重要且非常困难的，因此在这里我们需要任何帮助。 我们应该用哪种语言写规范？ 对于程序员来说，这始终是第一个问题：我们将使用哪种语言编写。 没有一个正确的答案：我们解决的问题过于多样化。 TLA +对某些人很有用-这是我开发的规范语言。 对于其他人，使用中文更方便。 一切都取决于情况。
另一个问题更为重要：如何实现更清晰的思维？ 答：我们必须像科学家一样思考。 在过去的500年中，这种思维方式已得到证明。 在科学中，我们建立现实的数学模型。 从严格意义上讲，天文学也许是第一门科学。 在天文学中使用的数学模型中，天体显示为具有质量，位置和动量的点，尽管实际上它们是极其复杂的物体，具有山脉和海洋，潮汐。 与其他模型一样，此模型旨在解决某些问题。 如果您需要找到一个行星，那么对于确定望远镜的指向非常有用。 但是，如果您要预测这颗行星的天气，则此模型将无法工作。
数学使我们能够确定模型的属性。 科学证明了这些属性与现实之间的关系。 让我们谈谈我们的科学，计算机科学。 我们工作的现实是各种类型的计算系统：处理器，游戏机，计算机，执行程序等。 我将讨论在计算机上运行程序，但总的来说，所有这些结论都适用于任何计算机系统。 在我们的科学中，我们使用许多不同的模型：图灵机，部分排序的事件集以及许多其他模型。
什么是程序？ 这是可以独立考虑的任何代码。 假设我们需要编写一个浏览器。 我们执行以下三个任务：为用户设计程序的表示形式，然后编写程序的高级方案，最后编写代码。 在编写代码时，我们知道我们需要编写一个用于格式化文本的工具。 在这里，我们再次需要解决三个问题：确定此工具将返回的文本； 选择一种格式化算法； 编写代码。 此任务有其自己的子任务：在单词中正确插入连字符。 我们还分三个步骤解决此子任务-如我们所见，它们在许多级别上都重复进行。
让我们更详细地考虑第一步：程序解决了什么问题。 在这里，我们通常将程序建模为一个函数，该函数接收一些输入并提供一些输出。 在数学中，函数通常被描述为有序对。 例如，自然数的平方函数被描述为集合{<0,0>，<1,1>，<2,4>，<3,9>，...}。 这种功能的范围是每对中第一个元素的集合，即自然数。 要定义一个函数，我们需要指定它的范围和公式。
但是数学中的函数与编程语言中的函数并不相同。 数学要简单得多。 由于我没有时间处理复杂的示例，请考虑一个简单的示例：C中的函数或Java中的静态方法，该函数返回两个整数的最大公约数。 在此方法的规范中，我们编写：为参数M和N计算GCD(M,N) ，其中GCD(M,N)是一个函数，其域是整数对的集合，返回值是可被整数整除的最大整数。 M和N 现实与这个模型有什么关系？ 该模型使用整数操作，在C或Java中，我们有一个32位int 。 该模型使我们能够确定GCD算法是否正确，但不能防止溢出错误。 这将需要一个更复杂的模型，没有时间可用。
让我们谈谈函数作为模型的局限性。 某些程序（例如，操作系统）的工作不会归结为针对某些参数返回某个值；它们可以连续执行。 此外，作为模型的功能不适合第二步：规划解决问题的方法。 快速排序和气泡排序计算的功能相同，但是它们是完全不同的算法。 因此，为了描述实现程序目标的方式，我使用了一个不同的模型，我们将其称为标准行为模型。 其中的程序以所有允许的行为的集合的形式出现，每个行为都是一个状态序列，一个状态是将值分配给变量。
让我们看一下欧几里德算法的第二步。 我们需要计算GCD(M, N) 。 我们将M初始化为x ，将N初始化为y ，然后从较大的变量中减去较小的变量，直到它们相等。 例如，如果M = 12且N = 18 ，我们可以描述以下行为：
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
如果M = 0且N = 0 ？ 零可以被所有数字整除，因此在这种情况下没有最大除数。 在这种情况下，我们需要返回第一步，然后问：我们真的需要计算非正数的GCD吗？ 如果没有必要，则只需要更改规格即可。
在这里应该对生产率做些小的论述。 通常用每天编写的代码行数来衡量。 但是，如果您删除了某些行，那么您的工作就会有用得多，因为您的bug占用空间较小。 摆脱代码的最简单方法是第一步。 您可能根本不需要您尝试实现的所有功能。 简化程序并节省时间的最快方法是不做不值得做的事情。 在节省时间方面，第二步位居第二。 如果您通过编写的行数来衡量生产率，那么考虑如何完成任务将使您的生产率降低 ，因为您可以用更少的代码解决相同的问题。 我无法在此处提供确切的统计信息，因为由于我花了很多时间在规范（即第一步和第二步）上，所以无法计算未写的行数。 而且实验也不能放在这里，因为在实验中我们无权完成第一步，因此任务是预先确定的。
在非正式规范中，许多困难很容易被忽略。 为功能编写严格的规范没有什么复杂的；我将不讨论这一点。 相反，我们将谈论为标准行为模型编写严格的规范。 有一个定理指出，可以使用安全性和活动性描述任何行为集。 安全性意味着不会发生任何不良情况，程序不会给出错误的答案。 活力意味着迟早会有好事发生，也就是说，程序迟早会给出正确的答案。 通常，安全性是一个更重要的指标；错误通常在此处出现。 因此，为了节省时间，我不会谈论生存能力，尽管它当然也很重要。
我们通过首先规定许多可能的初始状态来实现安全性。 其次，与每个状态的所有可能的下一个状态的关系。 我们将以科学家的身份行事，并在数学上定义状态。 初始状态集由公式描述，例如，在欧几里得算法的情况下： (x = M) ∧ (y = N) 。 对于M和N某些值，只有一个初始状态。 与下一个状态的关系由公式描述，其中下一个状态的变量用破折号写成，而当前状态不带破折号。 对于欧几里得算法，我们将处理两个公式的析取，其中一个x是最大值，第二个y ：
在第一种情况下，y的新值等于y的先前值，我们得到x的新值，从较大的变量中减去较小的值。 在第二种情况下，我们做相反的事情。
让我们回到欧几里得算法。 再次假设M = 12 ， N = 18 。 这确定了唯一的初始状态， (x = 12) ∧ (y = 18) 。 然后，将这些值替换为上面的公式并得到：
在这里，唯一可能的解决方案是： x' = 18 - 12 ∧ y' = 12 ，我们得到的行为是： [x = 12, y = 18] 。 同样，我们可以描述行为中的所有状态： [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6] 。
在最后一个状态[x = 6, y = 6]表达式的两个部分均为false，因此它没有下一个状态。 因此，我们具有第二步的完整规范-如我们所见，这是工程师和科学家所用的非常普通的数学，而在计算机科学中则并不奇怪。
这两个公式可以组合为一个时间逻辑公式。 她优雅且易于解释，但现在她没有时间了。 时间逻辑我们可能只需要活泼的属性，不需要安全性。 这样的时间逻辑并不令人愉快，它不是很普通的数学，但是在生动的情况下这是必不可少的恶魔。
在欧几里得算法中，对于x和y每个值，都有x'和y'唯一值，使与下一个状态的关系成立。 换句话说，欧几里得算法是确定性的。 为了模拟非确定性算法，有必要使当前状态具有多个可能的未来状态，并且不带质数的变量的每个值都具有具有与下一个状态的关系为真的笔触的变量的多个值。 这并不难做到，但我现在不举一些例子。
要制作工具，您需要形式数学。 如何使规范正式化？ 为此，我们需要一种正式的语言，例如TLA + 。 此语言中的欧几里得算法的规范如下所示：
带有三角形的等号符号表示将符号左侧的值定义为等于符号右侧的值。 本质上，规范是一个定义，在我们的例子中是两个定义。 您需要在TLA +中为规范添加声明和一些语法，如上图所示。 在ASCII中，它将如下所示：
如您所见，没有什么复杂的。 可以检查TLA +的规范，即绕过小模型中的所有可能行为。 在我们的情况下，该模型将是M和N特定值N 这是一种非常有效且简单的验证方法，可完全自动运行。 此外，您可以编写真实的形式证明并以机械方式进行验证，但这需要花费大量时间，因此几乎没有人这样做。
TLA +的主要缺点在于它是数学，而程序员和计算机科学家都害怕数学。 乍一看，这听起来像是在开玩笑，但不幸的是，我是认真地说出来的。 我的同事刚刚告诉我他如何尝试向几位开发人员解释TLA +。 配方一出现在屏幕上，便立即具有玻璃眼睛。 因此，如果TLA +令人恐惧，则可以使用PlusCal ，它是一种玩具编程语言。 PlusCal中的表达式可以是任何TLA +表达式，也就是说，基本上可以是任何数学表达式。 PlusCal还具有用于非确定性算法的语法。 由于任何TLA +表达式都可以用PlusCal编写，因此它更能表达任何实际的编程语言。 PlusCal被进一步编译为易于阅读的TLA +规范。 当然，这并不意味着复杂的PlusCal规范将在TLA +上变成一个简单的规范-只是它们之间的对应关系是显而易见的，不会再有其他复杂性。 最后，可以使用TLA +工具验证此规范。 通常，PlusCal可以帮助克服数学恐惧症；即使对于程序员和计算机科学家而言，它也很容易理解。 在过去的一段时间（约10年）中，我在上面发布了算法。
也许有人会反对TLA +和PlusCal是数学，而数学仅适用于发明的示例。 实际上，您需要一种具有类型，过程，对象等的真实语言。 事实并非如此。 这是在亚马逊工作的克里斯·纽科姆（Chris Newcomb）写道： “我们在10个大型项目中使用了TLA +，并且在每种情况下，TLA +的使用对开发都做出了重大贡献，因为我们能够在投入生产之前发现危险的错误，并且因为他给了我们积极的性能优化所必需的理解和信心，不会影响程序的真实性 。 ” 您经常会听到，使用形式化方法时，我们得到的代码效率低下-实际上，一切都恰恰相反。 另外，人们相信，即使程序员确信其有用性，也不能使管理人员确信需要正式方法。 纽科姆写道： “经理们现在正在竭尽全力为TLA +编写规范，他们为此专门投入时间 。 ” 因此，当经理们看到TLA +正在运行时，他们会很乐意接受。 克里斯·纽科姆（Chris Newcomb）大约在六个月前（2014年10月）撰写了这篇文章，但据我所知，现在TLA +用于14个项目中，而不是10个项目中。另一个示例与XBox 360的设计有关。一个实习生来到Charles Thacker并撰写内存系统规范。 由于使用了此规范，因此发现了一个以前不会注意到的错误，因此，每个XBox 360在使用四个小时后都会掉落。 IBM工程师已确认他们的测试不会检测到该错误。
您可以在Internet上阅读有关TLA +的更多信息，现在让我们讨论非正式规范。 我们很少需要编写计算最小公除数等的程序。 通常，我们编写的程序类似于我为TLA +编写的漂亮打印机工具。 经过最简单的处理后，TLA +代码将如下所示：
但是在上面的示例中，用户最有可能希望对连词和等号进行对齐。 因此，正确的格式应该更像这样：
考虑另一个示例：
相反，在这里，源中等号，加法和乘法的对齐是随机的，因此最简单的处理就足够了。 通常，没有正确格式的精确数学定义，因为在这种情况下，“正确”表示“用户想要的”，而这不能通过数学确定。
似乎如果我们没有对真相的定义，那么该说明就没有用了。 但是事实并非如此。 如果我们不确切知道程序应该做什么，这并不意味着我们不需要考虑程序的工作-相反，我们应该为此付出更多的努力。 这里的规范尤其重要。 为结构清单确定最佳程序是不可能的，但这并不意味着我们根本不应该执行它，并且将代码作为意识流来编写并不是一件容易的事。 最后，我以Java文件中的注释形式编写了六个规则的说明，并带有定义。 这是其中一个规则的示例： a left-comment token is LeftComment aligned with its covering token 。 该规则用数学英语写成： LeftComment aligned ， left-comment和LeftComment aligned covering token是具有定义的术语。 数学家就是这样描述数学的：他们写术语的定义，并在它们的基础上编写规则。 该规范的好处是，理解和调试这六个规则比850行代码简单得多。 我必须说，编写这些规则并不容易，在调试它们上花费了大量时间。 尤其是出于这个目的，我编写了报告使用哪个规则的代码。 由于我通过一些示例检查了这六个规则，因此我不需要调试850行代码，并且发现这些错误非常容易。 Java为此提供了一些出色的工具。 如果我只是编写代码，那将花费我更长的时间，并且格式化的质量会变差。
为什么不可能使用正式规范？ 一方面，正确的执行在这里不是很重要。 结构清单肯定不会使任何人满意，因此在所有异常情况下我都不需要进行正确的工作。 更重要的是我没有足够的工具。 用于测试TLA +模型的工具在这里没有用，因此我将不得不手动编写示例。
给定的规范具有所有规范的共同特征。 它具有比代码更高的级别。 您可以用任何语言来实现它。 要编写它，任何工具或方法都没有用。 没有编程课程可以帮助您编写此规范。 并且没有工具可以使此规范变得不必要，除非您当然编写了专门用于在TLA +上编写结构清单程序的语言。 最后，此规范没有确切说明我们将如何编写代码，仅表示此代码的功能。 我们正在编写一个规范，以帮助我们在开始考虑代码之前仔细考虑问题。
但是，此规范还具有将其与其他规范区分开的功能。 95％的其他规格更短，更简单：
此外，该规范是一组规则。 这通常是规格不佳的标志。 理解规则集的含义是非常困难的，这就是为什么我不得不花很多时间调试它们的原因。 但是，在这种情况下，我找不到更好的方法。
值得一提的是，这些程序可以连续运行。 通常，它们可以并行运行，例如，操作系统或分布式系统。 很少有人能在他们的脑海或纸上理解它们，尽管我曾经负担得起，但我不是其中之一。 因此，需要可以测试我们工作的工具-例如TLA +或PlusCal。
如果我已经知道代码应该做什么，那么为什么需要编写规范？ 实际上，在我看来只有我知道这一点。 另外，如果有规范，局外人不再需要进入代码来了解他到底在做什么。 我有一条规则：不应有任何一般性规则。 当然，该规则是有例外的，这是我遵循的唯一通用规则：代码功能的规范是告诉人们使用该代码时需要知道的一切。
那么程序员到底需要了解什么呢？ 对于初学者，每个人都一样：如果您不写，那么您只会以为自己在想。 另外，您需要在编码之前进行思考，这意味着您需要在编码之前进行编写。 规范是我们在开始编码之前编写的。 任何人都可以使用或修改的任何代码都需要该规范。 而且这个“某人”可能在编写代码一个月后就成为了代码的作者。 对于大型程序和系统，类，方法，有时甚至是单个方法的复杂部分，都需要该规范。 关于该代码到底需要写什么？ 有必要描述他在做什么，即对使用此代码的任何人都有用的东西。 有时也可能需要准确指示代码如何实现其目标。 如果我们在算法过程中通过了此方法，则将其称为算法。 如果它更特别，新颖，那么我们将其称为高级设计。 没有形式上的区别：两者都是程序的抽象模型。
应该如何精确地编写代码规范？ 最主要的是：它应该比代码本身高一级。 它应该描述状态和行为。 它应根据任务要求严格。 如果要编写有关如何执行任务的规范，则可以用伪代码或使用PlusCal编写。 学习编写规范对正式规范是必要的。 这将为您提供必要的技能，这将对那些非正式的人有所帮助。 以及如何学习编写正式规范？ 当我们学习编程时，我们先编写程序，然后对其进行调试。同样的事情：您需要编写一个规范，使用模型检查工具对其进行检查并修复错误。TLA +可能不是正式规范的最佳语言，而另一种语言可能更适合您的特定需求。TLA +的优点是，它可以教您出色的数学思维。
如何链接规范和代码？借助将数学概念及其实现联系起来的注释。如果使用图，则在程序级别，将有节点数组和链接数组。因此，您需要准确地编写这些编程结构如何实现图形。
, . , , . , . . , , . , . , .
— . — Amazon. . ? . , , . , . — , . . .
. - , , . , - , , . . , . , , . , ? -, , , , . , . , . , , . -, , . . , , .
, , . - . , — . , , . , , , , . . , . , , — . , .
TLA+ PlusCal , . , .
, . — , . , Hydra 2019, 11-12 2019 -. .