面向对象编程中的会话和联合类型

### 面向对象编程中的会话和联合类型 #### 1. 查找函数 在面向对象编程的会话和联合类型体系中，有几个重要的查找函数，如`ftypew`、`stype`、`rtype`和`sbody`。 - `ftypew`：返回对参数应用`ftypew`结果的交集。在没有多重继承的情况下，可能的情况相对明确，可避免引入交集类型。 - `stype`：返回一组会话类型。当以类名作为参数调用时，返回单例；以合适的联合类型调用时，返回对应参数类型集合的并集，涵盖构建联合类型的所有类的会话类型。 - `rtype`：以协变方式工作，因为结果对象不能用于写入模式。 - `sbody`：仅以类名作为类型参数调用，因为会话仅在对象上调用，而所有对象的类型都是类名。 可以验证，所有应用于等效联合类型的查找函数，在定义时会返回等效联合类型或相同的会话类型集合。 #### 2. 操作语义 在异步通信中传递的对象存储在堆中。堆`h`是一个有限映射，其定义域由对象和通道名组成，语法如下： ```plaintext h ::= [] |  →(, $ : ) |  →  | h::h ``` 其中`::`表示堆连接。在评估过程中，表达式` ()`会被新的对象标识符``替换，堆会将对象标识符``映射到其类名``和对应对象的字段列表``的对`(, $ : )`。 堆的操作包括更新对象字段和映射通道名到对象队列。例如，`h[ →h()[$ → ′]]`表示更新对象``的字段`$`为对象`′`；`h[ → ]`表示将通道``映射到队列``。 评估过程中使用了特殊的通道添加操作`...`和延续替换操作`⌊.../ ⌋`。表达式的减少是线程和堆对之间的关系：`P,h −→P′,h′`。减少规则使用评估上下文`E`来捕获“下一个要减少的子表达式”的概念，其语法如下： ```plaintext E ::= [−] | E ;  | E .$ | E .$ :=  | .$ := E | E .{ } | E • { } | .(E ){ 1 ⇒ 1  2 ⇒ 2} ``` 减少规则如下表所示： | 规则名称 | 规则内容 | | ---- | ---- | | PAR - R | `,h −→P,h′ || P1,h −→P || P1,h′` | | SEQ - R | `E [ ; ],h −→E [ ],h` | | FLD - R | `h() = (,  : ) E [ . i],h −→E [ i],h` | | NEWC - R | `fields() =    h E [   ()],h −→E [ ],h::[  →(,  : )]` | | FLDASS - R | `E [ .  := ′],h −→E [ ′],h[  →h()[  → ′]]` | | SESSREQ - R | `h() = (, ) sbody(, ) = ′ , ˜ h E [ . { }],h −→E [ ] || [ / ] ′ ˜ ,h[ , ˜ →()]` | | SESSDEL - R | `h() = (, ) sbody(, ) = E [ • {}],h −→E [[ / ] ],h` | | SENDCASE - R | `h(˜ ) =  h() = (, )  ⇓{1, 2} = i E [ .  (){1 ⇒ 1  2 ⇒ 2}],h −→E [ i],h[˜ →  :: ]` | | RECEIVECASE - R | `h() =  ::  h() = (, )  ⇓{1, 2} = i E [ . (){1 ⇒ 1  2 ⇒ 2}],h −→E [[ / ] i],h[ → ]` | | SENDWHILE - R | `E [ .  ( ){1 ⇒ 1  2 ⇒ 2}],h −→E [ .  ( ){1 ⇒ ′ 1  2 ⇒ ′ 2}],h` 其中 ` ′ i = ⌊ i/⌋.  ( ){1 ⇒ 1  2 ⇒ 2}/` | | RECEIVEWHILE - R | `E [ . (){1 ⇒ 1  2 ⇒ 2}],h −→E [ . (){1 ⇒ ′ 1  2 ⇒ ′ 2}],h` 其中 ` ′ i = ⌊ i/⌋. (){1 ⇒ 1  2 ⇒ 2}/` | 这些规则定义了并行线程的执行、标准面向对象构造的执行以及会话请求、会话委托和通信操作