面向对象编程的语义与状态分析

# 面向对象编程的语义与状态分析 ## 1. 动态变量 ### 1.1 系统配置 引入变量 Π，其值为目前已创建对象的集合，称为当前配置。在程序执行期间，Π 的取值需满足以下条件： - 对象完整性：若 o ∈ Π 且 a 属于 o 类型的属性（a 为类类型），则 o.a 要么为 null，要么存在 o1 ∈ Π 且 ref(o.a) = ref(o1)。 - 对象唯一标识：对于 Π 中的任意对象 o1 和 o2，若 ref(o1) = ref(o2)，则 type(o1) = type(o2) 且 ref(state(o1)) = ref(state(o2))。 当创建新对象或修改现有对象的属性值时，系统配置 Π 会发生改变。对于每个类 C，用变量 Π(C) 表示类 C 的现有对象集合。 ### 1.2 外部变量 在程序的主方法中声明一组外部变量 extvar = {x1 : T1, ..., xk : Tk}，每个类型 Ti 称为 xi 的声明类型，记为 dtype(xi)。声明类型可以是内置基本类型或公共类。这些变量的值可由包含它们的主方法的方法和命令修改。 ### 1.3 局部变量 局部变量集合 localvar 由局部变量声明命令声明，包括 self（表示当前活动对象）和方法的参数。localvar 和 extvar 是不相交的集合。 由于方法调用可能嵌套，self 和方法参数可能会被多次声明，且类型可能不同。局部变量 x 有一系列声明类型 (x : ⟨T1, ..., Tn⟩)，用 TypeSeq 表示 x 的类型序列，T1 为最近声明的类型 dtype(xi)。 ### 1.4 可见性 引入变量 visibleattr 来保存对正在执行的命令可见的属性集合，其值定义了当前执行环境。对象 o 的方法将 visibleattr 设置为 Attr(o)（o 当前类型的属性），包括类的所有声明属性、其超类的受保护和公共属性以及公共类的所有公共属性；方法执行结束时，将 visibleattr 重置为全局环境（由公共类的所有公共属性组成）。 使用以下符号： - var 表示 extvar 和 localvar 的并集。 - VAR 是动态变量集合，包括 var 中的变量以及 Π 和 visibleattr。 - internalvar 是 VAR 中除 extvar 之外的元素集合。 ## 2. 动态状态 对于程序 S = Cdecls • Main，其动态状态 Γ 是从变量 VAR 到其值空间的映射，需满足以下条件： - 若 x ∈ VAR 且 dtype(x) 属于基本类型 T，则 Γ(x) 是 dtype(x) 中的值。 - 若 x ∈ VAR 且 dtype(x) 属于类名 cname，则 Γ(x) 要么为 null，要么是 v ∈ REF × CNAME 中的值，且存在对象 o ∈ Γ(Π) 使得 ref(o) = ref(v) 且 type(o) ⪯ type(v)。 两个状态 Γ1 和 Γ2 相等，当且仅当： - 对于任意 x ∈ VAR 且 dtype(x) 属于基本类型 T，Γ1(x) = Γ2(x)。 - 对于任意 x ∈ VAR 且 dtype(x) 属于类名 cname，Γ1(x) = null 当且仅当 Γ2(x) = null，且若 oi ∈ Γi(Π) 且 ref(Γi(x)) = ref(oi)（1 ≤ i ≤ 2），则 o1 = o2 且 type(Γ1(x)) = type(Γ2(x))。 对于状态 Γ 和子集 V ⊆ VAR，Γ(Π↓V) 将 Π 投影到 V 上，定义如下： - 若 x : C ∈ V，C 属于类名 cname，o ∈ Γ(Π) 且 ref(Γ(x)) = ref(o)，则 o ∈ Γ(Π↓V)。 - 若 o ∈ Γ(Π↓V) 且 a 是 type(o) 的类类型属性，o1 ∈ Γ(Π) 且 ref(o.a) = ref(o1)，则 o1 ∈ Γ(Π↓V)。 - Γ(Π↓V) 仅包含根据上述两条规则从 Γ(Π) 和外部变量的值构造的对象。 对于给定状态，表达式 e 可见（visible(e) 为 true）的条件如下： |条件|描述| |----|----| |1|e 是声明的简单变量，即 e 是 x，其中 x ∈ var| |2|e ≡ self.a 且存在类名 N ∈ cname 使得 N ⪰ atype(self) 且 N.a ∈ visibleattr| |3|e 形式为 e1.a 且 e1 不是 self，visible(e1) 为 true，存在 N ⪰ type(e1) 且 N.a ∈ visibleattr| ## 3. 表达式求值 表达式 e 在给定状态下的求值确定其类型 type(e) 及其值。若 type(e) 是内置基本类型，则值为 type(e) 的成员；否则，值为 REF × CNAME 中的元素。求值使用系统配置，仅对定义良好的表达式进行求值，定义良好的条件可以是静态和动态的。表达式的求值结果如下表所示： |表达式|求值| |----|----| |null|D(null) = true，type(null) = NULL，ref(null) = null| |x|D(x) = visible(x) ∧ (dtype(x) ∈ T ∨ dtype(x) ∈ cname) ∧ (dtype(x) ∈ T ⇒ head(x) ∈ dtype(x)) ∧ (dtype(x) ∈ cname ⇒ ref(head(x)) ∈ ref(Π(dtype(x))))，type(x) = dtype(x)（dtype(x) ∈ T），type(head(x))（否则）| |self|D(self) = self ∈ locvar ∧ dtype(self) ∈ cname ∧ ref(head(self)) ∈ ref(Π(dtype(self)))，type(self) = type(head(self))| |le.a|D(le.a) = D(le) ∧ le ≠ null ∧ dtype(le) ∈ cname ∧ visible(le.a)，type(le.a) = type(state(le)(a))，ref(le.a) = ref(state(le)(a))| |(C)e|D((C)e) = D(e) ∧ type(e) ∉ T ∧ atype(e) ⪯ C，type((C)e) = C，ref((C)e) = ref(e)| ## 4. 命令语义 ### 4.1 赋值 赋值 le := e 定义良好的条件是 le 和 e 都定义良好，且 e 的当前类型与 le 的声明类型匹配： ```plaintext D(le := e) = D(le) ∧ D(e) ∧ (type(e) ∈ cname ⇒ type(e) ⪯ dtype(le)) ``` 赋值有两种情况： - 重新将值赋给变量： ```plaintext [[x:=e]] = {x} : D(x:=e) ⊢ (x′ = ⟨value(e)⟩ · tail(x)) ``` - 修改附加到表达式的对象的属性值： ```plaintext [[l ```