测试开发工具【免费下载链接】hypothesisThe property-based testing library for Python项目地址https://gitcode.com/gh_mirrors/hy/hypothesis点击查看免费下载导读本文以 Hypothesis 官方博客的经典实战案例为骨架电影《虎胆龙威3》中主角需要在 3 加仑和 5 加仑两只水壶之间精确量出 4 加仑水否则会被引爆。原作者 Nicolas Chammas 受 TLA 形式化规格示例启发将这一谜题移植为 Hypothesis 的RuleBasedStateMachine状态机测试——通过声明状态转移规则rule与不变量invariant让属性测试框架自动搜索违反不变量的操作序列从而逼Hypothesis 替我们找出答案。读完本文你将掌握状态机测试的核心思想、rule/invariant/note/settings等 API 的完整用法、Hypothesis 如何寻找并最小化失败用例以及如何把这类找反例的思路迁移到真实系统的数据库、队列、协议等有状态场景中。背景从 TLA 到属性测试电影谜题在《虎胆龙威3》Die Hard with a Vengeance中John McClane 与 Zeus Carver 面对这样一道难题给定一只3 加仑的水壶和一只5 加仑的水壶如何恰好量出4 加仑水水无限供应水壶没有刻度。这一经典问题在算法界常被称为水壶问题Water Jug Problem。形式化规格语言 TLA这类问题可以用形式化规格语言 TLA 描述。TLA 与编程语言类似都用来描述系统的行为但它建立在更严格的数学基础之上能够对系统行为进行更可靠的推理。TLA 社区有一个 DieHard.tla 示例把水壶操作建模为状态机初始状态是两只空壶状态转移是装满倒空互倒等操作再借助模型检查器穷举/搜索状态空间找出能够达到大壶中恰有 4 加仑这一目标状态的转移序列。属性测试与 HypothesisTLA 是规格 模型检查而 Python 世界的属性测试Property-Based Testing走的是另一条路给机器一个关于代码行为的高层描述让机器自动生成测试用例来验证这个描述是否成立。相比传统单元测试中手动编写具体输入与预期输出属性测试把找反例的工作交给了机器。Hypothesis 正是 Python 生态中属性测试的成熟实现即本仓库 hypothesis 所对应的开源项目。它支持状态化测试stateful testing即不仅生成单个数据还生成整段测试程序——由一系列原子操作组合而成的操作序列。官方文档 stateful.rst 开篇即引用了本文所讲的《虎胆龙威》示例并推荐读者结合本文理解规则式状态机测试。核心实现把水壶问题写成状态机测试原文档给出了完整的可运行代码。下面保留原代码并补充关键注解from hypothesis import note, settings from hypothesis.stateful import RuleBasedStateMachine, invariant, rule # 默认设置下 Hypothesis 不一定能在足够少的例子里找到反例 # 因此提高单次运行的测试用例数量上限让搜索更充分。 settings(max_examples2000) class DieHardProblem(RuleBasedStateMachine): small 0 # 3 加仑小壶当前水量 big 0 # 5 加仑大壶当前水量 # ---- 六种合法操作状态转移---- rule() def fill_small(self): self.small 3 rule() def fill_big(self): self.big 5 rule() def empty_small(self): self.small 0 rule() def empty_big(self): self.big 0 rule() def pour_small_into_big(self): old_big self.big self.big min(5, self.big self.small) self.small self.small - (self.big - old_big) rule() def pour_big_into_small(self): old_small self.small self.small min(3, self.small self.big) self.big self.big - (self.small - old_small) # ---- 不变量任何时候都必须成立的性质 ---- invariant() def physics_of_jugs(self): # 水量不能超出壶的容量也不能为负 assert 0 self.small 3 assert 0 self.big 5 invariant() def die_hard_problem_not_solved(self): # 故意声明大壶永远装不到 4 加仑 note(f small: {self.small} big: {self.big}) assert self.big ! 4 DieHardTest DieHardProblem.TestCase代码结构拆解这个测试类由三部分构成与 RuleBasedStateMachine 的源码实现 一一对应状态实例变量small与big记录两只壶当前的水量初始均为 0。源码中状态机携带被测系统与支撑数据数据可存放在实例变量中也可划分为 Bundles。转移rule装饰的方法装满、倒空、互倒共 6 个操作共同定义了系统的全部合法行为。从源码看rule内部会把装饰的方法包装成Rule对象stateful.py#L875-L939并支持targets/target把返回值写入 Bundle与策略参数如rule(nintegers())。不变量invariant装饰的方法每个操作执行后都会被调用抛出异常即代表违反不变量。源码中invariant生成Invariant对象stateful.py#L1112-L1159装饰后的函数在每一步之后运行可通过抛出异常来表示不变量被破坏。physics_of_jugs约束了物理事实小壶永远在[0, 3]、大壶永远在[0, 5]。die_hard_problem_not_solved则故意声明大壶不可能有 4 加仑——这正是引导 Hypothesis 去破解谜题的关键相当于反向声明目标状态不可达。最后一行DieHardTest DieHardProblem.TestCase把状态机类转换成 unittest 的TestCase。源码中_to_test_casestateful.py#L502-L514动态创建一个StateMachineTestCase其runTest调用run_state_machine_as_test(cls, settingsself.settings)因此可以直接被 pytest、unittest 发现和执行。运行方式把上述代码保存为.py文件后直接调用 pytestpytest how-not-to-die-hard-with-hypothesis.py即可看到 Hypothesis 在约 0.22 秒内找到反例并输出如下结果原文档的原始输出self DieHardProblem({}) invariant() def die_hard_problem_not_solved(self): note( small: {s} big: {b}.format(sself.small, bself.big)) assert self.big ! 4 E AssertionError: assert 4 ! 4 E where 4 DieHardProblem({}).big how-not-to-die-hard-with-hypothesis.py:17: AssertionError ----------------------------- Hypothesis ----------------------------- small: 0 big: 0 Step #1: fill_big() small: 0 big: 5 Step #2: pour_big_into_small() small: 3 big: 2 Step #3: empty_small() small: 0 big: 2 Step #4: pour_big_into_small() small: 2 big: 0 Step #5: fill_big() small: 2 big: 5 Step #6: pour_big_into_small() small: 3 big: 4 1 failed in 0.22 seconds 输出中的Hypothesis区块正是最短复现程序装满大壶 → 倒入小壶 → 倒空小壶 → 再倒入小壶 → 装满大壶 → 倒入小壶最终big 4。这正是电影中 McClane 与 Carver 的操作过程也是 TLA 示例给出的同一组解。深入原理Hypothesis 是如何做到的状态机执行模型从源码看一次测试运行会为每个测试用例新建一个状态机实例然后循环执行stateful.py#L146-L186默认每一步从所有可用规则中随机选择一个执行规则选择本身是一个组合策略RuleStrategy见 stateful.py#L1162可用的规则集合还会受precondition过滤每步结束后调用check_invariants检查所有invariant步数上限由settings.stateful_step_count控制默认 50见 _settings.py#L959-L969单次运行能生成的测试用例数量由settings.max_examples控制默认 100见 _settings.py#L755-L794。原文档把max_examples提高到 2000正是因为默认设置下 Hypothesis 不一定能在足够的例子里找到反例——这是一个很实用的经验当搜索空间较大时可以先用少量例子跑通再逐步加大max_examples。最小化反例ShrinkingHypothesis 的核心工作方式原文档作者自述的总结它读取我们声明的程序性质——包括规则、不变量、数据类型、函数签名——并自动生成数据或操作序列来探测程序行为。一旦发现某段数据或某个操作序列违反已声明性质就会尝试将其缩减为最小反例minimum falsifying example即用最少的步骤复现同一问题从而极大降低我们理解 bug 的难度。所以上节输出中的 6 步序列不是随便找的——它是 Hypothesis 在违反不变量之后收缩得到的最短操作序列。这种找到反例再最小化的机制让状态机测试既具备发现力又具备可读性。note 的作用die_hard_problem_not_solved中的note(f small: {self.small} big: {self.big})会在反例输出中记录每一步后的水量快照。从 control.py#L258-L278 的源码看note记录的值会随最小失败用例一起报告并在Verbosity.verbose及以上级别输出全部记录非字符串值会自动转成字符串。这就是输出里每行 small: ... big: ...的来源让整个状态演化过程一目了然。实战延伸把同一套路用于真实系统水壶问题是玩具但状态机 不变量的方法论可以直接迁移到真实有状态系统。Hypothesis 官方文档 stateful.rst 给出了一个更贴近生产的例子对比测试示例数据库的真实实现与内存模型。其骨架如下import shutil import tempfile from collections import defaultdict import hypothesis.strategies as st from hypothesis.database import DirectoryBasedExampleDatabase from hypothesis.stateful import Bundle, RuleBasedStateMachine, rule class DatabaseComparison(RuleBasedStateMachine): def __init__(self): super().__init__() self.tempd tempfile.mkdtemp() self.database DirectoryBasedExampleDatabase(self.tempd) self.model defaultdict(set) # 期望行为的简化内存模型 keys Bundle(keys) values Bundle(values) rule(targetkeys, kst.binary()) def add_key(self, k): return k rule(targetvalues, vst.binary()) def add_value(self, v): return v rule(kkeys, vvalues) def save(self, k, v): self.model[k].add(v) self.database.save(k, v) rule(kkeys, vvalues) def delete(self, k, v): self.model[k].discard(v) self.database.delete(k, v) rule(kkeys) def values_agree(self, k): assert set(self.database.fetch(k)) self.model[k] def teardown(self): shutil.rmtree(self.tempd) TestDBComparison DatabaseComparison.TestCase这个例子引出了水壶问题中没用到但同样重要的 APIBundle命名集合用于让数据在规则之间流转targetkeys写入kkeys读出鼓励 Hypothesis 对同一 key/value 反复操作更容易暴露状态一致性 bugteardown每次运行结束后清理临时目录TestCase.settings可对单个状态机设置参数例如DatabaseComparison.TestCase.settings settings(max_examples50, stateful_step_count100)即减少用例数、加长每个用例的步数。文档还提醒若需要根据机器当前状态来画参数普通策略不够用可用st.runner().flatmap(...)访问实例变量或直接用st.data()。此外initialize保证在任何rule之前恰好执行一次precondition可过滤不适用的规则比在规则内assume高效得多详见 stateful.rst。常见问题与调优建议为什么默认设置可能找不到反例max_examples默认 100、stateful_step_count默认 50即默认每次运行最多执行约 5000 步随机操作。水壶问题的状态空间虽小但恰好把大壶灌到 4属于较深的路径随机游走未必在 100 个用例内命中。此时按原文档做法提高max_examples如 2000或同时调整stateful_step_count即可。反例输出是伪代码但通常可直接复制状态机输出的复现序列通常非常接近 Python 代码如state DatabaseComparison()、var1 state.add_key(kb)等见 stateful.rst#L98-L112多数情况下可以复制进测试中直接复现前提是对象有合适的repr。更细粒度的控制不想依赖TestCase时可直接调用run_state_machine_as_test(state_machine_factory, settings...)它接受任意无参数调用即返回状态机实例的类或函数运行并打印最短失败程序stateful.py#L255-L279。总结这篇文章展示了属性测试一个非常优雅的侧面把这个问题无解写成不变量让机器去找反例反例本身就是答案。TLA 靠模型检查穷举状态空间Hypothesis 靠随机搜索加收缩最小化殊途同归地解出了同一道水壶题。正如原作者所言把 TLA 示例翻译成 Hypothesis 的 Python 版本出人意料地直接Python 版的规格并不比 TLA 原文冗长多少区别只在于 TLA 用small与small表示当前值与下一步值而 Python 需要借助old_small、old_big这类中间变量。把这一思维应用到日常开发数据库一致性、分布式队列、缓存与存储的等价性、协议实现等一切存在状态转移的系统都可以用RuleBasedStateMachine建模——声明操作与不变量剩下的交给 Hypothesis 去折腾。你甚至会发现机器替你生成出了一段解决问题的程序。进一步阅读完整的状态机测试文档见 hypothesis/docs/stateful.rstRuleBasedStateMachine与rule/invariant/precondition/initialize的实现见 hypothesis/src/hypothesis/stateful.pymax_examples与stateful_step_count等设置的默认值与说明见 hypothesis/src/hypothesis/_settings.pynote的行为见 hypothesis/src/hypothesis/control.py#L258-L278。赞分享测试开发工具【免费下载链接】hypothesisThe property-based testing library for Python项目地址https://gitcode.com/gh_mirrors/hy/hypothesis点击查看免费下载相关推荐LeetCode 365 水壶问题题解从 BFS 状态搜索到裴蜀定理Bézouts identityLeetCode 365 水壶问题题解从 BFS 状态搜索到裴蜀定理Bézouts identity 导读 本文以 leetcode 题解仓库中 pro文档教程知识库Python 测试代码实战指南从 unittest、doctest 到 pytest、Hypothesis、tox 与 mock 的完整测试栈Python 测试代码实战指南从 unittest、doctest 到 pytest、Hypothesis、tox 与 mock 的完整测试栈 本指南源自开源文档教程LeetCode 365 水壶问题全解从 BFS 状态搜索到数学模拟与裴蜀定理LeetCode 365 水壶问题全解从 BFS 状态搜索到数学模拟与裴蜀定理 每日一题系列 每日一题说明 https://link.gitcode.com文档教程知识库上一篇LinkSwift网盘下载助手3步解锁九大网盘高速下载的终极方案下一篇在 Floci 中实现 CodeGuru Reviewer 仓库关联生命周期接口、校验与存储详解创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考