成员等式逻辑规范的声明式调试

### 成员等式逻辑规范的声明式调试 #### 1. 引言 声明式语言在学术界之外的应用，因缺乏便捷的辅助工具（如调试器）而受到限制。传统上，声明式语言将问题逻辑（定义期望计算的内容）和控制（实际执行计算的方式）分开，这虽有优势，但在调试错误计算时会带来严重问题。由于其执行机制复杂，难以应用命令式语言中基于逐步跟踪调试器的典型技术。 因此，声明式语言领域引入了基于语言语义的新调试方法，如抽象诊断和声明式调试。声明式调试也称为算法调试，已广泛应用于逻辑、函数和多范式编程语言。它是一种半自动技术，从用户认为不正确的计算（错误症状）开始，定位导致错误的程序片段。该方法使用调试树逻辑表示计算过程，通过遍历调试树并向外部（通常是用户）询问，直到找到错误节点。错误节点是指结果错误但子节点结果正确的节点，对应错误的代码片段。 本文介绍了用于Maude功能模块的声明式调试器。Maude是一种高级语言和高性能系统，支持等式和重写逻辑计算，其模块通常对应重写逻辑规范。Maude功能模块对应成员等式逻辑规范，除方程外，还允许声明成员断言来描述元素所属的类别。 Maude系统支持多种调试方法，如跟踪、项着色和使用内部调试器，但这些方法存在不足。本文提出的声明式调试方法解决了功能模块调试中的问题，调试过程从初始项到意外的完全归约项的错误转换开始，调试器构建证明树后向用户提问，答案可帮助缩小调试范围。当前版本的工具具有以下特点： - 支持各种功能模块，包括不同的操作符属性、方程定义和模块参数化。 - 提供两种遍历调试树的策略：自上而下和分治查询。 - 用户可选择包含正确语句的模块，以减少向用户提问的数量。 - 允许用户调试标记了可疑方程和成员关系的模块，未标记的语句被视为正确，用户还可在调试过程中信任某些语句。 #### 2. Maude功能模块 Maude使用成员等式逻辑（MEL），这是一种表达性很强的等式逻辑，除方程外还允许声明成员断言。 ##### 2.1 成员等式逻辑 MEL中的签名是一个三元组 (K,Σ,S)，其中K是种类集合，Σ是多类签名，S是两两不相交的种类集合族。MEL的原子公式可以是方程 t = t′ 或成员断言 t : s，句子是全称量化的Horn子句。MEL规范的模型称为代数，一个Σ - 代数A由每个种类k的集合Ak、每个操作符的函数以及每个种类的子集组成。规范 (Σ,E) 有一个初始模型TΣ/E。 由于考虑的MEL规范需满足汇流性、终止性和种类递减性等可执行性要求，方程 t = t′ 可从左到右定向为 t →t′。在这些假设下，条件方程中的等式条件可通过找到公共项来检查。 ##### 2.2 在Maude中的表示 Maude功能模块使用语法 fmod ... endfm 引入，是可执行的MEL规范，其语义由满足规范的代数类中的相应初始成员代数给出。在功能模块中，可声明种类、子种类关系、操作符、成员关系和方程，Maude会自动从用户声明的种类和子种类关系中推断种类。 例如，操作符声明 “op _div_ : Nat NzNat -> Nat .” 逻辑上可理解为种类级别的声明和条件成员公理。 ##### 2.3 一个有错误的示例：非空排序列表 以下是一个在Maude中指定自然数排序列表的简单示例： ```maude (fmod SORTED-NAT-LIST is pr NAT . sorts NatList SortedNatList . subsorts Nat < SortedNatList < NatList . op __ : NatList NatList -> NatList [ctor assoc] . vars E E’ : Nat . var L : NatList . var OL : SortedNatList . cmb [olist] : E L : SortedNatList if E <= head(L) /\ L : SortedNatList . op head : NatList -> Nat . eq [hd1] : head(E) = E . eq [hd2] : head(L E) = E . op insertion-sort : NatList -> SortedNatList . op insert-list : SortedNatList Nat -> SortedNatList . eq [is1] : insertion-sort(E) = E . eq [is2 ```