第四章 编写正确的程序 这一章以二分搜索为例演示了算法验证的“三步曲“：初始化、保持和终止 初始化：循环初次执行的时候不变式为真 保持：如果在某次迭***始的 时候以及循环体执行的时候，不变式都为真，那么，循环体执行完毕的时候不变式依然为真 终止：循环能够...