标签 DSL 下的文章

使用TLA+形式化验证Go并发程序

本文永久链接 – https://tonybai.com/2024/08/05/formally-verify-concurrent-go-programs-using-tla-plus

Writing is nature’s way of letting you know how sloppy your thinking is – Guindon

在2024年6月份举办的GopherCon Europe Berlin 2024上,一个叫Raghav Roy的印度程序员(听口音判断的)分享了Using Formal Reasoning to Build Concurrent Go Systems,介绍了如何使用形式化验证工具TLA+来验证Go并发程序的设计正确性。

TLA+是2013年图灵奖获得者、美国计算机科学家和数学家、分布式系统奠基性大神、Paxos算法Latex的缔造者Leslie B. Lamport设计的一种针对数字系统(Digital Systems)的高级(high-level)建模语言,TLA+诞生于1999年,一直低调演进至今。

TLA+不仅可以对系统建模,还可以与模型验证工具,比如:TLC model checker,结合使用,对被建模系统的行为进行全面的验证。我们可以将TLA+看成一种专门用于数字系统建模和验证的DSL语言

注:TLA是Temporal Logic of Actions的首字母缩写,Temporal Logic,即时序逻辑,是一种用于描述和推理系统行为随时间变化的逻辑框架,由Arthur Prior在1950年代后期引入逻辑学。在后面对TLA+的进一步介绍中,大家可能就会逐渐理解为什么Lamport给这门语言命名为TLA+了。

这不是我第一次接触TLA+,去年就花过一些时间了解过TLA+的资料,可能是因为姿势不够正确,没有在本博客留下只言片语,而这次我打算写点有关TLA+的东西。

1. 为什么需要TLA+

从1999年Lamport发表的论文“Specifying Concurrent Systems with TLA+”以及他2014年在微软的演讲“Thinking Above the Code”中 ,我们大致可以得到Lamport在20多年前设计TLA+的朴素的动机:期望程序员能像科学家一样思考,在编码之前用一种精确的形式化的语言写出目标系统的spec,这个过程类似于建筑架构师在建筑施工之前编制建筑的蓝图(blueprint)

为什么要编写目标系统的spec呢?

综合来自Lamport的相关资料,大致可以梳理出以下两点:

  • 从程序员的角度来看,在开始编码之前,先在抽象的层面思考系统行为,而不是过早地陷入编程语言的具体语法中。并且先写下规格说明,可以帮助程序员明确需求,认知系统,发现潜在问题,并为后续的编码和维护提供指导。
  • 从系统复杂性的角度来看,对于日益复杂的并发和分布式系统,仅靠直觉思考很难保证正确性,传统的测试方法也已经不足以发现所有问题。这时候写spec(规格说明)并用配套的检查工具进行验证就变得非常必要。

那为什么要新设计TLA+来写spec呢,而不是使用像C++这类编程语言,或是其他已存在的形式化语言来编写spec呢?

Lamport给出的理由有以下几个:

  • 编程语言的局限性:像C++这样的编程语言主要是为了实现而设计的,而不是为了spec。它们往往过于关注实现细节,而不是高层次的系统行为,缺乏描述并发和分布式系统所需的抽象能力,不适合表达系统的时序性质和不变量。

  • 已有形式化语言的不足:当时存在的其他形式化语言大多存在要么过于学术化,难以在实际工程中应用,要么难以自然地表达并发和分布式系统的特性等问题;并且缺少工具支持,不具备spec验证功能。

  • 数学建模的局限:纯粹的数学公式虽然精确,但对非数学背景的工程师来说难以理解和使用,缺乏工具支持,难以自动化验证,难以直接映射到系统设计和实现。

Lamport设计的TLA+是建立在坚实的数学基础之上,这使得它能够支持严格的数学推理和证明与自动化验证工具(如TLC模型检查器)无缝集成。TLA+被设计为在高度抽象的层面描述系统,不会像编程语言那样受实现细节的束缚。此外,结合时序逻辑和状态机,TLA+可以描述并发和分布式系统,并在设计层面验证系统的正确性。

根据Lamport的不完全统计,TLA+在Intel、Amazon、Microsoft等大厂都有应用,一些知名的算法以及开源项目也使用TLA+进行了形式化验证,比如Raft算法的作者就给出了Raft算法的TLA+ spec,国内分布式数据库厂商pingcap也在项目中使用TLA+对raft算法以及分布式事务做了形式化的验证

在这些应用案例中,AWS的案例是典型代表。AWS也将应用TLA+过程中积累的经验以paper的形式发表了,其论文集合也被Lamport放置在其个人主页上了。从这些论文内容来看,AWS对TLA+的评价是很正面的:AWS使用TLA+对10个大型复杂的真实系统进行建模和验证,的确发现了多个难以通过其他方法发现的微妙错误。同时,通过精确描述设计,TLA+迫使工程师更清晰地思考,消除了“看似合理的含糊之处”。此外,AWS工程师认为TLA+ spec也是一种很好的文档形式,可以提供精确、简洁、可测试的设计描述,有助于新人快速理解系统。

铺垫了这么多,TLA+究竟是什么?它是如何在高级抽象层面对分布式系统和并发系统进行描述和验证的?接下来,我们就来看一下。

2. Lamport对TLA+的定义

在Lamport的论文、书籍以及一些演讲资料中,他是这么定义TLA+的:A language for high-level modeling digital systems。对于这个定义,我们可以“分段”来理解一下。

  • Digital System

什么是TLA+眼中的数字系统(Digital System)?Lamport认为数字系统包括算法(Algorithms)、程序(Programs)和计算机系统(Computer system),它们有一个共同特点,那就是可以抽象为一个按离散事件序列(sequence of discrete events)进行持续执行和演进的物理系统,这是TLA+后续描述(specify)数字系统的基础。随着多核和云计算的兴起,并发程序和分布式的关键(critical)系统成为了TLA+的主要描述对象,这样的系统最复杂,最难正确实现,价值也最高,值得使用TLA+对其进行形式化的验证。

  • High Level

TLA+面向设计层面,在代码实现层面之上,实施于编写任何实现代码之前。此外,High Level也意味着可以忽略那些系统中不是很关键(less-critical)的部分以及低层次的实现细节。

去除细节进行简化的过程就是抽象(Abstraction),它是工程领域最重要的环节。抽象可以让我们理解复杂的系统,如果不了解系统,我们就无法对系统进行正确的建模并实现它。

而使用TLA+编写系统spec其实就是一个学习对系统进行抽象的过程,学会抽象思考,可以帮助工程师提高设计能力。

  • Modeling

TLA+是通过描述系统的行为(behavior)来对数字系统进行建模的。那么什么是系统的行为呢?如下图所示:


此图由claude sonnet 3.5根据我的prompt生成

行为被Lamport定义为一系列的状态(Sequence of States),这些状态仍然按顺序排列,表示系统随时间的演变。而状态本身则是对变量的赋值。状态之间的转换由动作(action)描述,而系统的正确性由属性(properties)指定。

这种方法特别适合建模并发和分布式系统,因为它允许我们精确地描述系统的所有可能行为,包括不同组件之间的交互和可能的竞争条件,如下图所示:

在TLA+中,属性(properties)是用来描述系统应该满足的条件或特性,它们在验证系统行为的正确性方面起着关键作用。我们所说的系统工作正常就是指这些在执行过程中的属性都得到了满足。

在TLA+中,有两类属性是我们特别需要关注的,一类是安全属性(Safety Properties),一类则是活性属性(Liveness Properties)。前者确保“坏事永远不会发生”,比如使用不变量在并发系统中确保两个进程不会同时进入临界区;后者则是确保“好事最终会发生”,在分布式系统中的最终一致性(eventual consistency)是一个活性属性,它保证系统最终会达到一致的状态。TLA+允许我们精确地指定这些属性,然后使用TLC模型检查器来验证系统是否满足这些属性。这种方法特别适合于复杂的并发和分布式系统,因为它能够发现在传统测试中难以发现的微妙错误。

注:关于TLA+可以用来形式化描述(specify)和验证(check)数字系统的底层数学理论,可以参考Lamport老爷子那本最新尚未完成的书籍A Science of Concurrent Programs(2024.6.7版)

接下来,我们就来看看TLA+究竟如何编写。不过直接介绍TLA+语法比较抽象和枯燥,在我读过的TLA+语法资料中,Lamport在The TLA+ Video Course第二讲中将一个C示例程序一步一步像数学推导一样转换为TLA+语法的讲解对我帮助非常大,我觉得有必要将这个示例放到这篇文章中。

