面向切面编程中切面类别与时态属性的深入剖析

### 面向切面编程中切面类别与时态属性的深入剖析 #### 1 引言 面向切面编程旨在将横切关注点隔离到切面模块中，这些模块随后会与其他切面或更标准的面向对象类进行织入。不同的切面与基础程序的关联复杂程度各异。例如，日志记录或性能监控这类切面，对基础程序的影响相对较小；而处理整数计算溢出、限制特定用户对某些方法的访问等切面，影响则稍大；像为在线书店计算并应用折扣价格，或在建筑支持程序中更改建筑设计以满足残疾人访问规定的切面，与基础程序的计算联系更为紧密。 早期的研究提出了三种类型的切面：观察型、调节型和侵入型。观察型切面通常通过添加字段和方法来收集系统信息，但不影响基础计算；调节型切面改变控制流，如在特定条件下激活哪些方法，但不改变现有字段的计算；侵入型切面会改变现有字段的值，但不应破坏系统的理想属性。 本文对这些切面类别进行了扩展和细化，分析了不同类别切面如何影响系统属性。这些属性类别用通用时态逻辑公式描述，可用于系统细化和证明技术。通过这些类别和引理，某些属性可以自动确定，无需使用模型检查器进行昂贵的证明；对于其他属性和类别，验证虽不直接，但可使用更简单的证明方法。切面类别有助于软件开发，促进了模块化。 本文以一个处理分数的在线考试系统为例，该系统使用`Rational`类生成和检查简单算术练习的在线考试。`RationalExam`类负责启动考试、生成问题、接受答案并检查答案的正确性。后续会添加切面来汇总结果、限制系统使用和化简分数。 为了研究系统属性并对应用的切面进行分类，假设系统和切面都有规范。这些规范描述了系统的理想属性，通常只需确定属性所属的类别，如安全属性或不变属性，而无需确切知道规范的具体内容。规范应在系统添加切面或切面组合时得到维护。例如，在分数系统中，一个理想的不变属性是每个分数的分母为正，添加的切面应保持这一属性。 一般来说，当一个切面属于某个类别时，对增强系统的属性有不同的语义影响。最佳情况下，基础系统的属性类可自动在增强系统中保持；某些情况下，只需分析切面代码就能确定属性；最坏情况下，需考虑整个系统，但对于某些属性可使用更简单的证明方法。本文基于状态图的语义视图来证明关于切面类别和时态属性类型的引理。 #### 2 时态逻辑与属性类别 ##### 2.1 切面的规范 切面的规范需要描述在切面识别的每个连接点上基础系统的假设，以及在连接点满足假设时，建议应用后所需满足的条件。对于每个连接点和建议代码段，建议假设系统的某些属性，并在完成时保证某些属性（可能在切面执行期间也有一些属性）。这种假设 - 保证结构对于描述切面的附加价值至关重要。 由于许多切面处理非功能问题，如可用性、容错性、安全性或持久性，明确提供其规范更为困难。但这里不做区分，时态逻辑可用于规范功能和非功能属性。即使某些属性未正式表达，对于下面的属性分析，确定特定属性所属的规范属性类别（如不变属性）就足够了。 ##### 2.2 时态逻辑的语义 时态逻辑为描述执行序列的属性提供了形式化表示，使用时态模态词对执行序列和其中的状态进行量化。在线性时态逻辑的最简单版本（无存在属性）中，`G`表示“全局”，即从当前状态开始的所有状态；`F`表示“未来”，即最终存在一个状态。例如，断言`G(p => Fq)`表示在每个状态中，如果`p`为真，则最终会有一个状态`q`。`pUq`表示`p`在所有状态中保持，直到满足`q`的状态（且存在这样的状态）。`Xp`表示`p`在下一个状态中为真。 形式上，对于执行序列`σ`和其中的索引`i`： - `(σ, i)`满足`Gp`当且仅当`∀j ≥ i. p(σ(j))` - `(σ, i)`满足`Fp`当且仅当`∃ j ≥ i. p(σ(j))` - `(σ, i)`满足`pUq`当且仅当`∃ j ≥ i. q(σ(j)) ∧ ∀k. j >k≥ i. p(σ(k))` - `(σ, i)`满足`Xp`当且仅当`p(σ(i+1))` 线性时态逻辑（LTL）仅定义了这种格式的模态词。在分支时态逻辑（如CTL）中，还有路径量词`A`（表示所有可能的延续）和`E`（表示某些可能的延续）。时态逻辑公式在应用于系统时，基于Kripke结构语义进行解释，该结构由状态转换图组成，节点表示系统可达的可能状态，边表示系统的可能原子动作。 在线性时态逻辑中，断言对于系统为真，当且仅当它对于从初始状态开始的Kripke结构中的每个路径都为真；对于CTL，公式必须对于展开Kripke结构得到的执行树为真。因此，LTL断言`Gp`等价于分支时态逻辑断言`AGp`。 ##### 2.3 时态属性的类别 时态属性类别最早由相关研究定义，它们对应于简单的语法形式、证明方法和复杂度层次结构。 - **安全属性**：在每个状态中都成立，可能与当前状态之前的状态历史有关。这类属性描述了系统允许的操作、条件以及不可能出现的状态。所有安全属性都可以表示为`Gp`形式的LTL断言，其中`p`是不包含其他未来模态词的谓词，仅与状态变量或导致当前状态的过去历史有关。 - **（全局）不变属性**：是安全属性中最常见的子类，在每个状态中都为真，不考虑计算历史。在面向对象系统中，常见的较弱安全断言是类不变属性，要求在类的每个方法调用之前和之后都为真（方法调用期间不一定）。部分正确性断言也是一种不变属性，当系统终止时成立。类不变属性和部分正确性断言可以转换为全局不变属性的形式。 - **活性属性**：保证在每个可能的执行中最终成立。例如，某种方法激活的成功终止、每个发送的消息最终被接收等。这类属性总是可以使用未否定的最终性（`F`或`Until`）模态词来表达，常见的组合形式有`Fp`、`GFp`、`FGp`等。 - **存在属性**：在分支时态逻辑中，存在属性可以表达关于系统可能计算的断言，语法上等价于带有未否定的`E`路径量词的属性，与系统可能执行中的计算存在有关。 以下是这些属性类别的总结表格： | 属性类别 | 描述 | 语法形式 | 示例 | | --- | --- | --- | --- | | 安全属性 | 在每个状态成立，可能与历史有关 | `Gp`（`p`为过去谓词） | `G(denominator > 0)` | | 不变属性 | 每个状态都为真，不考虑历史 | `Gp` | `G(denominator > 0)` | | 活性属性 | 最终在每个执行中成立 | `Fp`, `GFp`, `FGp`等 | `F(answer_received)` | | 存在属性 | 关于可能计算的断言 | 带`E`量词 | `E(reach_interrupt)` | #### 3 切面和对象系统的语义 ##### 3.1 切面语义的方法 为了定义和推理切面类别及其与属性类别的联系，需要定义面向对象系统的形式和语义。有多种形式化的切面和切面系统语义定义方法，如指称语义、操作语义（小步语义）、进程演算和函数式方法。原则上，任何一种方法都可以用于证明切面类别与时态属性正确性之间的联系。大多数方法假设一个简化的对象或函数基础语言，以专注于新切面构造的语义定义。 ##### 3.2 对象系统的状态机语义 本文采用状态图语义视图，因为它最适合时态属性的验证，并且被软件模型检查器（如Bandera）使用。这种视图可以在UML状态图语义中看到，每个类都有一个状态图（相当于分层状态图），表示该类每个实例（对象）的可能状态和转换。 对象状态图中的节点为对象的变量、字段和控制状态提供特定值，边（转换）描述从该节点执行启用步骤的效果。系统由活动对象的状态图的交叉积描述，通过潜在的方法调用进行链接。以下是状态机语义的mermaid流程图： ```mermaid graph LR classDef startend fill:#F5EBFF,stroke:#BE8FED,stroke-width:2px; classDef process fill:#E5F6FF,stroke:#73A6FF,stroke-width:2px; classDef decision fill:#FFF6CC,stroke:#FFBC52,stroke-width:2px; A([开始]):::startend --> B(对象状态图):::process B --> C(节点 - 变量、字段、控制状态值):::process B --> D(边 - 执行效果):::process C --> E(交叉积):::process D --> E E --> F( ```