UML类构造形式化方法对比与类正确性证明探索

### UML类构造形式化方法对比与类正确性证明探索 #### 1. UML类构造形式化方法分析 在UML类构造的形式化方面，不同的方法各有特点。Kim & Carrington（KC）方法在处理UML的一些复杂概念上表现出色。 ##### 1.1 聚合与组合 KC对组合关系的形式化表示在图21中有所体现。组合关系中，部分类（Part）和复合类（Whole）都依据类和关联的规则进行形式化。部分声明使用了OZ的非共享包含符号（⃝C），这表明部分完全包含在Whole所代表的结构中（意味着删除传播），并且没有一个Part类的对象会被两个不同的Whole类对象包含（非共享包含）。 | 类 | 属性 | 约束 | | --- | --- | --- | | ThingRel | atrel1 : ATREL1; rB2 : ThingB; rWhole : Whole | self ∈rB2.rWhole ∧ self ∈rWhole.rB2 | | Whole | atw1 : ATW 1; rB2 : P ThingRel; parts : P Part⃝C | #rB2 ∈ 1..5; ∀rb : rB2 • self = rb.rWhole; ∀p : parts • self = p.whole | | Part | atp1 : ATP1; whole : Whole | self ∈ whole.parts | 而KC对聚合的形式化与简单关联相同。 ##### 1.2 系统状态 在KC中，整个系统在OZ类模式中定义为类实例的集合。其形式化规则如下： - 每个OZ类在系统类中实例化为一个集合。 - 如果OZ类是超类，那么该类的实例化必须是该类多态类型的集合。 ```plaintext System thingAs : P ThingA; thingBs : P ThingB; parents : P ↓Parent childAs : P ChildA; childBs : P ChildB; thingRels : P ThingRel wholes : P Whole; parts : P Part ∀a : thingAs • a.rB1 ⊆ thingBs ∧ ran(a.rParent) ⊆ parents ∀b : thingBs • b.rA1 ∈ thingAs ∧ b.rWhole ⊆ thingRels ∧ b.rSelf 1 ∈ thingBs ∧ b.rSelf 2 ⊆ thingBs ∀p : parents • p.rA2 ⊆ thingAs ∀w : wholes • w.rB2 ⊆ thingRels ∧ w.parts ⊆ parts ∀p : parts • p.whole ∈ wholes ∀tr : thingRels • tr.rB2 ∈ thingBs ∧ tr.rWhole ∈ wholes ∀tr1, tr2 : thingRels | tr1.rWhole = tr2.rWhole ∧ tr1.rB2 = tr2.rB2 • tr1 = tr2 childAs ⊆ parents ∧ childBs ⊆ parents ∀p : parents • p ̸ ∈ Parent ``` 在系统状态模式中，还添加了约束来克服缺失的特性，并对原始方法进行了一些小的修正。例如，声明了类Parent的抽象属性（原始工作中缺失），并在系统状态模式的谓词中强制规定了ThingRel作为关联类的正确行为（不允许其实例中的链接重复）。 #### 2. 不同形式化方法的比较 不同的形式化方法在支持UML示例图的特性方面都存在不足。Hall将关联形式化为链接类，KC对关联类的形式化都违反了UML关联的语义，因为UML中不允许链接（对象引用元组）重复。不过，这个问题可以通过在组件或系统模式中强制正确的行为来纠正。 | 方法 | 优点 | 缺点 | | --- | --- | --- | | Z方法 | 能近似面向对象语义，有成熟的标准和工具 | 形式化过程繁琐，缺乏足够的抽象性 | | OZ方法 | 固有面向对象概念使UML概念的形式化更简洁、直观 | 类型检查工具不成熟 | 总体而言，Z是一种更开放的语言，但使用Z来近似面向对象语义比较繁琐。OZ的固有