3. 从C代码到TLA+:转换步骤详解

Lamport的这个过程展示了如何从一个具体的编程语言实现(以C代码为例)逐步抽象到一个数学化的、更加通用的系统描述。每一步都增加了抽象级别,最终得到一个可以用于形式化验证的TLA+规范(spec)。以下是这个演进过程的主要阶段:

3.1 初始C程序分析

下面是这个示例的原始C代码:

int i;
void main() {
    i = someNumber();
    i = i + 1;
}

这不是一个并发程序,它只有一个执行路线(execution),前面说过,一个行为(execution)是一个状态序列,我们就来定义这个状态序列以及它们之间的转换关系。

我们先识别出程序的状态变量:i以及引入的控制状态变量(PC),PC变量来表示程序的执行位置。接下来我们就来描述一个可以代码该程序所有状态的“状态机”。

3.2 状态机描述

该程序可以划分为三个状态:

  • 初始状态:i = 0, PC = “start”
  • 中间状态:i in {0, 1, …, 1000}(这里限定了someNumber函数返回的数值范围), PC = “middle”
  • 结束状态:i = i + 1, PC = “done”

下面用自然语言描述一下上述状态的转换关系:

if current value of pc equals "start"
    then next value of i in {0, 1, ..., 1000}
         next value of pc equals "middle"
    else if current value of pc equals "middle"
            then next value of i equals current value of i + 1
                 next value of pc equals "done"
            else no next values

接下来,我们就来将上述对于状态转换的描述变换一下,尽量用数学来表示。

3.3 转换为数学表示

这里的转换分为几步,我们逐一来看。

  • 换掉”current value of”
if pc equals "start"
    then next value of i in {0, 1, ..., 1000}
         next value of pc equals "middle"
    else if pc equals "middle"
            then next value of i equals i + 1
                 next value of pc equals "done"
            else no next values

替换后,pc即the current value of pc,i即current value of i。

  • 换掉”next value of”

我们用i’换掉”next value of i”, 用pc’换掉”next value of pc”,结果如下:

if pc equals "start"
    then i' in {0, 1, ..., 1000}
         pc' equals "middle"
    else if pc equals "middle"
            then i' equals i + 1
                 pc' equals "done"
            else no next values
  • 用”=”符号换掉equals

替换的结果如下:

if pc = "start"
    then i' in {0, 1, ..., 1000}
         pc' = "middle"
    else if pc = "middle"
            then i' = i + 1
                 pc' = "done"
            else no next values
  • 将in换为数学符号∈
if pc = "start"
    then i' ∈ {0, 1, ..., 1000}
         pc' = "middle"
    else if pc = "middle"
            then i' = i + 1
                 pc' = "done"
            else no next values

3.4 TLA+语法转换

  • 将集合表示换为正式的数学符号

{0, 1, …, 1000}并非数学表示集合的方式,替换后,结果如下:

if pc = "start"
    then i' ∈ 0..1000
         pc' = "middle"
    else if pc = "middle"
            then i' = i + 1
                 pc' = "done"
            else no next values

这里0..1000使用了TLA+的集合表示语法。

  • 转换为单一公式(formula)

将C代码转换为上面的最新代码后,你不要再按照C的语义去理解上述转换后的代码了。新代码并非是像C那样为了进行好一些计算而编写的一些指令,新代码是一个关于i、pc、i’和pc’的公式(formula),这是理解从C带TLA+的最为关键的环节,即上述这段代码整体就是一个公式

上述代码的意思并非if pc = “start”为真,然后执行then部分,否则执行else部分。其真正含义是如果pc = “start”为真,那么上述整个公式将等于then这个公式的值,否则整个公式将等于else公式的值。

不过我们看到在上面的then子句中存在两个独立的公式,以第一个then为例,两个独立公式分别为i’ ∈ 0..1000和pc’ = “middle”。这两个独立的公式之间是and的关系,我们需要将其转换为一个公式。TLA+中使用”/\”表示and连接,下面是使用”/\”将公式连接后的结果:

if pc = "start"
    then (i' ∈ 0..1000) /\
         (pc' = "middle")
    else if pc = "middle"
            then (i' = i + 1) /\
                 (pc' = "done")
            else no next values
  • 改造else公式

问题来了! 当存在某个状态,使得整个公式等于最后一个else公式的值时,我们发现这个值为”no next values”,而前面的then、else if then公式的值都为布尔值TRUE或FALSE。这里最后的ELSE公式,它的值应该为FALSE,无论i、pc、i’和pc’的值为什么,因此这里直接将其改造为FALSE:

if pc = "start"
    then (i' ∈ 0..1000) /\
         (pc' = "middle")
    else if pc = "middle"
            then (i' = i + 1) /\
                 (pc' = "done")
            else FALSE
  • TLA+的关键字为大写且TLA+源码为ASCII码

if、then、else 这些都是TLA+的关键字,而TLA+的关键字通常为大写,并且TLA+源码为ASCII码,∈需换成\in。这样改变后的结果如下:

IF pc = "start"
    THEN (i' \in 0..1000) /\
         (pc' = "middle")
    ELSE IF pc = "middle"
            THEN (i' = i + 1) /\
                 (pc' = "done")
            ELSE FALSE

到这里,我们就得到了一个美化后的的TLA+公式了!

3.5 干掉if else

前面说过,我们将C代码改造为了一个公式,但公式中依然有if else总是感觉有些格格不入,是不是可以干掉if else呢!我们来试一下!

我们先用A、B替换掉then语句中的两个公式:

IF pc = "start"
    THEN A
    ELSE IF pc = "middle"
            THEN B
            ELSE FALSE

如果整个公式为TRUE,需要(pc = “start”)和A都为TRUE,或(pc = “middle”)和B都为TRUE。TLA+引入一个操作符\/表示or,这样整个公式为TRUE的逻辑就可以表示为:

   ((pc = "start") /\ A)
\/ ((pc = "middle") /\ B)

好了,现在我们再把A和B换回到原先的公式:

   ((pc = "start") /\
    (i' \in 0..1000) /\
    (pc' = "middle"))
\/ ((pc = "middle") /\
    (i' = i+1 ) /\
    (pc' = "done"))

你是不是感觉不够美观啊!TLA+提供了下面等价的、更美观的形式:

\/ /\ pc = "start"
   /\ i' \in 0..1000
   /\ pc' = "middle"
\/ /\ pc = "middle"
   /\ i' = i+1
   /\ pc' = "done"

这种形式完全去掉了括号,并可以像列表一样表达公式!并且无论是/\还是\/都是可交换的(commutative),顺序不影响公式的最终结果。

3.6 完整的TLA+ spec

从数学层面,上面C代码将被拆分为两个公式,一个是初始状态公式,一个是下个状态的公式:

初始状态公式:(i = 0) /\ (pc = "start")
下一状态公式:
              \/ /\ pc = "start"
                 /\ i' \in 0..1000
                 /\ pc' = "middle"
              \/ /\ pc = "middle"
                 /\ i' = i+1
                 /\ pc' = "done"

但对于一个完整的TLA+ spec来说,还需要额外补充些内容:

---- MODULE SimpleProgram ----

EXTENDS Integers
VARIABLES i, pc

Init == (pc = "start") /\ (i = 0)
Next == \/ /\ pc = "start"
           /\ i' \in 0..1000
           /\ pc' = "middle"
        \/ /\ pc = "middle"
           /\ i' = i + 1
           /\ pc' = "done"
====

一个完整的TLA+ spec是放在一个module中的,上面例子中module为SimpleProgram。TLA toolkit要求tla文件名要与module名相同,这样上面代码对应的tla文件应为SimpleProgram.tla。

EXTENDS会导入TLA+内置的标准module,这里的Integers就提供了基础的算术运算符,比如+和..。

VARIABLES声明了状态变量,比如这里的i和pc。变量加上’即表示该变量的下一个状态的值。

接下来便是公式的定义。Init和Next并非固定公式名字,你可以选择任意名字,但使用Init和Next是惯用法。

“====”用于标识一个module的Body内容的结束。

对于上面简单的C程序,这样的spec是可以的。但在实际使用中,spec中的Next一般会很长,一个好的实践是对其进行拆分。比如这里我们就将Next拆分为两个子公式:Pick和Add1:

