定时CSP、Object-Z与对象建模技术解析

### 定时CSP、Object - Z与对象建模技术解析 在软件开发中，对于复杂系统的建模和规范描述一直是重要的研究方向。本文将探讨定时CSP与Object - Z的结合，以及在不扩展Z语言的情况下进行对象建模的相关技术。 #### 定时CSP与Object - Z结合的相关研究 在将定时CSP与基于状态的符号（如Z和Object - Z）集成的研究中，有多种不同的方法。 ##### 基于状态模拟的正确性 即使采用两事件模型，基于状态的模拟仍是正确的细化关系。因为它能在两事件模型中生成模拟，对应于两事件语义中的故障 - 发散细化。两事件模型的故障子集可以通过单事件的模拟来验证。这一特性具有重要的实际意义，由于基于状态的模拟规则相对于所选的CSP模型是不变的，Object - Z组件可以独立地进行规范和开发，而无需考虑使用单事件还是两事件模型语义，这也是使用两事件模型的一个很好的动机。 ##### 与非原子细化的联系 非原子细化是标准Z和Object - Z模拟规则的推广，它处理规范之间粒度的变化。在非原子细化中，一个抽象操作可以分解为一系列具体操作。这与两事件模型有明显的联系，因为在两事件模型中，单个事件e被分解为序列es; ef。在关系设置中，e和es; ef之间的细化对应于非原子细化。不过，与进程代数中动作细化的概念以及故障 - 发散细化的联系仍有待进一步探索。 ##### 相关集成方法比较 - **TCOZ**：Mahony和Dong定义的TCOZ是定时CSP和Object - Z的整体集成，但它采用了一种非组合的方式，需要用全新的符号编写规范，而不是像这里所做的那样组合用单个语言编写的组件。虽然TCOZ表达能力很强，但可能缺乏本文所实现的集成的简单性。 - **RT - Z**：Sühl定义的RT - Z与本文的工作最为接近，其背后的理念相似，但RT - Z使用Z而不是Object - Z，并且没有像本文这样全面讨论语义，也没有研究相关的细化概念。 ##### 两事件模型的同步问题 Fischer指出两事件模型在同步方面存在潜在问题。输入参数包含在开始事件中，输出参数包含在结束事件中，通过并行组合进行同步时，需要匹配输入值和输出值，这可能会出现问题。解决方案是确保包含两事件同步的规范只进行单向通信，这样一个组件的第一个事件可以与另一个组件的第二个事件同步。但这一方案的全部后果还需要进一步探索，实际上，之前两事件的使用仅限于不需要同步的操作。另一种方法是采用多事件模型，通常区分开始、结束和中间三个事件，并确保所有通信通过专门为此引入的中间事件实现，不过该模型的实用性也需要进一步研究。 #### 不扩展Z的对象建模方法 在不扩展Z语言的情况下，也可以优雅地指定面向对象的系统，包括封装、继承和子类型多态（动态调度）。 ##### 对象建模的关键思想 - **对象是黑盒**：与大多数扩展Z的面向对象方法不同，这里将每个对象视为黑盒，隐藏其内部细节。通过为每个类层次结构定义一个给定类型来实现，对象就是该给定类型的成员。对于单根继承层次结构（如Java和Smalltalk），定义一个给定类型[Object]；对于多根继承层次结构（如C++），为每个根类定义一个给定类型（如[Document, Window]）。多根方法可以通过Z类型系统静态检测一些错误，但不允许定义继承自两个不同层次结构的对象；单根方法更灵活，适用于类层次结构可能演变的新系统。 - **子类型是子集**：定义新的对象类型时，将其定义为现有类型的子集。例如，定义Document继承自Object，可写为Document : P Object；对于多重继承，如Pane既是Document又是Window的一部分，可写为Window : P Object，Pane : P(Document ∩ Window)。 - **方法是函数/关系**：在编程语言中，方法调用通常表示为outputs := object.method(inputs)。在Z中，使用谓词(object′, outputs) ∈ method(object, inputs)来建模，其中method是一个松散定义的公理关系method : (Class × Inputs) ↔ (Class × O