本文为转载 . 但在她之前有一点介绍。 丧尸是怎么形成的？ 每个人都遇到过这样一种情况，他们想把朋友或同事拉到他们的水平，但没有成功。 与其说是你，不如说是他，“行不通”：天平的一边是正常的薪水、任务等等，另一边是思考的需要。 思考是不愉快和痛苦的。 他很快就放弃了，完全没有动脑筋继续写代码。 你想象需要付出多少努力才能克服习得性无助的障碍，但你就是不去做。 丧尸就是这样形成的，看起来可以治愈，但似乎没有人会去做。
当我看到那个 （是的，教科书上的同志） 而且不做报告，而是做问答环节，我有点警惕。 为了以防万一，Leslie 是一位世界著名的科学家，分布式计算基础著作的作者，您也可以通过 LaTeX 中的字母 La 了解他 - “Lamport TeX”。 第二个令人担忧的因素是他的要求：每个来的人都必须（绝对免费）提前听他的一些报告，至少提出一个问题，然后才来。 我决定去看看 Lamport 在那里广播的内容 - 太棒了！ 正是那东西，治愈僵尸的神奇链接药丸。 我警告你：从文本来看，超灵活方法论的爱好者和那些不喜欢测试所写内容的人可能会特别疲倦。
实际上，在 habrokat 之后，研讨会的翻译就开始了。 享受阅读！
无论你承担什么任务，你总是需要经历三个步骤：
- 决定你想要达到的目标；
- 决定你将如何实现你的目标；
- 达到你的目标。
这也适用于编程。 在编写代码时，我们需要：
- 决定程序应该做什么；
- 确定它应该如何执行任务；
- 编写相应的代码。
最后一步当然很重要，但今天不讲。 相反，我们将讨论前两个。 每个程序员在开始工作之前都会执行它们。 除非您决定要编写浏览器还是数据库，否则您不会坐下来写作。 必须存在对目标的特定想法。 你一定要考虑程序到底要做什么，不要以某种方式编写，希望代码能以某种方式变成浏览器。
这个代码预想究竟是如何发生的呢？ 我们应该为此付出多少努力？ 这完全取决于我们要解决的问题的复杂程度。 假设我们要编写一个容错的分布式系统。 在这种情况下，我们应该在坐下来编写代码之前仔细考虑一下。 如果我们只需要将整数变量递增 1 怎么办？ 乍一看，这里的一切都是微不足道的，不需要思考，但后来我们记得可能会发生溢出。 因此，即使要了解一个问题是简单还是复杂，您也首先需要思考。
如果你提前考虑问题的可能解决方案，就可以避免错误。 但这需要你的思路清晰。 为此，您需要写下您的想法。 我真的很喜欢 Dick Guindon 的名言：“当你写作时，大自然会告诉你你的想法是多么草率。” 如果你不写，你只认为你在思考。 你需要以规范的形式写下你的想法。
规范执行许多功能，尤其是在大型项目中。 但我只会谈论其中之一：它们帮助我们清晰地思考。 清晰地思考是非常重要的，也是相当困难的，所以在这里我们需要任何帮助。 我们应该用什么语言编写规范？ 一般来说，这始终是程序员的第一个问题：我们将用什么语言编写。 没有一个正确答案：我们要解决的问题太多样化了。 对于某些人来说，TLA+ 是我开发的规范语言。 对于其他人，使用中文更方便。 一切都视情况而定。
更重要的是另一个问题：如何实现更清晰的思维？ 答：我们必须像科学家一样思考。 这是一种在过去 500 年中证明了自己的思维方式。 在科学中，我们建立现实的数学模型。 天文学也许是严格意义上的第一门科学。 在天文学使用的数学模型中，天体表现为具有质量、位置和动量的点，尽管实际上它们是有山有海、有潮汐有潮汐的极其复杂的物体。 与其他任何模型一样，此模型的创建是为了解决某些问题。 如果您需要寻找行星，这对于确定将望远镜指向何处非常有用。 但是如果你想预测这个星球上的天气，这个模型就不行了。
数学使我们能够确定模型的属性。 科学表明这些属性如何与现实相关。 让我们谈谈我们的科学，计算机科学。 我们工作的现实是各种计算系统：处理器、游戏机、计算机、执行程序等等。 我将讨论在计算机上运行程序，但总的来说，所有这些结论都适用于任何计算系统。 在我们的科学中，我们使用许多不同的模型：图灵机、部分有序的事件集等等。
什么是程序？ 这是任何可以独立考虑的代码。 假设我们需要写一个浏览器。 我们执行三个任务：我们设计用户的程序视图，然后我们编写程序的高级图，最后我们编写代码。 当我们编写代码时，我们意识到我们需要编写一个文本格式化程序。 这里我们又需要解决三个问题：确定这个工具返回什么文本； 选择格式化算法； 写代码。 此任务有其自己的子任务：正确地将连字符插入单词中。 我们还分三个步骤解决了这个子任务——如您所见，它们在许多级别上重复。
让我们更详细地考虑第一步：程序解决了什么问题。 在这里，我们通常将程序建模为接受一些输入并产生一些输出的函数。 在数学中，函数通常被描述为一组有序的对。 例如，自然数的平方函数被描述为集合 {<0,0>, <1,1>, <2,4>, <3,9>, …}。 这种函数的域是每对第一个元素的集合，即自然数。 要定义一个函数，我们需要指定它的作用域和公式。
但是数学中的函数与编程语言中的函数不同。 数学要容易得多。 由于我没有时间处理复杂的示例，让我们考虑一个简单的示例：C 中的函数或 Java 中返回两个整数的最大公约数的静态方法。 在这个方法的规范中，我们会写：计算 GCD(M,N) 论据 M и N哪里 GCD(M,N) - 一个函数，其域是整数对的集合，返回值是可被整除的最大整数 M и N. 这个模型与现实有什么关系？ 该模型对整数进行操作，而在 C 或 Java 中我们有一个 32 位 int. 这个模型允许我们决定算法是否正确 GCD，但它不会防止溢出错误。 这将需要一个更复杂的模型，但没有时间。
让我们谈谈函数作为模型的局限性。 有些程序（如操作系统）不只是为某些参数返回某个值，它们可以连续运行。 此外，作为模型的功能不太适合第二步：规划如何解决问题。 快速排序和冒泡排序计算的是同一个函数，但它们是完全不同的算法。 因此，为了描述程序的目标是如何实现的，我使用了一个不同的模型，我们称之为标准行为模型。 其中的程序被表示为一组所有允许的行为，每个行为又是一个状态序列，状态就是对变量的赋值。
让我们看看 Euclid 算法的第二步是什么样的。 我们需要计算 GCD(M, N). 我们初始化 M 如 x和 N 如 y，然后重复从较大变量中减去这些变量中较小的变量，直到它们相等。 例如，如果 M = 12和 N = 18，我们可以描述以下行为：
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
A除非 M = 0 и N = 0？ 零可以被所有数字整除，所以在这种情况下没有最大的除数。 在这种情况下，我们需要回到第一步问：我们真的需要为非正数计算 GCD 吗？ 如果这不是必需的，那么您只需要更改规范即可。
这里我们应该稍微题外话一下生产力。 它通常以每天编写的代码行数来衡量。 但是如果你去掉了一定数量的行，你的工作就会更有用，因为你有更少的错误空间。 摆脱代码的最简单方法是第一步。 您完全有可能不需要您尝试实现的所有花里胡哨的功能。 简化程序和节省时间的最快方法就是不做不该做的事情。 第二步是第二个最省时的潜力。 如果你用写的行来衡量生产力，那么思考如何完成一项任务会让你 生产力较低，因为你可以用更少的代码解决同样的问题。 我这里不能给出准确的统计，因为我没有办法统计我在规范上花时间，也就是在第一步和第二步上没有写的行数。 而且这里也不能设置实验，因为在实验中我们没有权利完成第一步，任务是预先确定的。
非正式规范中的许多困难很容易被忽略。 编写严格的功能规范没有什么难的，我不会讨论这个。 相反，我们将讨论为标准行为编写强规范。 有一个定理说任何一组行为都可以使用安全属性来描述 （安全） 和生存属性 （活跃度）. 安全意味着不会发生任何不好的事情，程序不会给出错误的答案。 生存能力意味着迟早会有好事发生，即程序迟早会给出正确答案。 通常，安全性是一个更重要的指标，错误最常发生在这里。 因此，为了节省时间，我不会谈论生存能力，尽管它当然也很重要。
我们首先通过规定一组可能的初始状态来实现安全性。 其次，每个状态与所有可能的下一个状态的关系。 让我们像科学家一样行动，用数学方式定义状态。 初始状态集由公式描述，例如，在 Euclid 算法的情况下： (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] 表达式的两部分都是假的，所以它没有下一个状态。 所以，我们对第二步有一个完整的说明——正如你所看到的，这是很普通的数学，就像在工程师和科学家中一样，而不是像在计算机科学中那样奇怪。
这两个公式可以组合成时序逻辑的一个公式。 她举止优雅，好解释，只是现在没空理她。 我们可能只需要时序逻辑来实现活泼属性，而不需要安全性。 我不喜欢这样的时间逻辑，它不是很普通的数学，但在生动的情况下，它是一种必要的邪恶。
在欧几里得算法中，对于每个值 x и y 具有独特的价值 x' и y'，这使得与下一个状态的关系为真。 换句话说，欧几里得算法是确定性的。 要对非确定性算法建模，当前状态需要有多个可能的未来状态，并且每个非素数变量值都有多个素数变量值，以便与下一个状态的关系为真。 这很容易做到，但我现在不举例。
要制作工作工具，您需要形式数学。 如何使规范正式化？ 为此，我们需要一种正式的语言，例如， . Euclid 算法的规范在这种语言中看起来像这样：
带三角形的等号符号表示符号左侧的值定义为等于符号右侧的值。 本质上，规范是一个定义，在我们的例子中是两个定义。 对于 TLA+ 中的规范，您需要添加声明和一些语法，如上面的幻灯片所示。 在 ASCII 中，它看起来像这样：
如您所见，没有什么复杂的。 可以测试 TLA+ 的规范，即绕过小模型中所有可能的行为。 在我们的例子中，这个模型将是某些值 M и N. 这是一种非常高效和简单的完全自动的验证方法。 也可以写出形式化的真值证明，然后机械地检查，但这需要很多时间，所以几乎没有人这样做。
TLA+ 的主要缺点是它是数学，程序员和计算机科学家都害怕数学。 乍一看，这听起来像个玩笑，但不幸的是，我是认真的。 我的同事刚刚告诉我他是如何尝试向几位开发人员解释 TLA+ 的。 公式一出现在屏幕上，顿时就变成了呆呆的眼睛。 所以如果 TLA+ 吓到你，你可以使用 ，它是一种玩具编程语言。 PlusCal 中的表达式可以是任何 TLA+ 表达式，即大体上可以是任何数学表达式。 此外，PlusCal 具有用于非确定性算法的语法。 因为 PlusCal 可以编写任何 TLA+ 表达式，所以 PlusCal 比任何真正的编程语言都更具表现力。 接下来，PlusCal 被编译成易于阅读的 TLA+ 规范。 当然，这并不意味着复杂的 PlusCal 规范会变成 TLA+ 上的简单规范——只是它们之间的对应关系很明显，不会有额外的复杂性。 最后，该规范可以通过 TLA+ 工具进行验证。 总而言之，PlusCal 可以帮助克服数学恐惧症，即使对于程序员和计算机科学家来说也很容易理解。 过去，我在上面发布算法有一段时间（大约 10 年）。
或许有人会反对说 TLA+ 和 PlusCal 是数学，而数学只对发明的例子起作用。 实际上，您需要一种具有类型、过程、对象等的真实语言。 这是错误的。 以下是在亚马逊工作的 Chris Newcomb 写道： “我们已经在十个主要项目中使用了 TLA+，在每个项目中，使用它都对开发产生了重大影响，因为我们能够在投入生产之前发现危险的错误，并且因为它给了我们所需的洞察力和信心在不影响程序真实性的情况下进行积极的性能优化”. 您经常会听到，当使用形式化方法时，我们会得到低效的代码——实际上，一切恰恰相反。 此外，有一种观点认为，即使程序员确信形式化方法的用处，也无法说服管理者相信形式化方法的必要性。 纽科姆写道： “现在管理人员都在大力推动编写TLA+的规范，并专门为此分配时间”. 因此，当管理人员看到 TLA+ 正在发挥作用时，他们会很乐意接受它。 Chris Newcomb 大约在六个月前（2014 年 14 月）写了这篇文章，但据我所知，现在有 10 个项目使用了 TLA+，而不是 360 个。另一个例子是 XBox 360 的设计。一位实习生来到 Charles Thacker 和为内存系统编写规范。 多亏了这个规范，才发现了一个原本不会被注意到的错误，因此每个 XBox XNUMX 在使用四个小时后都会崩溃。 IBM 工程师确认他们的测试不会发现此错误。
您可以在 Internet 上阅读有关 TLA+ 的更多信息，但现在让我们谈谈非正式规范。 我们很少需要编写计算最小公约数之类的程序。 我们更经常编写程序，例如我为 TLA+ 编写的漂亮打印机工具。 经过最简单的处理后，TLA+代码大概是这样的：
但在上面的示例中，用户很可能希望连词和等号对齐。 所以正确的格式看起来更像这样：
考虑另一个例子：
而这里相反，等号、加号、乘号在源码中的排列是随机的，所以最简单的处理就足够了。 一般来说，正确的格式没有精确的数学定义，因为在这种情况下“正确”意味着“用户想要什么”，而这无法从数学上确定。
似乎如果我们没有真值的定义，那么规范就毫无用处。 但事实并非如此。 仅仅因为我们不知道一个程序应该做什么并不意味着我们不需要考虑它是如何工作的——相反，我们必须付出更多的努力。 规范在这里尤为重要。 结构化打印的最优方案是无法确定的，但这并不代表我们根本不应该采用它，把代码写成意识流也不是什么好事。 最后，我写了一个包含六个规则的规范和定义 以评论的形式 在java文件中。 以下是其中一条规则的示例： a left-comment token is LeftComment aligned with its covering token. 这条规则是用数学英语写的： LeftComment aligned, left-comment и covering token - 带有定义的术语。 数学家就是这样描述数学的：他们写下术语的定义，并根据这些定义制定规则。 这样一个规范的好处是，850 个规则比 850 行代码更容易理解和调试。 我必须说编写这些规则并不容易，调试它们需要花费大量时间。 特别是出于这个目的，我写了一个代码来报告使用了哪个规则。 由于我在几个例子上测试了这六个规则，我不必调试 XNUMX 行代码，而且发现错误也很容易。 Java 对此有很好的工具。 如果我刚刚编写代码，我会花费更长的时间，而且格式的质量也会更差。
为什么不能使用正式的规范？ 一方面，正确的执行在这里并不是太重要。 结构打印输出肯定不会取悦任何人，所以我不必让它在所有奇怪的情况下都能正常工作。 更重要的是我没有足够的工具。 TLA+ 模型检查器在这里没有用，所以我必须手动编写示例。
上述规格具有所有规格共有的特征。 它比代码更高级别。 它可以用任何语言实现。 任何工具或方法对编写它都是无用的。 没有编程课程可以帮助您编写此规范。 并且没有任何工具可以使此规范成为不必要的，当然，除非您正在编写一种专门用于在 TLA+ 中编写结构化打印程序的语言。 最后，本规范并没有说明我们将如何编写代码，它只说明了这段代码的作用。 我们编写规范是为了帮助我们在开始考虑代码之前考虑清楚问题。
但是这个规范也有区别于其他规范的特点。 95% 的其他规范明显更短更简单：
此外，该规范是一组规则。 通常，这是规格不佳的标志。 理解一组规则的后果是相当困难的，这就是为什么我不得不花很多时间调试它们。 但是，在这种情况下，我找不到更好的方法。
关于连续运行的程序值得多说几句。 通常，它们并行工作，例如操作系统或分布式系统。 很少有人能在精神上或纸上理解它们，我不是其中之一，尽管我曾经能够做到。 因此，我们需要能够检查我们工作的工具——例如 TLA+ 或 PlusCal。
如果我已经知道代码究竟应该做什么，为什么还要编写规范呢？ 事实上，我只是以为我知道。 此外，有了规范，局外人不再需要进入代码来了解他到底做了什么。 我有一个规则：不应该有一般规则。 这个规则有一个例外，当然，这是我遵循的唯一通用规则：代码做什么的规范应该告诉人们他们在使用代码时需要知道的一切。
那么关于思考，程序员究竟需要知道些什么呢？ 对于初学者来说，和其他人一样：如果你不写，那么在你看来，你只是在思考。 此外，您需要在编码之前思考，这意味着您需要在编码之前先编写。 规范是我们在开始编码之前编写的内容。 任何人都可以使用或修改的任何代码都需要规范。 而这个“某人”可能就是代码写完一个月后的作者本人。 大型程序和系统、类、方法，有时甚至是单个方法的复杂部分都需要规范。 关于代码究竟应该写些什么？ 您需要描述它的作用，即什么对使用此代码的任何人都有用。 有时可能还需要指定代码如何实现其目的。 如果我们在算法课程中经历过这种方法，那么我们就称它为算法。 如果它是更特别、更新颖的东西，那么我们就称它为高层次设计。 这里没有形式上的区别：两者都是程序的抽象模型。
您究竟应该如何编写代码规范？ 最主要的是：它应该比代码本身高一级。 它应该描述状态和行为。 它应该像任务要求的那样严格。 如果您正在编写有关如何执行任务的规范，您可以用伪代码或使用 PlusCal 编写它。 您需要学习如何在正式规范上编写规范。 这将为您提供必要的技能，这些技能也将帮助您掌握非正式技能。 你如何学习编写正式的规范？ 当我们学习编程时，我们编写程序然后调试它们。 这里也是一样的：编写规范，用模型检查器检查，并修复错误。 TLA+ 可能不是正式规范的最佳语言，另一种语言可能更适合您的特定需求。 TLA+的优势在于它很好地教授了数学思维。
如何链接规范和代码？ 借助链接数学概念及其实现的注释。 如果您使用图形，那么在程序级别您将拥有节点数组和链接数组。 因此，你需要准确地写出图是如何被这些编程结构实现的。
需要注意的是，以上都不适用于实际写代码的过程。 当你写代码的时候，也就是你执行第三步的时候，你也需要思考，想通程序。 如果一个子任务被证明是复杂的或不明显的，你需要为它写一个规范。 但我不是在这里谈论代码本身。 您可以使用任何编程语言、任何方法，这与它们无关。 此外，以上都没有消除测试和调试代码的需要。 即使抽象模型编写正确，在其实现中也可能存在错误。
编写规范是编码过程中的一个附加步骤。 多亏了它，可以更轻松地发现许多错误——我们从亚马逊程序员的经验中了解到这一点。 有了规范，节目的质量就更高了。 那么，为什么我们经常没有它们呢？ 因为写作很难。 写作很难，因为为此你需要思考，而思考也很困难。 假装你的想法总是更容易。 这里可以用跑步来类比——跑得越少，跑得越慢。 您需要锻炼肌肉并练习写作。 需要练习。
规格可能不正确。 您可能在某个地方犯了错误，或者需求可能已经改变，或者可能需要进行改进。 任何人使用的任何代码都必须更改，因此迟早规范将不再与程序匹配。 理想情况下，在这种情况下，您需要编写新的规范并完全重写代码。 我们非常清楚没有人会那样做。 实际上，我们修补代码并可能更新规范。 如果这迟早会发生，那么为什么要编写规范呢？ 首先，对于将要编辑你的代码的人来说，规范中的每一个额外的单词都是金子般的重量，这个人很可能就是你自己。 我经常因为在编辑代码时没有获得足够的规范而自责。 而且我编写的规范比代码还多。 因此，当您编辑代码时，规范总是需要更新。 其次，随着每次修订，代码变得更糟，变得越来越难以阅读和维护。 这是熵的增加。 但是，如果您不从规范开始，那么您编写的每一行都将是一次编辑，并且代码从一开始就会笨拙且难以阅读。
如上所述 , 没有计划就没有胜利，没有计划就没有胜利. 他对战斗略知一二。 有一种观点认为编写规范是浪费时间。 有时确实如此，任务非常简单，无需考虑。 但是你应该永远记住，当你被告知不要写规范时，你就是被告知不要思考。 你应该每次都考虑一下。 仔细思考任务并不能保证您不会犯错误。 众所周知，没有人发明魔术棒，编程是一项艰巨的任务。 但如果你不把问题想透，你肯定会犯错误。
你可以在一个特殊的网站上阅读更多关于 TLA+ 和 PlusCal 的信息，你可以从我的主页去那里 . 这就是我的全部，谢谢你的关注。
请注意，这是翻译。 当您写评论时，请记住作者不会阅读它们。 如果你真的想和作者聊天，那么他将参加将于 2019 年 11 月 12 日至 2019 日在圣彼得堡举行的 Hydra XNUMX 会议。 可以购买门票 .
来源： habr.com