---- MODULE SimpleProgram ----

EXTENDS Integers
VARIABLES i, pc

Init == (pc = "start") /\ (i = 0)
Pick == /\ pc = "start"
        /\ i' \in 0..1000
        /\ pc' = "middle"
Add1 == /\ pc = "middle"
        /\ i' = i + 1
        /\ pc' = "done"
Next == Pick \/ Add1
====

4. 使用TLA+ Toolkit验证spec

Lamport提供了TLA+的Module Checker,我们可以从其主页提供的工具包下载链接下载TLA+ Toolkit。

先将上面的TLA+ spec存入一个名为SimpleProgram.tla的文件。然后打开TLA+ Toolkit,选择File -> Open spec -> Add New Spec…,然后选择你本地的SimpleProgram.tla即可加载该spec:

之后,我们可以点击菜单项“TLC Model Checker” -> New Model,便可以为该tla建立一个model配置(去掉deadlock),运行check后,你能看到下面结果:

我们看到model check一共检查了2003个不同的状态。

注:TLA+还提供了一个Visual Studio Code的扩展,也可以用来specify和check model。

5. 使用TLA+验证Go并发程序

Go语言因其强大的并发编程能力而备受青睐。然而,Go的并发方案虽然简单,但也并非银弹。随着并发程序复杂性的增加,开发者常常面临着难以发现和调试的错误,如死锁和竞态条件。这些问题不仅影响程序的正确性,还可能导致严重的系统故障。对于Go开发的并发系统的关键部分,采用TLA+进行形式化的验证是一个不错的提高系统正确性和可靠性的方法。

接下来,我们就建立一个生产者和消费者的Go示例,然后使用TLA+为其建模并check。理论上应该是先有设计思路,再TLA+验证设计,再进行代码实现,这里的Go代码主要是为了“描述”该并发程序的需求和行为逻辑。

// go-and-tla-plus/producer-consumer/main.go
package main

import (
    "fmt"
    "sync"
)

func producer(ch chan<- int, wg *sync.WaitGroup) {
    defer wg.Done()
    for i := 0; i < 5; i++ {
        ch <- i
    }
    close(ch)
}

func consumer(ch <-chan int, wg *sync.WaitGroup) {
    defer wg.Done()
    for num := range ch {
        fmt.Println("Consumed:", num)
    }
}

func main() {
    ch := make(chan int)
    var wg sync.WaitGroup
    wg.Add(2)

    go producer(ch, &wg)
    go consumer(ch, &wg)

    wg.Wait()
}

任何Go初学者都可以很容易读懂上面的程序逻辑:Producer生产0到4四个数,每生成一个就通过unbuffered channel发出,consumer从channel接收数字并消费。Producer生产完毕后,关闭channel。Consumer消费完所有数字后,退出,程序终止。

下面是使用TLA+编写的ProducerConsumer的完整Spec:

// go-and-tla-plus/producer-consumer/ProducerConsumer.tla

---- MODULE ProducerConsumer ----
EXTENDS Integers, Sequences

VARIABLES
    ch,           \* 通道内容
    produced,     \* 已生产的消息数
    consumed,     \* 已消费的消息数
    closed        \* 通道是否关闭

TypeOK ==
    /\ ch \in Seq(0..4)
    /\ produced \in 0..5
    /\ consumed \in 0..5
    /\ closed \in BOOLEAN

Init ==
    /\ ch = <<>>
    /\ produced = 0
    /\ consumed = 0
    /\ closed = FALSE

Produce ==
    /\ produced < 5
    /\ ch = <<>>
    /\ ~closed
    /\ ch' = Append(ch, produced)
    /\ produced' = produced + 1
    /\ UNCHANGED <<consumed, closed>>

Close ==
    /\ produced = 5
    /\ ch = <<>>
    /\ ~closed
    /\ closed' = TRUE
    /\ UNCHANGED <<ch, produced, consumed>>

Consume ==
    /\ ch /= <<>>
    /\ ch' = Tail(ch)
    /\ consumed' = consumed + 1
    /\ UNCHANGED <<produced, closed>>

Next ==
    \/ Produce
    \/ Close
    \/ Consume

Fairness ==
    /\ SF_<<ch, produced, closed>>(Produce)
    /\ SF_<<produced, closed>>(Close)
    /\ SF_<<ch>>(Consume)

Spec == Init /\ [][Next]_<<ch, produced, consumed, closed>> /\ Fairness

THEOREM Spec => []TypeOK

ChannelEventuallyEmpty == <>(ch = <<>>)
AllMessagesProduced == <>(produced = 5)
ChannelEventuallyClosed == <>(closed = TRUE)
AllMessagesConsumed == <>(consumed = 5)

====

这个Spec不算长,但也不短,你可能看不大懂,没关系,接下来我们就来说说从main.go到ProducerConsumer.tla的建模过程,并重点解释一下上述TLA+代码中的重要语法。

针对main.go中体现出来的Producer和Consumer的逻辑,我们首先需要识别关键组件:生产者、消费者和一个通道(channel),然后我们需要确定状态变量,包括:通道内容(ch)、已生产消息数(produced)、已消费消息数(consumed)、通道是否关闭(closed)。

接下来,我们就要定义action,即导致状态变化的step,包括Produce、Consume和Close。

最后,我们需要设置初始状态Init和下一个状态Next,并定义安全属性(TypeOK)和一些活性属性(如AllMessagesConsumed等)

现在,我们结合上述TLA+的代码,来说一下上述这些逻辑是如何在TLA+中实现的:

---- MODULE ProducerConsumer ----

这一行定义了模块名称,模块名称与文件名字(ProducerConsumer.tla)要一致,否则TLA+ Toolkit在Open Spec时会报错。

EXTENDS Integers, Sequences

这行会导入整数和序列模块,以使用相关运算符。

VARIABLES
    ch,           \* 通道内容
    produced,     \* 已生产的消息数
    consumed,     \* 已消费的消息数
    closed        \* 通道是否关闭

这里使用VARIBALES关键字定义了四个状态变量,整个TLA+程序的函数逻辑就围绕这四个变量进行,TLC Model check也是基于这些状态变量对TLA+ module进行验证。

TypeOK ==
    /\ ch \in Seq(0..4)
    /\ produced \in 0..5
    /\ consumed \in 0..5
    /\ closed \in BOOLEAN

定义不变量,确保变量状态在系统的所有行为过程中始终保持在合理范围内,该TypeOK不变量即是整个程序的安全属性。

Init ==
    /\ ch = <<>>
    /\ produced = 0
    /\ consumed = 0
    /\ closed = FALSE

这是初始状态的公式,对应了四个变量的初始值。

Produce ==
    /\ produced < 5
    /\ ch = <<>>
    /\ ~closed
    /\ ch' = Append(ch, produced)
    /\ produced' = produced + 1
    /\ UNCHANGED <<consumed, closed>>

这里定义了生产操作的公式,只有在produced < 5,ch为空且closed不为true时,才会生产下一个数字。这里设定ch为空作为前提条件,主要是为了体现Channel的unbuffered的性质。

Close ==
    /\ produced = 5
    /\ ch = <<>>
    /\ ~closed
    /\ closed' = TRUE
    /\ UNCHANGED <<ch, produced, consumed>>

这里定义了关闭操作的公式,这里的ch = <<>>子公式的目的是等消费完之后再关闭channel,当然这里与Go的机制略有差异。

Consume ==
    /\ ch /= <<>>
    /\ ch' = Tail(ch)
    /\ consumed' = consumed + 1
    /\ UNCHANGED <<produced, closed>>

这里定义了消费操作的公式,只有channel不为空,才进行消费。

Next ==
    \/ Produce
    \/ Close
    \/ Consume

这里基于三个操作公式定义了下一个状态(Next)的公式,使用\/运算符将这三个操作连接起来,表示下一步可以执行其中任意一个操作。

Fairness ==
    /\ SF_<<ch, produced, closed>>(Produce)
    /\ SF_<<produced, closed>>(Close)
    /\ SF_<<ch>>(Consume)

这里定义了公平性条件,确保各操作最终会被执行。

Spec == Init /\ [][Next]_<<ch, produced, consumed, closed>> /\ Fairness

