【程序安全百分百】系列文章

第一章:笑傲代码江湖

TODO:

  •   - [ ] 语言的能力(什么是语言?《人类简史》,人类语言的诞生,意识的表达,语言的不正确性)
      - [ ] 计算机语言的发展(举例,C)
      - [ ] 犯错的人类(举例)
      - [ ] 逻辑的诞生(三段论,引出逻辑系列文章:谓词逻辑,一阶逻辑,费马大定理,高阶逻辑,霍尔逻辑,分离逻辑)
    
  •   - [ ] 软件测试
      - [ ] 模型检测
      - [ ] 定理证明
    

只要是要使用到语言,脑洞可以开到无限大,语言是万能的吗?语言能够描述意识中所有的想法吗?语言的目的是交流,交流的目的是欲望,欲望的目的是生存……尽管可以无限想象,但在计算机的世界里,语言可以看成是逻辑,既然是逻辑,就是无懈可击的,没有二义性,简单直白,都是数学的特点。

在刚开始学编程时,我们一般通过测试来验证我们的程序,比如执行一次程序,得到执行结果,看跟自己心中期望的结果是否相同。这可以看成是简单的软件测试思路。通过测试来判断软件的正确性在工业界取得很高的效率,一般的软件公司都有两个大部门,一个是软件开发,一个是软件测试。软件测试是不严谨的手段,并不能确保软件百分百的正确,因为程序的状态空间有可能是无限的,因为有无限状态,测试就不可能穷尽所有的可能。1996年,欧航局的Ariane 5 发射40秒后爆炸,爆炸的原因是软件中,变量从float类型转换到integer类型时溢出。这种错误,是测试很难发现的。

 欧航局研制的Ariane 5 爆炸

1
2
3
P M DERIVE(T ALG.E BH) :=
UC 16S EN 16NS (TDB.T ENTIER 16S
((1.0/C M LSB BH) * G M INFO DERIVE(T ALG.E BH)));