基于时态逻辑演算的程序验证

本文建立了时态逻辑演算。在该演算系统下,若能证明一程序抽象成的时态逻辑公式是定理,则该程序是完全正确的。