这里定义了整个并发程序的规范,包括初始条件Init和下一步动作约束以及Fairness条件。/\连接的第二段Next表示系统的每一步都必须符合Next定义的可能动作,并且不会改变 <<ch, produced, consumed, closed>> 元组中变量之外的其他变量。Fairness 表示系统必须满足前面定义的 Fairness 条件。

THEOREM Spec => []TypeOK

这是一个定理,表示如果系统满足Spec规范,则一定会满足TypeOK这个不变量。其中的”=>”是蕴含的意思,A => B表示如果A为真,那么B必然为真。用一个例子可以解释这点,如果x > 3为真,那么 x > 1 必为真,我们可以将其写为:x > 3 => x > 1。

ChannelEventuallyEmpty == <>(ch = <<>>)
AllMessagesProduced == <>(produced = 5)
ChannelEventuallyClosed == <>(closed = TRUE)
AllMessagesConsumed == <>(consumed = 5)

这里定义了四个活性属性,用于在TLC Model check时验证最终状态使用,其中:ChannelEventuallyEmpty表示最终消息队列 ch 一定会为空;AllMessagesProduced表示最终一定会生产5条消息;ChannelEventuallyClosed表示最终消息队列一定会被关闭;AllMessagesConsumed表示最终一定会消费5条消息。

接下来,我们可以使用前面提到的TLA+ Toolbox来check该spec,下面是model的设置和model check的结果:


model设置


check结果

注:在VSCode中使用TLA+插件的Checker对上述tla进行check,会出现不满足活性属性的error结果。

6. 小结

在这篇文章中,我们从Lamport提供的C语言代码示例出发,一步步介绍了如何将其转换为TLA+ spec,并使用TLA+ Toolkit进行验证。然后我们又以一个Go语言的生产者-消费者并发程序为例,展示了如何使用TLA+对其进行建模和验证。

不过我必须承认,TLA+这种形式化验证语言是极小众的。对大多数程序员来说,可能没什么实际帮助。即便是在大厂,真正使用TLA+对分布式系统进行形式化验证的案例也很少。

但是,我认为TLA+仍然有其独特的价值:

  • 它迫使我们用更抽象和精确的方式思考系统设计,有助于发现潜在的问题。
  • 对于一些关键的分布式系统组件,使用TLA+进行验证可以极大地提高可靠性。
  • 学习TLA+的过程本身就是一次提升系统设计能力的过程。

当然,形式化方法并非万能。比如它无法解决性能退化等问题,也不能验证代码是否正确实现了设计。我们应该将其视为系统设计和验证的补充工具,而不是替代品。

总之,虽然TLA+可能不适合所有人,但对于那些构建复杂分布式系统的工程师来说,它仍然是一个值得学习和使用的强大工具。我希望这篇文章能为大家了解和入门TLA+提供一些帮助。

本文涉及的源码可以在这里下载 – https://github.com/bigwhite/experiments/blob/master/go-and-tla-plus

本文部分源代码由claude 3.5 sonnet生成。

7. 参考资料


Gopher部落知识星球在2024年将继续致力于打造一个高品质的Go语言学习和交流平台。我们将继续提供优质的Go技术文章首发和阅读体验。同时,我们也会加强代码质量和最佳实践的分享,包括如何编写简洁、可读、可测试的Go代码。此外,我们还会加强星友之间的交流和互动。欢迎大家踊跃提问,分享心得,讨论技术。我会在第一时间进行解答和交流。我衷心希望Gopher部落可以成为大家学习、进步、交流的港湾。让我相聚在Gopher部落,享受coding的快乐! 欢迎大家踊跃加入!

img{512x368}
img{512x368}

img{512x368}
img{512x368}

著名云主机服务厂商DigitalOcean发布最新的主机计划,入门级Droplet配置升级为:1 core CPU、1G内存、25G高速SSD,价格5$/月。有使用DigitalOcean需求的朋友,可以打开这个链接地址:https://m.do.co/c/bff6eed92687 开启你的DO主机之路。

Gopher Daily(Gopher每日新闻) – https://gopherdaily.tonybai.com

我的联系方式:

  • 微博(暂不可用):https://weibo.com/bigwhite20xx
  • 微博2:https://weibo.com/u/6484441286
  • 博客:tonybai.com
  • github: https://github.com/bigwhite
  • Gopher Daily归档 – https://github.com/bigwhite/gopherdaily

商务合作方式:撰稿、出书、培训、在线课程、合伙创业、咨询、广告合作。

Go测试的20个实用建议

本文永久链接 – https://tonybai.com/2024/01/01/go-testing-by-example

2023年11月初,Go语言技术负责人Russ Cox在GopherCon Australia 2023大会上进行了题为“Go Testing By Example”的演讲:

12月初Russ Cox重新录制了该演讲内容的视频,并在个人网站上放了出来。这个演讲视频是关于如何编写好的Go测试的,Russ Cox介绍了20个实用建议,非常值得Go初学者甚至Go资深开发者学习并应用到实践中。这里是基于该视频整理的文字稿(可能并非逐字逐句),供广大Gopher参考。

注:在GopherCon Australia 2023,退休后暂定居澳大利亚的Go语言之父Rob Pike也做了一个名为“What We Got Right, What We Got Wrong”的主题演讲。在Go开源14年之后,有很多事情值得思考。这个演讲“事后诸葛亮般地”探讨了Go迄今为止取得的一些经验教训:不仅包括进展顺利的方面,还包括本可以做得更好的方面。可惜目前该演讲视频或文字稿并未放出,我们也只能等待。


大家好!这是几周前我在GopherCon Australia 2023进行的一次演讲,演讲的内容是关于如何编写好的测试。

不过首先让我们来思考一下为什么我们要编写测试。一些有关编程的书中常讲到:测试是为了发现程序中的错误!比如Brian W. Kernighan和Rob Pike合著的《The Practice of Programming》一书中讲到:“测试是一种坚定的、系统地尝试,旨在破坏你认为可以正确运行的程序”。这是真实的。这就是为什么程序员应该编写测试。但对于今天在这里的大多数人来说,这不是我们编写测试的原因,因为我们不仅仅是程序员,我们是软件工程师。什么意思呢?我想说的是,软件工程就是当你编程时增加时间和其他程序员时所发生的事情。编程意味着让程序运行,你有一个问题需要解决,你编写一些代码,运行它,测试它,调试它,得到答案,你就完成了。这本已经相当困难了,而测试是该过程的重要组成部分。但软件工程意味着你在长期与其他人一起开发的程序中完成所有这些工作,这改变了测试的性质。

让我们先看一个对二分查找函数的测试:

如图所示,这个函数接受一个有序(sorted)切片、一个目标值(target)和一个比较函数(cmp)。它使用二分搜索算法查找并返回两个内容:第一,如果目标存在,则返回其索引(index),第二是一个布尔值,指示目标是否存在。

大多数二分查找算法的实现都有错误,这个也不例外。我们来测试一下。

下面是一个很好的二分搜索的交互式测试:

你输入两个数字n和t,测试程序便创建一个包含n个元素的切片,其元素值按10倍增,然后程序在切片中搜索t并打印结果,然后你反复重复这一过程。

这可能看起来不足为奇,但有多少人曾经通过运行这种交互式测试程序来测试生产环境用的代码(production code)?我们所有人都这样做过。当你独自编程时,像这样的交互式测试程序对于查找bug非常有用,到目前为止代码看起来可以正常工作。

但这个交互式测试程序只适合独自编程时使用,如果你从事软件工程,意味着你要长时间保持程序的运行,并与其他人合作,那么这种类型的测试程序就不太有用了。

你需要一种每个人都可以在日常工作中运行的测试程序,可以在他们编写代码的同时运行,并且可以由计算机在每次代码提交时自动运行。问题在于仅通过手动测试程序只能确保它在今天正常工作,而自动化、持续的测试可以确保它在明天和未来都可以正常工作,即使其他不熟悉这段代码的人开始对其进行维护。并且我们要明确一点:那个不太熟悉代码的人可能是指未来六个月甚至六周后的你。

这是一个软件工程师的测试。你可以在不了解代码工作原理的情况下运行它。任何同事或任何计算机都可以使用”go test”运行该测试,并可以立即知道该测试是否通过。我肯定你已经见过这样的测试了。

软件工程的理想是拥有能够捕捉到后续可能出现的所有错误的测试。如果你的测试达到了这个理想状态,那么当你的所有测试都通过时,你应该可以放心地自动将你的代码部署到生产环境中,这就是人们所称的持续部署。如果你还没有这样做,如果这个想法让你感到紧张,那么你应该问问自己为什么。要么你的测试已经足够好,要么它们还不够好。如果它们足够好,那为什么不这样做呢?而如果它们不够好,那就倾听这些疑虑,并找出它们告诉你哪些测试被遗漏了。

