Skip to main content

形式化验证与自动化测试探索

· 4 min read
Tags:
ayanami

最近在学形式化验证相关的内容，顺便探索了一下自动化测试的工具链。

形式化验证入门​

读了一篇很好的文章：SAT/SMT, z3, Model Checking, Translation Validator - 有关形式化验证我所知道的一切

好文，有点像一个综述，涵盖了SAT/SMT求解器、z3、Model Checking、Translation Validator等。

伟大的CDM（计算离散数学），这学期上的最好的两门课CDM & CSE（计算机系统工程），让我对这些概念有了更深的理解。

从Model Checker到自动化测试​

在看Model Checker的时候，想到了自动化（生成）（单元）测试。

首先先把AI-based的方法ban了——无法保证正确性，还需要人review的话，感觉不如让测试工程师自己用AI。

已有的工具​

好像只有Java有一个EvoSuite，能在AST层面自动生成单元测试。逛知乎又看到一篇文章，是在AST的level上给C++生成单测的，但可惜不开源：C/C++ 单元自动化测试解决方案实践

Hypothesis：Python的属性测试库​

wow，伟大的AI帮我找到了一个有趣的Python库：Hypothesis

给出的例子就很吸引人了。Hypothesis是一个**属性测试（Property-based Testing）**库，你只需要描述代码应该满足的属性（不变量），它会自动生成大量测试用例来尝试找到反例。

from hypothesis import given, strategies as st

@given(st.lists(st.integers()))
def test_sort_is_sorted(xs):
    result = sorted(xs)
    assert result == sorted(result)
    assert set(result) == set(xs)

完全符合我对一个自动化测试/验证的库的想象！感觉如果用Python写一些算法的话会很好用。

Schemathesis：API测试的利器​

实际上是因为看到了这个库：Schemathesis

感觉能自动化超级多的垃圾时间。如果能做CI/CD集成的话再好不过了。

感想​

感觉以后写Web项目真得最开始就和OpenAPI一套架子搭好。有了规范，就能自动生成文档、自动测试、自动验证——这才是工程化该有的样子。

想给jcourse生成一个OpenAPI文档，感觉两种方案：

  1. Annotation based：加注释，工作量好大
  2. 架构重构：彻底重构handler层，通过约定和配置覆写默认的处理方法，降低灵活性带来更好的集成

参考了这篇文章：Autogenerated API Documentation in Go with OpenAPI/Swagger

Java味道太足了，但确实是经过验证的好实践。

Loading Comments...