论文部分内容阅读
本文讨论适于研究并发控制问题的逻辑。由于现有某些逻辑(如动态逻辑、时态逻辑)的缺陷,因此我们提出了程序逻辑 TDL,它是时态逻辑的扩展,它易于研究并发程序,能表达程序的输入一输出性质和时态性质,并提供合成的开发证明方法。本文先讨论时态逻辑TL 和程序集 PG,然后定义程序逻辑 TDL 及证明系统 PT 并讨论它的表达能力,最后说明PT 的相对合理性和完全性。