几年前,我正在为新的Go官方网站go.dev编写代码。那时我们还在手动部署该网站,并且至少每周一次。我做的一项代码变更在我的机器上运行正常,但在部署到生产环境后便无法正常工作了,这着实令人非常烦恼和尴尬。解决办法是进行更好的测试和自动化的持续部署。现在,每当代码库中有新的提交时,我们使用一个Cloud Build程序来运行本地测试,并将代码推送到一个全新的服务器,然后运行一些只能在生产环境中运行的测试。如果一切正常,我们会将流量打到新的服务器。这样做改善了两点。首先,我不再导致令人尴尬的网站宕机。其次,每个人都不再需要考虑如何部署网站。如果他们想做变更,比如修复拼写错误或添加新的博客文章,他们只需发送更改请求,对其进行审核、测试和提交,然后自动化流程会完成其余工作。

要确信当其他人更改代码时你的程序不会出错,要确信只要测试通过就可以随时将程序推送到生产环境,你需要一套非常好的测试。但是什么样的测试才算是好的呢?

一般来说,使测试代码优秀的因素与使非测试代码优秀的因素是相同的:勤奋(hard work)、专注(attention)和时间(time)。对于编写优秀的测试代码,我没有什么“银弹式”的或硬性的规则,就像编写优秀的非测试代码一样。然而,我确实有一系列基于我们在Go上的良好实践的建议,我将在这次演讲中分享20个编写优秀测试代码的实用建议。

建议1:让添加新测试用例变得容易

这是最重要的建议。因为如果添加一个新测试用例很困难,你就不会去做。在这方面,Go已经提供了很好的支持。

上图是函数Foo的一个最简单的测试。我们专门设计了Go测试,使其非常容易编写。没有繁杂的记录或仪式会妨碍你。在包级别的测试中,这已经相当不错了,但在特定的包中,你可以做得更好。

我相信你已经了解了表驱动测试。我们鼓励使用表驱动测试,因为它们非常容易添加新的测试用例。这是我们之前看到的那个测试用例:假设我们只有这一个测试用例,然后我们想到了一个新的测试用例。我们根本不需要编写任何新的代码,只需要添加一行新的数据。如果目标是“使添加新的测试用例变得容易”,那么对于像这样的简单函数,向表中添加一行数据就足够了。不过,这也引出了一个问题:我们应该添加哪些测试用例?这将引导我们来到下一个建议。

建议2:使用测试覆盖率来发现未经测试的代码

毕竟,测试无法捕捉到未运行的代码中的错误。Go内置了对测试覆盖率的支持。下面是它的样子:

你可以运行“go test -coverprofile”来生成一个覆盖率文件,然后使用“go tool cover”在浏览器中查看它。在上图的显示中,我们可以看到我们的测试用例还不够好:实际的二分查找代码是红色的,表示完全未经测试。下一步是查看未经测试的代码,并思考什么样的测试用例会使这些代码行运行。

经过仔细检查,我们只测试了一个空切片,所以让我们添加一个非空的切片的测试用例。现在我们可以再次运行覆盖率测试。这次我将用我写的一个小命令行程序“uncover”来读取覆盖率文件。Uncover会显示未被测试覆盖的代码行。它不会给你网页视图那样的全局视图,但它可以让你保持在一个终端窗口中。Uncover向我们展示了只剩下一行代码未被测试执行。这是进入切片的第二半部分的行,这是有道理的,因为我们的目标是第一个元素。让我们再添加一个测试,搜索最后一个元素。

当我们运行测试时,它通过了,我们达到了100%的覆盖率。很棒。我们完成了吗?没有,这将引导我们到下一个实用建议。

建议3:覆盖率不能替代思考

覆盖率对于指出你可能忽略的代码部分非常有用,但机械工具无法替代对于高难度的输入、代码中的微妙之处以及可能导致代码出错的情况进行的实际思考。即使代码拥有100%的测试覆盖率,仍然可能存在bug,而这段代码就存在bug。这个提示也适用于覆盖率驱动的模糊测试(fuzzing test)。模糊测试只是尝试通过代码探索越来越多的路径,以增加覆盖率。模糊测试也非常有帮助,但模糊测试也不能替代思考。那么这里缺少了什么呢?

需要注意的一点是,唯一一个无法找到目标的测试用例是一个空输入切片。我们应该检查在具值的切片中无法找到目标的情况。具体来说,我们应该检查当目标小于所有值、大于所有值和位于值的中间时会发生什么。所以让我们添加三个额外的测试用例。

注意添加新测试用例是多么容易。如果你想到一个你的代码可能无法正确处理的情况,添加该测试用例应该尽可能简单,否则你就会觉得麻烦而不去添加。如果太困难,你就不会添加。你还可以看到我们正在开始列举这个函数可能出错的所有重要路径。这些测试对未来的开发进行了约束,以确保二分查找至少能够正常工作。当我们运行这些测试时,它们失败了。返回的索引i是正确的,但表示target是否找到的布尔值是错误的。所以让我们来看看这个问题。

阅读代码,我们发现返回语句中的布尔表达式是错误的。它只检查索引是否在范围内。它还需要检查该索引处的值是否等于target值。所以我们可以进行这个更改,如图所示,然后测试通过了。现在我们对这个测试感到非常满意:覆盖率是良好的,我们也经过了深思熟虑。还能做什么呢?

建议4:编写全面的测试

如果你能够测试函数的每一个可能输入,那就应该这样做。但现实中可能无法做到,但通常你可以在一定约束条件下测试特定数量以内的所有输入。下面是一个二分查找的全面测试:

我们首先创建一个包含10个元素的切片,具体来说就是从1到19的奇数。然后我们考虑该切片的所有可能长度的前缀。对于每个前缀,我们考虑从0到两倍长度的所有可能目标,其中0是小于切片中的所有值,两倍长度是大于切片中的所有值。这将详尽地测试每个可能的搜索路径,以及长度不超过我们的限制10的所有可能尺寸的切片。但是现在我们怎么知道答案是什么呢?我们可以根据测试用例的具体情况进行一些数学计算,但有一种更好、更通用的方法。这种方法是编写一个与真正实现不同的参考实现。理想情况下,参考实现应该明显是正确的,但它只需与真实实现采用不同的方法即可。通常,参考实现将是一种更简单、更慢的方法,因为如果它更简单和更快,你会将其用作真正的实现。在这种情况下,我们的参考实现称为slowFind。测试检查slowFind和Find是否可以在答案上达成一致。由于输入很小,slowFind可以采用一个简单的线性搜索。

通过生成所有可能的输入并将结果与简单的参考实现进行比较,这种模式非常强大。它做的一件重要的事情是覆盖了所有基本情况,例如0个元素的切片、1个元素的切片、长度为奇数的切片、长度为偶数的切片、长度为2的幂的切片等等。大多数程序中的绝大多数错误都可以通过小规模的输入进行重现,因此测试所有小规模的输入非常有效。事实证明,这个全面测试通过了。我们的思考相当不错。

现在,如果全面测试失败,那意味着Find和slowFind不一致,至少有一个有bug,但我们不知道是哪一个有问题。添加一个直接测试slowFind会有所帮助,而且很容易,因为我们已经有了一个测试数据表。这是表驱动测试的另一个好处:可以使用这些表来测试多个实现。

建议5:将测试用例与测试逻辑分开

在表驱动测试中,测试用例在表中,而处理这些测试用例的循环则是测试逻辑。正如我们刚才所看到的,将它们分开可以让你在多个上下文中使用相同的测试用例。那么现在我们的二分查找函数完成了吗?事实证明没有,还有一个bug存在,这引导我们到下一个问题。

建议6:寻找特殊情况

即使我们对所有小规模情况进行了全面测试,仍然可能存在潜在的bug:

现在,这里再次展示了代码。还剩下一个bug。你可以暂停视频,花一些时间来查看它。

有人看出bug在哪里了吗?如果你没有看到,没关系。这是一个非常特殊的情况,人们花了几十年的时间才注意到它。Knuth告诉我们,尽管二分查找在1946年发表,但第一个正确的二分查找实现直到1964年才发表。但是这个bug直到2006年才被发现。

