摘要
本文建立了时态逻辑演算。在该演算系统下,若能证明一程序抽象成的时态逻辑公式是定理,则该程序是完全正确的。
Temporal logic calculu is established. The program is total correctenessif it can prove that the temporal logic formula from a program abstractingis a theorem in the system of the calculu.
关键词
演绎
时态逻辑
程序验证
不变式
deduction
inveriant
well-structure
temporal logic
