逻辑程序中自动绑定相关错误诊断

### 逻辑程序中自动绑定相关错误诊断 #### 1. 抽象与或图遍历 绑定错误搜索过程的核心在于遍历抽象与或图的部分节点，并执行抽象操作，从而得到抽象替换，这与分析过程中的操作类似。我们需要一个遍历抽象与或图的概念，同时用新生成的抽象替换替换现有的抽象替换。 将所有替换都替换为 λ⊤ 的抽象与或图 R 记为 R⊤。 **定义 1（抽象与或图 R 的前向遍历，转换 ⇒R 的定义）** 设 ⇒R 是抽象与或图 R 节点上的一个转换： - **进入（Entry）**：⟨λ′j−1, B′j, λ′j⟩OR ⇒R ⟨λc, H, λs⟩AND，如果 H ∈ children(B′j) - λadd := Aunif(B′j, H, λ′j−1) - λc := Aproj(λadd, vars(H)) - **进入体（Enter Body）**：⟨λc, H, λs⟩AND ⇒R ⟨λ0, B1, λ1⟩OR，如果 B1 ∈ children(H) - λ0 := Aextend(λc, vars(H ← B1, ..., Bn)) - **右移（Move Right）**：⟨λi−1, Bi, λi⟩OR ⇒R ⟨λi, Bi+1, λi+1⟩OR，如果 ∃H′，{Bi, Bi+1} ⊆ children(H′) - **退出体（Exit Body）**：⟨λn−1, Bn, λn⟩OR ⇒R ⟨λc, H, λs⟩AND，如果 Bn ∈ children(B) 且 |children(B)| = n（即 Bn 是 H 的最右子节点） - λs := Aproj(λn, vars(H)) - **退出（Exit）**：⟨λc, H, λs⟩AND ⇒R ⟨λ′j−1, B′j, λ′j⟩OR，如果 H ∈ children(B′j) - λadd := Aunif(H, B′j, λs) - λext := Aextend(λadd, vars(H′ ← B′1, ..., B′n′)) - λ′j := Aconj(λc, λext) 如果从上下文可以清楚知道 R，我们将省略 ⇒R 中的下标 R。我们将 ⇒R 关系扩展到有限节点序列 s = [s1, ..., sn] 的遍历，记为 s⇒R，定义如下：s1 s⇒R sn 当且仅当 ∀1 ≤ i < n，si ⇒R si+1。“:” 运算符表示节点序列的连接。对于给定的 s，s⊤ 表示与 s 相同但所有替换都替换为 λ⊤ 的节点序列。 s⇒ 关系是我们绑定错误搜索算法的基础。注意，s⇒ 模拟了抽象解释执行的基本操作，因此可以安全地近似具体语义。如果一个抽象与或图是由抽象解释过程直接装饰的，即之后没有被 s⇒ 修改过任何节点，那么称该抽象与或图是 “新鲜的”。 **引理 1**：设 R 是对程序 P 进行分析得到的新鲜抽象与或图。假设 R 中有一个或节点 N = ⟨λi, A, λi+1⟩OR。同时假设在执行 P 时出现一个子推导 D = ←(A, ...)θ +; ←(B, ...)θθ′。 - (i) 如果 θ|A ∈ γ(λi)，那么存在一个节点序列 s，使得 N s⇒⟨λ′j, B, λ′j+1⟩OR 且 θθ′|B ∈ γ(λ′j)。 - (ii) 此外，存在一个对应的或节点 N ∗ = ⟨λ⊤, A, ⟩OR 和 R⊤ 中的一个节点序列 s⊤，使得 N ∗ s⊤⇒⟨λ∗j, B, ⟩OR 且 θθ′|B ∈ γ(λ∗j)（显然，我们有 λ′j ⊑ λ∗j）。 我们称 s 和 s⊤ 近似子推导 D。 **推论 1**：在引理 1 的假设下，(ii) 部分对所有 θ 都成立。 由于 s⇒ 执行的抽象操作序列与整个抽象解释过程相同，但仅限于抽象与或图中的一条特定路径，因此显然 s⇒ 的每一步生成的抽象替换都不比静态分析器生成的更一般。换句话说，s⇒ 相对于完整分析过程不会损失精度。 现在我们来证明应用 s⊤⇒ 定位绑定错误的合理性。 **命题 1**：设 ..., Bi a⃝Bi+1, ... 是程序 P 中一个子句体的片段，其中 λP rop 是点 a⃝ 处的期望属性。设 R 表示对 P 进行静态分析得到的（新鲜）抽象与或图。假设在 R⊤ 中存在一个节点序列 s⊤ 和一个带有原子 B′ 的或节点，使得 ⟨λ⊤, B′, λ⊤⟩OR s⊤⇒⟨λ∗i, Bi+1, ⟩OR。 如果 λ∗i ⊓ λP rop = ⊥，并且存在一个到达 a⃝ 且被 s⊤ 近似的子推导 D，那么 D 在 a⃝ 处包含一个症状。此外，以 B′ 为最左原子且具有相应替换的推导状态是与该症状相关的绑定错误。 证明：由推论 1 可得。 需要注意的是，尽管 s⇒ 关系近似具体语义，但它更细粒度，因为 s⇒ 可以区分 SLD 推导中被视为一步的操作，这些操作包括在消解式中选择原子、进入和退出子句。实际上，s⇒ 遍历的起始节点不一定是或节点，也可以是与节点。这使我们有机会比 SLD 消解语义更精确地定位一些错误。 #### 2. 示例 下面通过一个示例来解释如何使用 s⇒ 转换来定位绑定错误。总体思路是从症状开始遍历抽象与或图，以深度优先搜索（DFS）的方式逆着执行方向进行。这样就可以只检查在症状出现之前参与（抽象）执行的节点，从而找出可能包含错误的节点。 考虑以下 `slowsort` 示例： ```prolog slowsort(L,S) :- perm(L,S), sorted(S). perm([],[]). % 这里有一个错误: perm(L,[H,L1]) :- del(L,H,L2), perm(L2,L1). del([H|L],H,L). del([H|L],E,[H|L1]) :- del(L,E,L1). sorted([]). sorted([_]). sorted([X,Y|L]):- X =< Y, sorted([Y|L]). ``` `slowsort` 程序的目的是对数字列表进行排序，它首先生成输入列表的一个排列，然后检查生成的排列是否为有序列表。`perm/2` 谓词通过非确定性地从列表中移除一个元素（使用 `del/3` 谓词）来生成排列，然后对剩余列表递归调用自身。`sorted/2` 谓词用于检查列表是否有序。 可以为该代码添加一个入口声明：`:- entry slowsort(A,B) : list(A,num).`，该声明指定了对顶级/导出谓词的预期初始调用模式，静态分析器将其作为（自顶向下）分析图的起点。 注意，`perm/2` 的第二个子句头部存在绑定错误，正确的头部应该是 `perm(L,[H|L1])`。这个错误会导致在计算到达 `sorted/1` 的第三个子句中的库谓词 `=/2` 时引发运行时异常（“非法算术表达式”），因为输入列表的第二个元素 Y 本身是一个列表，而不是我们期望的数字。 在 Ciao 系统库中，谓词配备了指定其预期调用和成功模式的断言。因此，诊断程序可以知道 Y 的预期值（得益于分析的模块化性质），而无需用户事先做任何工作。实际上，静态断言检查能够检测到 Y 的值是类型 `rt21`，由以下正则项语法规则定义： ``` rt21 →[ ] rt21 →[num, rt21]. ``` 这意味着类型 `rt21` 的项要么是空列表，要么是一个二元列表，第一个元素是数字，第二个元素是类型 `rt21` 的项。因此，Y 的值与 `=/2` 断言中出现的预期类型 `arithexpr`（算术表达式）不兼容。 将这个点作为我们诊断会话的起始症状。 分析器生成的抽象与或图 R 的一部分如下： ```mermaid graph LR classDef or fill:#E5F6FF,stroke:#73A6FF,stroke-width:2px; classDef and fill:#FFF6C ```