bug是这样的,如果切片中的元素数量非常接近int的最大值,那么i+j会溢出,因此i+j/2就不是切片中间位置的正确计算方法了。这个bug于2006年在一个使用64位内存和32位整数的C程序中被发现,这个程序用于索引包含超过10亿个元素的数组。在Go语言中,这种特定组合基本上不会发生,因为我们要求使用64位内存时,也要使用64位整数,这正是为了避免这种bug。但是,由于我们了解到这个bug,而且你永远不知道你或其他人将来如何修改代码,所以避免这个bug是值得的。

有两种常见的修复方法可以避免数学计算溢出。速度稍快的方法是进行无符号除法。假设我们修复了这个问题。现在我们完成了吗?不。因为我们还没有编写测试。

建议7:如果你没有添加测试,那就没有修复bug

这句话在两个不同的方面下都是正确的。

第一个是编程方面。如果你没有进行测试,bug可能根本没有被修复。这听起来可能很愚蠢,但你有多少次遇到过这种情况?有人告诉你有一个bug,你立即知道修复方法。你进行了更改,并告诉他们问题已经修复。然后他们却回来告诉你,不,问题还存在。编写测试可以避免这种尴尬。你可以说,很抱歉我没有修复你的bug,但我确实修复了一个bug,并会再次查看这个问题。

第二个是软件工程方面,即“时间和其他程序员”的方面。bug并不是随机出现的。在任何给定的程序中,某些错误比其他错误更有可能发生。因此,如果你犯了一次这个错误,你或其他人很可能在将来再次犯同样的错误。如果没有测试来阻止它们,bug就会重新出现。

现在,这个特定的测试很难编写,因为输入范围非常大,但即使测试很难编写,这个建议仍然成立。实际上,在这种情况下,这个建议通常更为正确。

为了测试这种情况,一种可能性是编写一个仅在32位系统上运行的测试,对两千兆字节的uint8进行二分查找。但这需要大量的内存,并且我们现在已经没有多少32位系统了。对于测试这种难以找到的bug,通常还有更巧妙的解决方案。我们可以创建一个空结构体的切片,无论它有多长,都不会占用内存。这个测试在一个包含MaxInt个空结构体的切片上调用Find函数,寻找一个空结构体作为目标,但是它传入了一个总是返回-1的比较函数,声称切片元素小于目标。这将使二分查找探索越来越大的切片索引,从而导致溢出问题。如果我们撤销我们的修复并运行这个测试,那么测试肯定会失败。

而使用了我们的修复后,测试通过了。现在bug已经修复了。

建议8:并非所有东西都适合放在表中

这个特殊情况不适合放在表中,但这没关系。但是很多东西确实适合放在表中。

这是我最喜欢的一个测试表之一。它来自fmt.Printf的测试用例。每一行都是一个printf格式、一个值和预期的字符串。真实的表太大了,无法放在幻灯片上,但这里摘录了一些表中的代码行。

如果你仔细阅读整个表,你会看到其中一些明显是修复bug的内容。记住建议7:如果你没有添加测试,那就没有修复bug。表格使得添加这些测试变得非常简单,并且添加这些测试可以确保这些bug不会再次出现。

表格是将测试用例与测试逻辑分离并且方便添加新的测试用例的一种方法,但有时你会有很多测试,甚至写Go语法的开销也是不必要的。例如,这里是strconv包的一个测试文件,用于测试字符串与浮点数之间的转换。你可能认为编写解析器来处理这个输入太麻烦了,但一旦你知道了如何处理,其实并不需要太多工作,而且定义测试专用的小型语言实际上非常有用。

因此,我将快速介绍一下解析器,以展示它并不复杂。我们读取文件,然后将其分割成行。对于每一行,我们计算错误消息的行号。切片元素0表示第1行。我们去掉行尾的任何注释。如果行为空白行,我们跳过它。到目前为止,这是相当标准的样板代码。现在是重点。我们将行分割为字段,并提取出四个字段。

然后根据类型字段在float32或float64的数学运算中进行转换。myatof64基本上是strconv.ParseFloat64的变体,不同之处在于它处理允许我们按照从论文中复制的方式编写测试用例的十进制p格式。

最后,如果结果不是我们想要的,我们打印错误。这非常类似于基于表格的测试。我们只是解析文件,而不是遍历表格。它无法放在一个幻灯片上,但在开发时它可以放在一个屏幕上。

建议9:测试用例可以放在testdata文件中

测试不必都要放在源代码中。

作为另一个例子,Go正则表达式包包含了一些从AT&T POSIX正则表达式库复制过来的testdata文件。我不会在这里详细介绍,但我很感激他们选择为该库使用基于文件的测试,因为这意味着我可以重用testdata文件,将其用于Go。这是另一种ad-hoc格式,但它易于解析和编辑。

建议10:与其他实现进行比较

与AT&T正则表达式的测试用例进行比较有助于确保Go的包以完全相同的方式处理各种边缘情况。我们还将Go的包与C++的RE2库进行比较。为了避免需要编译C++代码,我们以记录所有测试用例的方式运行它,并将该文件作为testdata提交到Go中。

在文件中存储测试用例的另一种方法是使用成对的文件,一个用于输入,一个用于输出。为了实现go test -json,有一个名为test2json的程序,它读取测试输出并将其转换为JSON输出。测试数据是成对的文件:测试输出和JSON输出。

这是最简短的文件。测试输出位于顶部,它是test2json的输入,应该生成底部的JSON输出。以下是实现,展示了从文件中读取测试数据的惯用方法。

我们首先使用filepath.Glob查找所有的testdata。如果失败或找不到任何文件,我们会报错。否则,我们循环遍历所有文件。对于每个文件,我们通过获取基本文件名(不包括testdata/目录名和文件后缀)来创建子测试名称。然后我们用该名称运行一个子测试。如果你的测试用例足够复杂,每个文件一个子测试通常是有意义的。这样,当一个测试用例失败时,你可以使用go test -run只运行特定的文件。

对于实际的测试用例,我们只需要读取文件,运行转换器,并检查结果是否匹配。对于检查,我最开始使用了bytes.Equal,但随着时间的推移,编写一个自定义的diffJSON函数来解析两个JSON结果并打印实际差异的详细说明变得更有价值。

建议11:使测试失败易读

回顾一下,我们已经在二分查找中看到了这一点。

我认为我们都同意粉色框不是一个好的失败。但是黄色框中有两个细节使得这些失败尤为出色。首先,我们在单个if语句中检查了两个返回值,然后在简洁的单行中打印了完整的输入和输出。其次,我们不会在第一个失败处停止。我们使用t.Error而不是t.Fatal,以便执行更多的测试用例。结合起来,这两个选择让我们可以看到每个失败的完整细节,并在多个失败中寻找模式。

回到test2json,这是它的测试失败的情况。它计算出哪些事件是不同的,并清晰地标记它们。重要的是,在你编写测试时,你不必写这种复杂的代码。bytes.Equal在开始时是可以的,并且可以专注于代码。但是随着失败变得更加微妙,并且你发现自己花费太多时间只是阅读失败输出,这是一个好的信号,它告诉你是时候花一些时间使其更易读了。此外,如果确切的输出发生更改并且你需要更正所有的测试数据文件,这种类型的测试可能会有点麻烦。

建议12:如果答案可能会改变,编写代码来更新它们

通常的做法是在测试中添加一个“-update”标志。这是test2json的更新代码示例。

测试定义了一个新的“-update标志”。当标志为true时,测试将计算的答案写入答案文件,而不是调用diffJSON。现在,当我们对JSON格式进行有意的更改时,“go test -update”会更新所有答案。你还可以使用版本控制工具如“git diff”来审查更改,并在看起来不正确时撤销更改。在谈论测试文件的主题上,有时将一个测试用例分割成多个文件会很烦人。如果我今天编写这个测试,我就不会这样做。

建议13: 使用txtar进行多文件测试用例

注:导入txtar:import “golang.org/x/tools/txtar”

Txtar是我们几年前专门为解决多文件测试用例问题而设计的一种新的存档格式。其Go解析器位于golang.org/x/tools/txtar中,我还找到了用Ruby、Rust和Swift编写的解析器。

