对象导向精化：原理、规则与应用

### 对象导向精化：原理、规则与应用 #### 1. 对象系统精化 在对象导向编程中，理解两个对象程序之间的精化关系至关重要。我们定义，若两个对象程序 $S_i = Cdeclsi • Maini$（$i = 1, 2$）具有相同的外部变量集 $extvar$，且满足 $\forall extvar, extvar′, ok, ok′ · ([[S1]] ⇒[[S2]])$，则称 $S1$ 是 $S2$ 的精化，记为 $S1 ⊒sys S2$。 以下通过示例说明： - **示例 14.3**： - 对于任意类声明 $Cdecls$，$S1 = Cdecls • ({x : C}, C.new(x))$ 和 $S2 = Cdecls • ({x : C}, C.new(x); C.new(x))$ 是等价的。 - 假设类 $C \in pubcname$，$\langle a:Int, d\rangle\in attr(C)$，在 $op(C)$ 中有 $get(\emptyset; Int z; \emptyset)\{z := a\}$ 和 $update()\{a := a + c\}$，则 $Cdecls • ({x : C, y : Int}, C.new(x); x.update(); x.get(y))$ 和 $Cdecls • ({x : C, y : Int}, C.new(x); x.update(); x.get(y); C.new(x))$ 是等价的。 下面给出第二个示例的证明： 设第一个程序为 $S1$，第二个为 $S2$，假设声明部分定义良好。计算 $S1$ 的语义： \[ \begin{align*} [[C.new(x); x.update(), x.get(y)]] &= true \vdash\exists r \in REF · (\Pi′ = \{\langle r, C, \sigma0\rangle\} \land x′ = \langle r, C\rangle); [[x.update(); x.get(y)]]\\ &= \left( \begin{array}{l} true \vdash\exists r \in REF · (\Pi′ = \{\langle r, C, \sigma0\rangle\} \land x′ = \langle r, C\rangle)\\ \land self′ =< > \land \Pi′ = \{\langle r, C, \sigma0 \oplus\{a \mapsto d + c\}\rangle| r = ref(x)\}; [[x.get(y)]] \end{array} \right)\\ &= \left( \begin{array}{l} true \vdash\exists r \in REF · (\Pi′ = \{\langle r, C, \sigma0 \oplus\{a \mapsto d + c\}\rangle\} \land x′ = \langle r, C\rangle)\\ \land self′ =< >); [[x.get(y)]] \end{array} \right)\\ &= \left( \begin{array}{l} true \vdash\exists r \in REF · (\Pi′ = \{\langle r, C, \sigma0 \oplus\{a \mapsto d + c\}\rangle\} \land x′ = \langle r, C\rangle)\\ \land self′ =< >); true \vdash self′ =< > \land z′ =< > \land y′ = d + c\\ \land visibleattr′ = \{M.a | M \in pubname \land a \in pub(M)\} \end{array} \right)\\ &= \left( \begin{array}{l} true \vdash\exists r \in REF · (\Pi′ = \{\langle r, C, \sigma0 \oplus\{a \mapsto d + c\}\rangle\} \land x′ = \langle r, C\rangle)\\ \land self′ =< > \land z′ =< > \land y′ = c + d\\ \land visibleattr′ = \{M.a | M \in pubname \land a \in pub(M)\} \end{array} \right) \end{align*} \] 语义 $[[S1]]$ 通过存在量词隐藏 $\Omega, \Pi, self$ 和 $z$。设 $[[Cdecls]]$ 为 $true \vdash\Omega = \emptyset\land\Omega′ = \Omega0$，则 $[[S1]]$ 等于 $true \vdash\exists r \in REF · x′ = \langle r, C\rangle\land y′ = c + d$。 $S2$ 的主方法是 $S1$ 的主方法后接命令 $C.new(x)$，其语义为： \[ \begin{align*} [[C.new(x); x.update(), x.get(y)]]; [[C.new(x)]] &= \left( \begin{array}{l} true \vdash\exists r \in REF · (\Pi′ = \{\langle r, C, \sigma0 \oplus\{a \mapsto d + c\}\rangle \land x′ = \langle r, C\rangle)\\ \land self′ =< > \land z′ =< > \land y′ = c + d\\ \land visibleattr′ = \{M.a | M \in pubname \land a \in pub(M)\};\\ true \vdash\exists p \notin ref(\Pi) · \Pi′ = \Pi \cup\{\langle p, C, \sigma0\rangle\} \land (x′ = \langle p, C\rangle) \end{array} \right)\\ &= \left( \begin{array}{l} true \vdash\exists r, p \in REF · ((p \neq r) \land \Pi′ = \{\langle p, C, \sigma0\rangle, \langle r, C, \sigma0 \oplus\{a \mapsto d + c\}\rangle\}\\ \land x′ = \langle p, C\rangle) \land self′ =< > \land z′ =< > \land y′ = c + d\\ \land visibleattr′ = \{M.a | M \in pubname \land a \in pub(M)\} \end{array} \right) \end{align*} \] 隐藏内部变量后，$[[S2]]$ 简化为 $true \vdash\exists p \in REF · x′ = (p, C) \land y′ = c + d$。因此，$S1$ 和 $S2$ 相互精化。 但需注意，程序 $S1; x.get(y)$ 与 $S2; x.get(y)$ 不等价。第一个程序中 $y$ 的最终值仍为 $d + c$，而第二个程序中 $y$ 的最终值为 $d$。从白盒语义角度看，$S1$ 和 $S2$ 原本就不等价。 这个示例表明程序精化是非组合性的。给定两个主方法 $Maini = (extvar, ci)$（$i = 1, 2$），若 $Cdecls1 • Main1 \geq_{sys} Cdecls2 • Main2$，并不一定有 $Cdecls • (extvar, c1; c) \geq_{sys} Cdecls • (extvar, c2; c)$。非组合性是由于语义中隐藏了全局内部变量 $\Pi$ 导致的。不过，若使用白盒语义定义精化关系，当 $s$ 仅涉及对附加到外部变量的对象方法的调用时，上述非组合性将消失。因此，白盒精化是黑盒语义精化的子关系，且更具组合性。 还有一个定理：设 $Cdecls • Main$，$C$ 是 $Cdecls$ 中声明的公共类，$Cdecls1$ 是将 $C$ 改为私有类后从 $Cdecls$ 得到的。若 $Main$ 中未引用 $C$，则 $Cdecls • Main =_{sys} Cdecls1 • Main$，其中 $=_{sys}$ 是等价关系 $\geq_{sys} \cap\leq_{sys}$，且关系 $\geq_{sys}$ 是自反和传递的。 #### 2. 结构精化 示例 14.3 的证明表明，程序的局部变量和可见属性在每次方法调用后是常量。当程序中的主方法在语法上相同时，它们的系统状态之间的关系由这些程序的结构关系决定，即类名、属性、子类 - 超类关系以及类中的方法。 对象导向程序设计主要围绕类及其方法的设计。类声明部分实际上可以支持许多不同的应用主程序。下面重点介绍结构精化。 **定义 14.10**：设 $Cdecls1$ 和 $Cdecls2$ 是两个声明部分。若 $Cdecls1$ 能在任何对象系统中替换 $Cdecls2$，则称 $Cdecls1$ 是 $Cdecls2$ 的精化，记为 $Cdecls1 \geq_{class} Cdecls2$，即 $Cdecls1 \geq_{class} Cdecls2 \stackrel{def}{=} \forall Main · (Cdecls1 • Main \geq_{sys} Cdecls2 • Main)$。 非正式地说，$Cdecls1$ 至少支持与 $Cdecls2$ 相同数量的服务。显然，$\geq_{class}$ 是自反和传递的。我们用 $=_{class}$ 表示等价关系 $\geq_{class} \cap\leq_{class}$，在不引起混淆时省略下标。 结构精化不改变主方法。$Cdecls2$ 中的每个公共类都必须在精化后的声明部分 $Cdecls1$ 中声明，并且 $Cdecls2$ 中公共类的每个方法签名都必须在 $Cdecls1$ 中声明。 **定义 14.11**：对于 $i = 1, 2$，设 $Cdeclsi$ 是两个类声明部分。从 $Cdecls1$ 到 $Cdecls2$ 的结构转换是 $Cdecls1$ 的对象空间 $\tau_1$ 和 $Cdecls2$ 的对象空间 $\tau_2$ 之间的关系，可以表示为一个设计 $true \vdash\rho(\Omega1, \Omega′_2