利用状态变换的程序验证

本文试图把程序理解成一个定义在状态集上的状态函数。程序的执行过程等价于状态函数的求解过程。本文定义了程序语句的STP语义。在状态函数的意义下,证明了关于程序部分正确定理。最后,用实例说明了使用STP验证程序正确的可能性。