Txtar的设计有三个目标。首先,足够简单,可以手动创建、编辑和阅读。其次,能够存储文本文件的树形结构,因为我们在go命令中需要这个功能。第三,能够在git历史记录和代码审查中进行良好的差异比较。其他的包括成为完全通用的存档格式、存储二进制数据、存储文件模式(file mode)、存储符号链接等都不是目标,因为存档文件(archived file)格式往往变得十分复杂,而复杂性与第一个目标直接相矛盾。这些目标和非目标导致了一个非常简单的格式。下面是一个示例:txtar文件以注释开头。

本例中为”Here are some greetings.”,然后通常会有零个或多个文件,每个文件由形如”– 文件名 –”的行引入。这个存档包含两个单行文件,hello和g’day。就是这样,这就是整个格式。没有转义,没有引用,没有对二进制数据的支持,没有符号链接,没有可能的语法错误,没有复杂之处。下面是一个在测试数据中使用txtar文件的真实示例。

该测试数据用于计算差异的包:在这种情况下,注释对于人们来说很有用,用于记录正在进行的测试,然后在这个测试中,每个用例由两个文件和它们的差异后面跟随的两个文件组成。

使用txtar文件几乎和编写它们一样简单。下面是我们之前查看的diff包的测试。

这是通常的基于文件的循环,但我们在文件上调用了txtar.ParseFile。然后我们坚持认为存档包含三个文件,第三个文件的名称为diff。然后我们对两个输入文件进行差异比较,并检查结果是否与预期的差异匹配。

这就是整个测试。你可能已经注意到,在使用之前,文件数据会被传递给”clean”函数进行清理。clean函数允许我们在不使txtar格式本身复杂化的情况下添加一些特定于diff的扩展。

第一个扩展处理以空格结尾的行,在差异中确实会出现这种情况。许多编辑器希望去除这些尾随空格,因此测试允许在txtar的数据行末尾放置$,并且clean函数会删除该$。在这个示例中,标记的行需要以一个空格结尾。

此外,txtar要求文件中的每一行都以换行符结尾,但我们希望测试diff在不以换行符结尾的文件上的行为。因此,测试允许在结尾处放置一个字面意义上的“尖号D”。clean函数会删除“尖号D”和其后的换行符。在这种情况下,’new’文件最终没有最后的换行符,而diff正确报告了这一点。因此,尽管txtar非常简单,你也可以轻松地在其上添加自己的格式调整。当然,重要的是要记录这些调整,以便下一个参与测试的人能够理解它们。

建议14:对现有格式进行注解(annotation)来创建测试迷你语言

对现有格式进行注释,比如在txtar中添加$和尖号D,是一个强大的工具。

