面向对象的时序逻辑语言 (2009年)

针对时序逻辑语言缺少面向对象概念的现状, 对投影时序逻辑进行了扩展, 介绍了新的语法和语义。在扩展投影时序逻辑中, 基于变量集合的层次化和谓词的分组, 给出了对象、类和继承等概念的形式化定义。扩展投影时序逻辑的一个可执行子集被定义为面向对象的时序逻辑语言Framed Tempura++, 它能够用于面向对象的程序设计, 可以模拟组合Web服务的执行。所给出的实例表明, 该语言与Framed Tempura相比, 能有效地重用代码, 提高了代码的可读性和可维护性。关 键 词