试图通过手动推理软件正确性的结果就是证明过程比代码本身还长，而且比代码共容易包含错误。自动化工具是首选，但并非每次都有效。有一条相对折中的方案：半正式化推理正确性。
基本方案便是考虑把所有代码都分割成小段，从一行、一个功能调用、到每个块不超过10行，争论它们的正确性。这些论点要足够强大，才能说服你那魔鬼般的程序员同行。
应该选择一个部分，便于在每个端点处的程序状态(即程序计数和处于生命周期内的对象值)都能满足易于描述的特性，并且该部分的功能(状态转换)很容易描述为一个单任务——这些可以让推理更简单。这些端点能够概括函数的前置和后置条件等概念，以及循环和类(的实例)的不变量。尽可能使各个部分相对独立，简化推理，当然，随时修改它们也是必不可少的。
很多历经编程实战的知识(可能不够好)以及’好的’思想可以简化推理。因此，仅仅是想要推理你的代码，就说明你已经在考虑一种更好的代码风格和数据结构了。不必惊讶，这些实战大多是经得起静态代码分析器的检验的：
- 避免使用goto语句，否则会与远处的部分高度耦合。
- 避免使用可变的全局变量，这会让所有地方都依赖他们。
- 每一个变量都应该尽可能让其作用域最小。例如，一个局部对象应该在它第一次使用的时候才声明。
- 在关联时，让对象不可变。
- 通过空白符让代码可读，不论水平还是垂直(排版)。例如，对其有关联的数据机构，以及用空行把两个小节分开。
- 让代码自成文档，选择描述(但相对简短的)对象名、类型、函数等。
- 如果你需要一个嵌套的部分，最好把它变成函数。
- 让你的函数短小且聚焦于单一任务上。老旧的24行限制原则依然受用。尽管屏幕尺寸和分辨率一只在升级，但人类的认知能力从1960年后就没怎么变过。
- 函数参数应尽量少(4个不能再多了)。这并不是限制了函数的数据传递能力：把有联系的参数分组到同一对象中，能得益于对象的不变性以及保存推理，确保他们的统一性和连贯性。
- 更普遍的，每个代码单元，从代码块到库，都应该有一个窄接口。更少的通信可以降低必要的推理。这就意味着，返回内部状态的getters方法是一种责任——不要问一个对象拿到信息后如何工作。反之，应该问一个对象拿到信息后有没有开始工作。换句话说，封装的是全部，暴露的接口是窄的。
除了要推理它的合理性，讨论你的代码可以让你进一步理解它。传达你的见解，让每个人受益。
