"没有可靠性就谈不上完备性"这句话说得太绝对了点，但实际上都是先讲可靠性再说完备性，虽然两者没有逻辑上的隐含关系。

Hoare Logic是可靠的，但只是在PCA(partial correctnss assertions)的前提下相对完备。如果有一个程序验证工具，人家总是先要它做到可靠（也就是有错必纠），在这个基础上再尽量减少false positives。虽然理论上也可先设计一个完备的系统，也就是做到有纠必错，实际上应该没人会这么做。