How to Find Bugs in Systems That Don't Exist

TL;DR: 一场关于形式化方法的演讲以“做事器”三步流程为例，说明如何在尚不存在的系统中寻找 bug；开场还因硬件故障延迟了 8 分钟。 ## 迟到 8 分钟的开场 演讲者首先指出，活动晚了 8 分钟才开始。原因是： > 尽管软件应该正常工作，硬件也应该正常工作。而到今天早上为止，这个（硬件）不工作。 他澄清这不是自己的玩笑，而是杰森的玩笑——杰森就坐在后面。因此，他现在是在一台新笔记本电脑上，用不熟悉的操作系统，在 Keynote 里运行幻灯片，而旁边另一台电脑在 PowerPoint 里运行。也就是说，对这场演讲来说，这些都是不熟悉的软件。他调侃道： > 我想这意味着，我真的希望出问题的东西加起来正好是 8 分钟。 ## 形式化方法是什么 正式开讲前，演讲者请听众举手： > 这里有多少人听说过形式化方法或形式化规范？ 结果几乎所有人都举手了。他表示，这个演讲的第一课就是“了解你的听众”。因为通常情况下，当他讲这个话题时，房间里根本没有人举手，没人听说过这些东西。这时他必须从第一性原理出发，做整套 TED 式的“我在甚至不存在的系统中找 bug”的演讲。 但这次听众大多已知基础。演讲者还是给出了定义： > 形式化方法是一门用数学来分析运行中的代码或代码设计以寻找 bug 的学科。 同时，他仍然需要用一个“TED 入门例子”，因为它为演讲的大部分内容定下了框架。 ## 例子：做事器 想象我们有一个“做事器”。做事器做一件事。在第一版中，做事器分三步做这件事： 1. 它检查这件事是否被标记为已完成。 2. 然后，如果这件事还没有被标记为已完成，它就把这件事标记为已完成。 3. 然后它真正去做这件事。 演讲者说： > 这里面有一个 bug。 他请听众直接把 bug 喊出来。转录中有一位听众开始回应（“好的，”），但内容在此处截断。 ## 留下的问题 这个“做事器”的例子是演讲的开场引子。演讲者强调，这个例子会为后续内容定下框架。至于三步流程中的 bug 到底是什么、如何用形式化方法在系统尚不存在时发现它，则需要继续观看演讲才能知道。 Source: https://www.youtube.com/watch?v=zSZkLyD9ILI