演讲主题

正确性驱动建模：用TLA+设计系统

我们的头衔是科学家、工程师，我们具有丰富的设计经验，我们通晓各类设计方法。但是，我们可曾认真思考过软件工程中最基本的一个问题：设计的正确性。对这个问题的认识和处理方式，从某种程度上决定了软件开发中“科学”的成分。 正确性和我们经常谈论的设计方法和原则是两个正交的问题。想一想，如果一个复杂的并发系统出了bug，你定位bug的方式和系统是面向对象设计还是函数式设计，是否采用了敏捷方法、领域驱动等等有关系吗？没有，有时这些东西反而成为定位bug的障碍。 对于这类系统，定位bug最有效的方法是日志。Bug的根源往往是系统的某个行为状态没有满足预期的属性。所以我们会在系统的关键点上打印日志以记录我们觉得重要的系统状态，并通过各种方式测试系统以复现bug，然后分析日志，找出这个违反预期属性的行为。 这种方法繁琐、耗时、痛苦，而且bug还不一定会复现。因为无法保证那个导致bug的行为和状态一定出现，这往往和系统的运行环境有关。即便复现了，导致bug的状态序列通常嵌套很深，从海量的日志中找出这个序列无异于大海捞针. 但是，也只是在这个过程中，我们才开始真正认真思考到底想让系统干什么。 不过，如果把这个过程提前会怎么样呢？如果能在设计阶段就把正确性属性、和正确性有关的状态以及系统所有可能行为定义出来，这种定义既简洁明了，又具有和代码一样的精确性和严格性，并且还可以把这个设计驱动运行起来，让它呈现出所有可能行为，自动检查行为是否满足正确性属性，在出现问题时还会给出明确的状态序列…… 这个美梦能成真吗？ 能！并且会深刻影响设计，这正是本次演讲的主要内容。