论文部分内容阅读
针对面向对象系统，定义了一种基于时序逻辑的形式化规约语言。它不仅支持对面向对象思想中重要概念，如类、对象、继承等的描述，而且支持对面向对象系统的时序属性的描述，如类的状态之间的转换，类中某些属性必须一直满足的约束条件等。能够实现对系统属性的推理也是用这种语言描述的系统的动机之一。通过对一个局域网用户访问控制实例的描述来实现对这种形式化规约语言的直观阐述与理解。