摘要
本文研究建立了代数规范和时序逻辑规范的不同语义模型之间的关联,在结构偏代数上解释时序模态词,从而可以利用时序逻辑工具讨论由代数规范所定义的抽象对象的动态行为特征.
This paper contributes to make connections between two kinds of semanticmodels for algebraic and temporal specifications. A class of structured partial algebras are used as Kripke models to interpret temporal modalities. It provides the possibility for reasoning about behaviour constraints of abstract objects.
出处
《计算机学报》
EI
CSCD
北大核心
1992年第12期889-897,共9页
Chinese Journal of Computers
关键词
代数规范
时序逻辑
行为约束
语义
Algebraic specification, temporal logic, behaviour constraints, Kripke semantics.
