推理代码

原文链接

试图通过手动推理软件正确性的结果就是证明过程比代码本身还长,而且比代码共容易包含错误。自动化工具是首选,但并非每次都有效。有一条相对折中的方案:半正式化推理正确性。

基本方案便是考虑把所有代码都分割成小段,从一行、一个功能调用、到每个块不超过10行,争论它们的正确性。这些论点要足够强大,才能说服你那魔鬼般的程序员同行。

应该选择一个部分,便于在每个端点处的程序状态(即程序计数和处于生命周期内的对象值)都能满足易于描述的特性,并且该部分的功能(状态转换)很容易描述为一个单任务——这些可以让推理更简单。这些端点能够概括函数的前置和后置条件等概念,以及循环和类(的实例)的不变量。尽可能使各个部分相对独立,简化推理,当然,随时修改它们也是必不可少的。

很多历经编程实战的知识(可能不够好)以及’好的’思想可以简化推理。因此,仅仅是想要推理你的代码,就说明你已经在考虑一种更好的代码风格和数据结构了。不必惊讶,这些实战大多是经得起静态代码分析器的检验的:

  1. 避免使用goto语句,否则会与远处的部分高度耦合。
  2. 避免使用可变的全局变量,这会让所有地方都依赖他们。
  3. 每一个变量都应该尽可能让其作用域最小。例如,一个局部对象应该在它第一次使用的时候才声明。
  4. 在关联时,让对象不可变。
  5. 通过空白符让代码可读,不论水平还是垂直(排版)。例如,对其有关联的数据机构,以及用空行把两个小节分开。
  6. 让代码自成文档,选择描述(但相对简短的)对象名、类型、函数等。
  7. 如果你需要一个嵌套的部分,最好把它变成函数。
  8. 让你的函数短小且聚焦于单一任务上。老旧的24行限制原则依然受用。尽管屏幕尺寸和分辨率一只在升级,但人类的认知能力从1960年后就没怎么变过。
  9. 函数参数应尽量少(4个不能再多了)。这并不是限制了函数的数据传递能力:把有联系的参数分组到同一对象中,能得益于对象的不变性以及保存推理,确保他们的统一性和连贯性。
  10. 更普遍的,每个代码单元,从代码块到库,都应该有一个窄接口。更少的通信可以降低必要的推理。这就意味着,返回内部状态的getters方法是一种责任——不要问一个对象拿到信息后如何工作。反之,应该问一个对象拿到信息后有没有开始工作。换句话说,封装的是全部,暴露的接口是窄的。

除了要推理它的合理性,讨论你的代码可以让你进一步理解它。传达你的见解,让每个人受益。

0%