Hoare?逻辑 ·Hoarei逻辑良形公式{P}C{Q}的解释 部分正确性 在满足P的任何状态下执行C,若C终止则结果状 态一定满足Q。记作⑦ par{p)C1O) 完全正确性 在满足P的任何状态下执行C,则C一定终止并且 结果状态一定满足Q。记作ot{P}C{2} 通常建议用部分正确性证明十终止性证明来得到 完全正确性证明Hoare逻辑 • Hoare逻辑良形公式{ P } C { Q }的解释 – 部分正确性 在满足P的任何状态下执行C，若C终止则结果状 态一定满足Q。记作  par { P } C { Q } – 完全正确性 在满足P的任何状态下执行C，则C一定终止并且 结果状态一定满足Q。记作  tot { P } C { Q } – 通常建议用部分正确性证明＋终止性证明来得到 完全正确性证明