想研究一下，如何证明程序的正确性，有什么书推荐吗？

想从理论上研究一下，如何证明编写的程序的正确性，有没有哪本书可以推荐一下

欸，竟然有人会对这种理论感兴趣，强烈安利一下UW的 CSE331: Software Design and Implementation。https://courses.cs.washington.ed...ar/lecturelist.html
大半个学期在讲code reasoning, prove correctness和ADT，后面讲到的是writing maintainable code，涉及到design patterns, testing, OOP的痛点和解决方式。阐述了true subtype和Java subtype的区别，subclass的confusion。前期就很符合楼主想要的信息。整门课偏理论但是真的是码农界的一股清流，教的不是写代码但是是以后程序员升级的必备的宝藏，所以真心安利。

推荐看早期一点的学期的财力哦，这门课的创始教授几个都觉的很好，有一些slides后期做的不错，中间有两三个学期有一两个教授的一些细节教错了一点点，不过不影响学习，后面学期教的时候有提到并纠正。

prove correctness一开始有一些地方真的很困惑，一旦想通了就很容易了。例如想出decrementing function、branching的backward reasoning、和有时候figure out weakest precondition会有一些难。有疑惑的话可以多多交流~ 我是我们学校(不是UW)这门课的TA，应该大部分都能帮到。

SLiNv_Vic 发表于 2019-1-6 23:01
欸，竟然有人会对这种理论感兴趣，强烈安利一下UW的 CSE331: Software Design and Implementation。https:/ ...

好的，非常感谢，仔细研究一下。