让你的代码更可靠？秘诀是在脑中 “写证明”！

有网友分享了一个写代码时的小技巧，引发了大量程序员的共鸣。这个技巧就是：边写代码边在脑中 “证明” 它会正确运行。

这是一个技巧，但其实更像一种思维习惯：在写每一行代码的同时，不断验证它的逻辑是否自洽、是否会出错。当这种思维方式练熟之后，很多人会惊喜地发现：自己的代码常常一次就能跑通，甚至无需调试。

具体如何 “证明” 呢？Matthew 提供了五个实战中常用的思路：

1.单调性

程序中的某些状态一旦更新，就不该回退，比如 “已完成的任务”“增长的日志” 等。想象某个状态只能往一个方向变化，就能排除很多可能出错的路径。

2.前置条件 / 后置条件

明确函数 “执行前必须成立” 和 “执行后必须成立” 的条件，从而帮助你设计测试用例 & 写断言。如果某个函数的前 / 后置条件说不清楚，说明它本身就写得不清楚，值得重构！

3.不变量

不变量是贯穿整个程序生命周期必须保持不变的条件。把程序拆成小步骤，每一步都必须守住这个不变量，整体自然可靠。

当你发现系统变得诡异或时好时坏时，往往是某个关键不变量被偷偷破坏了。

4.隔离变化

代码的每一次改动，都有一个 “爆炸半径”。理想情况下，变化应尽量局限在本模块内部，而不是牵一发而动全身。

可以利用模块边界或接口作为防火墙，贯彻 “开闭原则”：加功能是加代码，而不是改旧代码。

5.归纳法

当你面对递归结构（比如树、列表）或写递归函数时，用数学归纳思维最自然。先证明最简单情况是正确的。再假设子结构已经正确，然后证明更大结构也正确。

作者在文章最后一段抛出了一个核心概念：Proof-affinity，直译是 “可证明性”。

简单来说就是，你写的代码，能不能轻松地用逻辑说服自己它不会出错。

不依赖测试、不需要日志，只靠逻辑推导，你就能大致确信这段逻辑的正确性，这种代码往往设计得很优秀。

上述的这些技巧，不仅能帮助你推理，也能反过来指导你如何写出好代码。换句话说：能被 “证明” 得越轻松的代码，往往本身就设计得更好。

这种证明的能力和练习打字一样，需要反复练手、变成本能。作者推荐从这三件事做起：

多写数学证明

多刷 Leetcode，但重质不重量

尝试用证明的方式解释自己的代码逻辑

来源: OSCHINA