这里是对现有格式进行注释的一个示例。这是Go类型检查器(type checker)的一个测试。这是一个普通的Go输入文件,但是期望的类型错误已经以/*ERROR*/注释的形式添加了进去。我们使用/*注释,这样我们就可以将它们放置在错误报告的确切位置上。测试运行类型检查器,并检查它是否在预期位置产生了预期的消息,并且没有产生任何意外的消息。下面是类型检查器的另一个示例。

在这个测试中,我们在通常的Go语法之上添加了一个assert注释。这使我们能够编写常量算术的测试,就像这个例子一样。类型检查器已经计算了每个常量表达式的布尔值,所以检查assert其实只是检查常量是否被求值为true。下面是另一个带有注释的格式示例。

Ivy是一个交互式计算器。你输入程序,通常是简单的表达式,它会打印出答案。测试用例是看起来像这样的文件:未缩进的行是Ivy的输入,缩进的行是注释,指示Ivy应该打印出预期的输出。编写新的测试用例再也没有比这更简单的了。这些带注释的格式扩展了现有的解析器和打印器(printer)。有时编写自己的解析器和打印器是有帮助的。毕竟,大多数测试涉及创建或检查数据,当你可以使用方便的形式处理数据时,这些测试总是可以更好。

建议15:编写解析器和打印器来简化测试

这些解析器和打印器不一定是用于testdata中数据文件的独立脚本。你也可以在常规的Go代码中使用它们。

这是一个运行deps.dev代码的一个测试片段。这个测试设置了一些数据库表行。它调用了一个使用数据库并正在进行测试的函数。然后它检查数据库是否包含了预期的结果。Insert和Want调用使用了一个专门为这些测试编写的用于数据库内容的迷你语言。解析器就像它看起来的那样简单:它将输入分割成行,然后将每行分割成字段。第一行给出了列名。就是这样。这些字符串中的确切间距并不重要,但是如果它们都对齐,当然看起来更美观。

因此,为了支持这个测试,deps.dev团队还有一个专门为这些测试编写的代码格式化程序。它使用Go标准库解析测试源代码文件。然后它遍历Go语法树,查找Insert或Want的调用。它提取字符串参数并将它们解析为表格。然后它将表格重新打印为字符串,将字符串重新插入语法树中,并重新打印语法树为Go源代码。这只是gofmt的一个扩展版本,使用了与gofmt相同的包。我这里不会展示这些代码,但代码量其实不多。

解析器和打印器需要花费了一些时间来编写。但现在,每当有人编写一个测试时,编写测试就更容易了。每当一个测试失败或需要更新时,调试也更容易了。如果你正在进行软件工程,收益将随着程序员数量和项目生命周期的增加而扩大。对于deps.dev来说,已经花费在这个解析器和打印器上的时间已经多次节省了。或许更重要的是,因为测试更容易编写,你可能会写更多的测试,这将导致更高质量的代码。

建议16:代码质量受测试质量限制

如果你不能编写高质量的测试,你将无法编写足够的测试,并且最终无法得到高质量的代码。

现在我想向你展示一些我曾经参与的最高质量的测试,这些测试是针对go命令的测试。它们将我们到目前为止看到的许多思想汇集在一起。这是一个简单但真实的go命令测试。这是一个txtar输入,其中包含一个名为hello.go的文件。archive comment是一个逐行简单命令语言编写的脚本。在脚本中,”env”设置一个环境变量来关闭Go module机制。井号引入注释。而”go”运行go命令,它应该运行hello world。该程序应该将hello world打印到标准错误中。”stderr”命令检查前一个命令打印的标准错误流是否与正则表达式匹配。因此,这个测试运行”go run hello.go”并检查它是否将hello world打印到标准错误中。

这里是另一个真实的测试。请注意底部的a.go是一个无效的程序,因为它导入了一个空字符串。第一行开头的感叹号是一个”非”操作符。NOT go list a.go意味着go list a.go应该失败。下一行的”NOT stdout .”表示标准输出不应该有与正则表达式”.”匹配的内容,也就是不应该打印任何文本。接下来,标准错误流应该有一个无效的导入路径的消息。最后,不应该发生panic。

建议17:使用脚本可以编写很好的测试

这些脚本使添加新的测试用例变得非常容易。

这是我们最小的测试用例:两行代码。最近我在破坏了unknown command的错误消息后添加了这个测试用例。总共,我们有超过700个这样的脚本测试,从两行到500多行不等。

这些测试脚本取代了一个更传统的使用方法(method)的测试框架。这张幻灯片展示了其中一个真实的测试,前面是脚本编写的测试用例,后面是等价的Go编写的传统测试代码。细节并不重要,只需注意脚本要比传统测试方法更容易编写和理解。

建议18:尝试使用rsc.io/script来创建基于脚本的测试用例

距离我们创建go脚本测试已经过去了大约五年时间,我们对这个特定的脚本引擎非常满意。Bryan Mills花了很多时间为它提供了一个非常好的API,早在11月份,我将其发布到了rsc.io/script以供导入使用。现在我说”尝试”是因为它还比较新,并且具有讽刺意味的是,它本身的测试还不够多,因为可导入的包只有几周的历史,但你仍然可能会发现它很有用。当我们对其有更多经验时,我们可能会将其放在更官方的位置上。如果你尝试了它,请告诉我结果如何。

提取脚本引擎的动机是为了在go命令测试的不同部分中重用它。这个脚本正在准备一个包含我们想要在常规go命令脚本测试中导入的模块的Git存储库(repo)。你可以看到它设置了一些环境变量,运行了真正的git init,设置了时间,在存储库中运行了更多的git命令来添加一个hello world文件,然后检查我们得到了我们想要的存储库。再一次,测试并不是从一开始就是这样的,这引出了下一个实用建议。

建议19:随着时间的推移改进你的测试

最初,我们没有这些存储库脚本。我们手工创建小型测试存储库,并将它们发布到GitHub、Bitbucket和其他托管服务器,具体取决于我们所需的版本控制系统。这种方法还算可以,但这意味着如果这些服务器中的任何一个宕机,测试就会失败。最终,我们花时间构建了自己的云服务器,可以为每个版本控制系统提供存储库服务。现在,我们手工创建存储库,将其压缩并复制到服务器上。这样做更好,因为现在只有一个服务器可能会使我们的测试失败,但有时也会出现网络问题。测试存储库本身也没有进行版本控制,并且与使用它们的测试不在一起,这也是一个问题。作为测试的一部分,基于脚本的版本完全可以在本地构建和提供这些存储库。而且现在很容易找到、更改和审查存储库的描述。这需要很多基础设施,但也测试了很多代码。如果你只有10行代码,你完全不需要拥有数千行的测试框架。但是如果你有十万行代码,这大约是go命令的规模,那么开发几千行代码来改进测试,甚至是一万行代码,几乎可以肯定是一个不错的投资。

建议20:追求持续部署

也许出于策略原因,你无法每次都实际部署那些通过了所有测试的代码提交,但无论如何都要追求这一目标。正如我在演讲开始时提到的,对于持续部署的任何疑问都是有益的小声音,它们告诉你需要更好的测试。而更好的测试的关键当然是让添加新测试变得容易。即使你从未实际启用持续部署,追求这一目标也可以帮助你保持诚实,提高测试的质量和代码的质量。

我之前提到过Go官方网站使用了持续部署。在每次提交时,我们运行测试来决定是否可以部署最新版本的代码并将流量路由到它。此时,你不会感到惊讶,我们为这些测试编写了一个测试脚本语言。上图是它们的样子。每个测试以一个HTTP请求开始。这里我们GET主页go.dev。然后对响应进行断言。每个断言的形式为”字段(field),运算符(operator),值(value)”。这里字段(field)是body,运算符(operator是contains,值(value)是body中必须包含的字面值。这个测试检查页面是否渲染过了,因此它检查基本文本以及一个副标题。为了更容易编写测试,根本没有引号。值就是运算符后面的其余部分。接下来是另一个测试用例。出于历史原因,/about需要重定向到pkg.go.dev。

这是另一个案例。这里没有什么特别的,只是检查案例研究页面是否渲染(rendering)了,因为它是由许多其他文件合成的。测试可以检查的另一个字段是HTTP响应代码,这是一个错误修复。我们错误地在Go存储库根目录中提供了这些文件,就好像它们是Go网站页面一样。我们希望改为返回404。你还可以测试标头foo的值,其中foo是某个标头。在这种情况下,标头Content-Type需要正确设置为主博客页面及其JSON feed。

这是另一个示例。这个示例使用正则表达式匹配运算符tilde和“\s+”语法,以确保页面具有正确的文本,无论单词之间有多少空格。这变得有点老套了,所以我们添加了一个名为trimbody的新字段,它是将所有空格序列替换为单个空格后的body。这个示例还显示了值可以作为多个缩进的行提供,以便更容易进行多行匹配。

我们还有一些无法在本地运行但在生产环境中仍值得运行的测试,因为我们将实时流量迁移到服务器之前需要进行这些测试。下面是其中两个。这些依赖于对生产环境playground后端的网络访问。这些案例除了URL不同之外都是相同的。这不是一个非常易读的测试,因为这些是我们唯一的POST测试。如果我们添加了更多这样的测试,我可能会花时间使它们看起来更好,以随着时间推移改进你的测试。但是现在它们还可以,它们起到了重要的作用。

最后,和往常一样,添加错误修复很容易。在问题51989中,live web站点根本没有呈现。因此,这个测试检查页面确实呈现并包含一个独特的文本片段。问题51989不会再次发生,至少不会在实际的网站上。肯定会有其他错误,但那个问题已经彻底解决了,这就是进步。以上这些是我有时间向你展示的这些例子。

小结

最后一个想法。我相信你经历过追踪错误并最终发现一个重要的代码片段是错误的情况。但不知何故,这个代码片段的错误大部分时间都无关紧要,或者错误被其他错误的代码抵消了。你可能会想:“这段代码以前是怎么工作的?”如果是你自己编写的代码,你可能会认为自己很幸运。如果是别人编写的代码,你可能会对他们的能力产生质疑,然后又认为他们很幸运。但是,大多数时候,答案并不是运气。对于这段代码为什么会工作的问题的答案几乎总是:因为它有一个测试。当然,代码是错误的,但测试检查了它足够正确,使系统的其他部分可以正常工作,这才是最重要的。也许编写这段代码的人确实是一个糟糕的程序员,但他们是一个优秀的软件工程师,因为他们编写了一个测试,这就是为什么包含该代码的整个系统能够工作的原因。

我希望你从这次演讲中得出的结论不是任何特定测试的具体细节,尽管我希望你可以留意对小型解析器和打印机的良好使用带来的好处。任何人都可以学会编写它们,并且有效地使用它们可以成为软件工程的超能力。最终,这对这些软件包来说是好测试。对于你的软件包,好测试可能看起来会有所不同。这没关系。但要使添加新的测试用例变得容易,并确保你拥有良好、清晰、高质量的测试。请记住,代码质量受测试质量的限制,因此逐步投入改进测试。你在项目上工作的时间越长,你的测试就应该变得越好。并且要追求持续部署,至少作为一种思想实验,以了解哪些方面的测试还不够充分。

总的来说,要像编写优秀的非测试代码一样,思考并投入同样的思想、关心和努力来编写优秀的测试代码,这绝对是值得的


“Gopher部落”知识星球旨在打造一个精品Go学习和进阶社群!高品质首发Go技术文章,“三天”首发阅读权,每年两期Go语言发展现状分析,每天提前1小时阅读到新鲜的Gopher日报,网课、技术专栏、图书内容前瞻,六小时内必答保证等满足你关于Go语言生态的所有需求!2023年,Gopher部落将进一步聚焦于如何编写雅、地道、可读、可测试的Go代码,关注代码质量并深入理解Go核心技术,并继续加强与星友的互动。欢迎大家加入!

img{512x368}
img{512x368}

img{512x368}
img{512x368}

著名云主机服务厂商DigitalOcean发布最新的主机计划,入门级Droplet配置升级为:1 core CPU、1G内存、25G高速SSD,价格5$/月。有使用DigitalOcean需求的朋友,可以打开这个链接地址:https://m.do.co/c/bff6eed92687 开启你的DO主机之路。

Gopher Daily(Gopher每日新闻) – https://gopherdaily.tonybai.com

我的联系方式:

  • 微博(暂不可用):https://weibo.com/bigwhite20xx
  • 微博2:https://weibo.com/u/6484441286
  • 博客:tonybai.com
  • github: https://github.com/bigwhite
  • Gopher Daily归档 – https://github.com/bigwhite/gopherdaily

商务合作方式:撰稿、出书、培训、在线课程、合伙创业、咨询、广告合作。

如发现本站页面被黑,比如:挂载广告、挖矿等恶意代码,请朋友们及时联系我。十分感谢! Go语言第一课 Go语言精进之路1 Go语言精进之路2 Go语言编程指南
商务合作请联系bigwhite.cn AT aliyun.com

欢迎使用邮件订阅我的博客

输入邮箱订阅本站,只要有新文章发布,就会第一时间发送邮件通知你哦!

这里是 Tony Bai的个人Blog,欢迎访问、订阅和留言! 订阅Feed请点击上面图片

如果您觉得这里的文章对您有帮助,请扫描上方二维码进行捐赠 ,加油后的Tony Bai将会为您呈现更多精彩的文章,谢谢!

如果您希望通过微信捐赠,请用微信客户端扫描下方赞赏码:

如果您希望通过比特币或以太币捐赠,可以扫描下方二维码:

比特币:

以太币:

如果您喜欢通过微信浏览本站内容,可以扫描下方二维码,订阅本站官方微信订阅号“iamtonybai”;点击二维码,可直达本人官方微博主页^_^:
本站Powered by Digital Ocean VPS。
选择Digital Ocean VPS主机,即可获得10美元现金充值,可 免费使用两个月哟! 著名主机提供商Linode 10$优惠码:linode10,在 这里注册即可免费获 得。阿里云推荐码: 1WFZ0V立享9折!


View Tony Bai's profile on LinkedIn
DigitalOcean Referral Badge

文章

评论

  • 正在加载...

分类

标签

归档



View My Stats