name:第四部分：程序验证入门 scene1 title:什么是程序验证？ scene1 content:程序验证是软件工程中的一个重要环节，它的目标是证明一个程序是否能完成其预定任务。这不仅仅是运行几次测试，而是通过形式化的方法来证明其正确性。 scene2 title:程序的质量问题 scene2 content:一个高质量的程序不仅要功能正确，还需要考虑效率、代码风格、可读性和易于修改等问题。程序验证主要关注的是“功能正确性”这一核心问题。 scene3 title:部分正确性 vs. 完全正确性 scene3 content:程序正确性分为两种：部分正确性（Partial Correctness）和完全正确性（Total Correctness）。部分正确性指的是：如果程序能够停止运行，那么它产生的结果一定是正确的。而完全正确性则更进一步，它要求程序不仅结果正确，而且必须保证总能停止运行。 scene4 title:断言：前置条件与后置条件 scene4 content:为了进行程序验证，我们引入“断言”的概念。初始断言（Initial Assertion），也叫前置条件（precondition），规定了程序输入需要满足的属性。最终断言（Final Assertion），也叫后置条件（postcondition），规定了程序输出应该满足的属性。 scene5 title:断言的实际应用：JUnit scene5 content:在实际编程中，单元测试框架如JUnit就广泛使用了断言。测试代码中的`Assert.assertTrue`就是一个最终断言，它用来验证程序的输出是否符合预期的属性。 scene6 title:形式化表示：霍尔三元组 (Hoare Triple) scene6 content:部分正确性可以用一种称为“霍尔三元组”的表示法来形式化，记作 p{S}q。它的意思是：如果在执行程序S之前，前置条件p为真，并且程序S能够终止，那么在S执行完毕后，后置条件q必然为真。 scene7 title:一个简单的部分正确性证明 scene7 content:来看一个例子：程序段 y:=2; z:=x+y。前置条件p是x=1，后置条件q是z=3。假设p为真，即x=1。程序执行第一步后y=2。执行第二步后z=x+y=1+2=3。此时后置条件q为真。因此，该程序段关于给定的p和q是部分正确的。