析取回答集程序设计结构化测试方法

杨 东，王以松

（贵州大学 计算机科学与技术学院，贵阳 550025）

0 引言

回答集程序设计（Answer Set Programming，ASP）是语法上基于传统逻辑程序设计（Prolog）而语义上基于稳定模型语义的非单调的一种描述式程序设计范式［1］。在ASP 中，搜索问题被简化为计算稳定模型，通过回答集求解器（用于生成稳定模型的程序）执行搜索得到问题的解。由于回答集程序的非单调特征、良好的表达能力以及各种有效的求解器（如clasp、dlv）的出现，ASP 已经在众多的人工智能领域得到了广泛运用，包括规划［2］、机器人［3-4］、知识推理［5］、决策支持［6］、电路诊断以及硬件设计［7-8］、自动驾驶［9］等。

回答集程序的工程化（包括软件调试、软件测试等）历经多年的发展取得了一定的成果：Janhunen 等［10］将过程式程序设计语言（包括C、Java 等）的测试覆盖方法引入到正规回答集程序，提出正规回答集程序的测试理论后；Janhunen 等［11］在此理论基础上实现了正规回答集程序的结构化测试方法，与随机测试实验结果的比较表明，虽然在测试结果上很难体现出随机测试和结构化测试的优劣性，但在某些特定的代码场景下，结构化测试方法相较于随机测试方法有着显著的规则异常捕获优势；Oetsch 等［12］提出了小范围内穷尽测试的测试方法测试正规回答集程序，在4 类包括增删规则和文字、谓词和变量重命名等共20 种回答集程序变异操作中，用不超过13 个个体符号的测试能达到99%的置信度；Febbraro等［13］提出了一种用于在ASP 中指定和运行单元测试的语言，该测试语言是在回答集编程集成开发环境（Integrated Development Environment for Answer Set Programming，ASPIDE）中实现的，支持回答集程序的全生命周期开发，将回答集程序的测试、调试、分析、求解器执行配置和输出等功能集成在一个对用户友好的图形化工具中；Busoniu 等［14］开发了一个回答集编程的集成开发环境SeaLion，为Gringo 和DLV（DataLog with Disjunction，where the logical disjunction symbol V is used）提供源代码编辑器，并提供如语法高亮显示、语法检查、代码完成、可视化程序和代码重构功能，显著提升了回答集程序开发人员的编程效率；Greβler 等［15］设计了正规回答集程序的测试工具Harvey，使用ASP 规则定义测试输入空间，并使用异或抽样实现测试输入对正规回答集程序进行随机测试；Amendola 等［16］提出了一种基于ASP 的测试执行机制以及在ASP 程序中进行内联测试的单元测试规范语言，并用该语言开发提供了一个支持测试驱动开发（Test-Driven Development，TDD）ASP 程序的编程环境。

析取回答集程序的表达能力严格强于正规情形［17］，判断一个析取回答集程序是否存在回答集是-完全的，而对正规回答集程序时是NP（Non-deterministic Polynomial）-完全的，因而析取回答集程序比正规回答集程序更复杂，应用范围也更广。然而，目前国内外仍缺少对析取回答集程序测试的深入研究，既缺乏其测试的理论基础，更没有系统化地析取逻辑程序自动化测试工具。

本文通过初步构建析取回答集程序的测试理论，模拟结构化测试方法中的语句覆盖、分支覆盖等覆盖形式，并给出相应的覆盖率计算方法，为进一步实现析取回答集程序自动化测试提供理论支持。

本文的主要工作包括3 个方面：

1）将回答集程序结构化测试的理论扩展到析取回答集程序，进一步扩大原有的测试理论和公式的应用范围；由析取回答集程序的规则可知，正规回答集程序的规则头满足只有一个原子的情形，也就是说正规回答集程序是析取回答集程序的特例。本文提出的析取回答集测试理论是正规回答集程序测试理论的泛化，即本文的测试理论不仅可以运用于析取回答集程序，也可运用于正规回答集程序，反之则不行。

2）对析取回答集程序的部分特殊性质和定理进行了提取、分析和证明。

3）提出了回答集程序的解释I的重要指标，通过该指标可以衡量不同解释I对回答集程序的规则满足性，从而判断解释I的有效性。

1 预备知识

下面主要介绍析取回答集程序的基础知识和定义，并给出析取回答集程序的实例和稳定模型的具体计算方法。

1.1 析取回答集程序

假设命题语言L建立在原子集合A之上。一个析取回答集程序P由一系列规则（rule）组成，这些规则的形式是：

其中：ai(1 ≤i≤k)，bj(1 ≤j≤m)，ct(1 ≤t≤n) 都是原子公式。对于回答集程序P中的任一规则，有：

1）a1∨a2∨… ∨ak表示该规则的头；

2）b1，b2，…，bm，notc1，notc2，…，notcn表示该规则的体。

特别地，当k=1 时，析取逻辑规则转为正规逻辑规则，即a1←b1，b2，…，bm，notc1，notc2，…，notcn。回答集程序中的否定形式为缺省否定，即对于一个原子集合S，notS={notp|p∈S}，给定式（1）中的规则r，有如下定义：

通常规则r的表达式简写为：hd(r) ←bd(r)。析取回答集程序示例如下。

例1 图的着色问题。给定一个图G，有三种颜色可以用于对图着色，要求相邻两个端点的颜色不同而且每个节点只有一种颜色。用node（X）表示顶点，边edge（X，Y）表示X、Y两个顶点之间有边，颜色用col（C）表示，三种颜色分别是｛red，green，blue｝，某个点着色用color（X，C）表示，则表示着色的析取逻辑程序为：

规则r1为析取规则，表示每一个节点可从三种颜色中选取一种颜色着色；规则r2表示相邻两个节点的颜色不能为同一个颜色；规则r3、r4、r5表示若点着了红蓝绿其中一种颜色后，就不能再着其他颜色。

1.2 析取回答集程序的回答集

命题语言L的解释是一函数I：A→{0，1}，其中I(p)=1表示给命题p赋值为真，I(p)=0 表示命题p赋值为假。一个解释I是来自集合A的原子的集合。若某个原子包含在I中，则表示该原子被赋值为真，否则赋值为假。

例2 若I={b}，P=b←a，则表示b赋值为真，且b为真时，命题P也为真。

若命题公式φ在解释I下为真，则称I⊨φ。若I满足命题理论Σ中的所有公式，则称I满足Σ；若I满足命题公式（集）则称I是该命题公式集的模型。解释I是逻辑程序P的模型（表示I满足P），记为I⊨P，其中符号满足(⊨)定义为：

1）对于一个原子p：I⊨p当且仅当p∈I；I⊨notp当且仅当I⊨p不成立；

2）对于一个集合S：I⊨S当且仅当I⊨s对于每一个s∈S，其中S的元素可以是原子p，或其缺省否定notp，或规则；

3）对于一条规则r：I⊨r当且仅当I⊨bd(r) 蕴含I⊨hd(r)。

一个程序P的模型I是P的极小模型，当且仅当不存在另外一个模型I′使得I′ ⊂I。给定一个程序P和一个解释I，PI={hd(r) ←pos(r)|r∈P，neg(r) ∩I=∅}是P关于I的G-L（Gelfond-Lifschitz）规约；若解释I是PI的极小模型，则称I是程序P的回答集［18］。对于一个逻辑程序P和一个原子a∈A，程序P定义原子a的规则集合，记为defP(a)={r∈P|a∈hd(r)}，也 称DefP(a) 中的规则定义了原子a。DefP(a，I)表示在解释I下程序P中定义原子a的规则集合，记为：defP(a，I)={r∈P|a∈I∩hd(r)}。P关于I的支撑规则集合定义为：{r∈P|I⊨bd(r)}，记为SuppR(P，I)。

2 测试理论

本章详细介绍软件工程中的测试方法，然后根据析取回答集程序的特点提出测试的思想和测试用例的概念，主要分为两个部分：一是阐述析取回答集程序结构化测试方法的技术路线；二是定义结构化测试方法以及测试用例的概念。

2.1 析取回答集程序结构化测试技术路线

软件测试是使用人工或自动的手段来运行或测定某个软件系统的过程，其目的在于检验它是否满足规定的需求或弄清预期结果与实际结果之间的差别［19］。软件工程领域的测试包括黑盒测试和白盒测试。黑盒测试是将软件看成一个盒子，测试人员无须考虑其内部逻辑结构，根据规格说明书设计测试用例。黑盒测试重点关注软件实现和规格说明书的一致性，根据输入/输出确定的逻辑关系设计测试数据，以检查其是否正确。白盒测试又称结构测试、透明盒测试、逻辑驱动测试或基于代码的测试。白盒测试是一种测试用例设计方法，盒子指的是被测试的软件，白盒指的是盒子是可视的，即清楚盒子内部的东西以及里面是如何运作的。白盒法全面了解程序内部逻辑结构，对所有逻辑路径进行测试［20］。

要采用白盒测试，首先就必须要设计合理的软件测试用例。软件测试用例是指对一项特定的软件产品进行测试任务的描述，体现测试方案、方法、技术和策略。测试用例是为某个特殊目标而编制的一组测试输入、执行条件以及预期结果，用于核实是否满足某个特定软件需求［21］。因此，对析取逻辑程序测试的思路是：首先对析取回答集程序定义测试用例（Test Case）的概念，通过构造析取回答集程序测试用例的输入、输出；然后利用软件测试的各项覆盖标准来实现析取回答集程序的测试覆盖，在此过程中设计和提出析取回答集程序的测试相关概念。

此外，还考虑到析取回答集程序语法的两个特点。

第一个特点是：规则（rule）是程序最重要的语法结构之一，测试理论的主要对象为析取回答集程序的规则。对于析取回答集程序的规则测试，又可以细分出对规则体、规则头、规则集合等测试对象。

第二个特点是：析取回答集程序不是顺序执行的特点，无法对析取回答集程序的某个断点进行测试。根据一个测试输入的解释I运算出来的回答集与标准回答集进行比对，以此来验证程序是否符合预期。

综上，结构化测试方法使得测试人员更加清楚地了解软件的内部结构和运行机制，从而更好地设计测试用例，为后续的测试实验设计提供方便，而且结构化测试方法通过统计代码覆盖率、路径覆盖率等技术指标对代码的测试更加明确。

2.2 析取回答集程序的测试用例

首先给出析取回答集程序的测试用例的定义。设P是一个析取回答集程序，IP、OP分别是程序P的输入原子集合字母表和输出原子集合字母表，假设I⊆IP，P[I]是逻辑程序P在解释I下的回答集，表示为定义一个P的规约满足映射关系σP，即程序P从集合IP到集合OP上的映射关系是σP，定义为σP：IP→。则给定一个输入I后，P的正确输出为σP(I)。由此对测试用例的定义如下。

定义1测试用例。P是一个任意的析取回答集程序，σP是P的一个规约，P和σP定义的测试用例为一对序偶T=I，O，其中I⊆IP，O=σP(I)。程序P通过测试用例的条件为P[I]=O。

例3 设析取回答集程序P有如下3 条规则：

通过程序P及其映射σP，很容易验证程序P在每一个测试用例T=I，O下测试均通过。一个析取回答集程序P和σP的测试套件S是P和σP的测试用例的集合。程序P测试通过测试套件S的条件是P测试通过S中的每一个测试用例。程序P关于σP正确的条件是：当且仅当P测试通过P和σP的每一个测试用例。

3 覆盖函数以及覆盖率

通过实例分析，确定相关的测试覆盖指标，以此衡量测试用例的覆盖情况。

3.1 结构化测试的覆盖形式

结构化测试在测试执行时需要每一行代码至少执行一次（语句覆盖）、遍历所有的程序分支（分支覆盖）或者其他的可能的分支，其覆盖标准有逻辑覆盖、循环覆盖和基本路径测试。根据析取回答集程序的语法规则和测试对象的差异性，给出相应的覆盖函数定义以及各覆盖条件下的函数，并给出具体的计算方法。

3.2 覆盖函数

定义2覆盖函数。逻辑程序P和测试输入集合的覆盖函数γ定义为γ：I×P→[0，1]，对于每个程序P和每个关于P的输入集合I ⊆，以下性质成立：

1）γ(I，P)=1，当且仅当I=；

2）γ(I′，P) ≤γ(I，P)，当且仅当P的每一个输入集合I′⊆I。

在这里说I 是解释的集合，当γ(I，P)=1 时，满足的条件为I=，可以生成所有逻辑程序P的覆盖。其次，析取回答集程序的覆盖函数的形式虽然与正规回答集程序相似，但是二者的含义却有不同，析取回答集程序产生的输入、输出集合的涵盖范围比正规回答集程序的范围大。

在软件工程中，如果一个测试用例使得被测试的文件（类或者函数）中所有的语句（判定）至少被执行到一次，那么这种测试覆盖准则被称为语句（判定）覆盖。软件工程中测试覆盖率的计算方法［20］如下：

考虑到析取回答集程序中没有语句、分支的概念，因此假设在输入I ⊆的情况下，其规则、定义、环以及子程序的覆盖数量与全部输入案例产生的规则、定义、环以及子程序的覆盖数量比值作为覆盖率。析取回答集程序的覆盖率公式定义为：

根据以上的覆盖率计算公式，可以计算出析取回答集程序的结构化测试方法中各覆盖形式下的覆盖率。

3.3 析取回答集程序的测试覆盖率

由于在析取回答集程序测试中，代码被逻辑规则替代，在回答集程序中，每行规则都会执行，因此需要测试回答集程序中的每一条规则。而测试覆盖率是测试在给定的解释I下，规则r是否满足，并且规则又可分为规则的头、规则的体、规则集合等不同的测试对象，根据测试对象的满足情况，得到析取回答集程序的以下各种覆盖。

在面向过程的程序测试方法中，路径覆盖法主要是通过测试用例的执行，覆盖程序中所有可能的路径。由于在析取回答集程序中，规则与规则不会产生分支执行，因此使用部分规则组成的集合作为一个子程序，通过对子程序的覆盖来模拟路径覆盖的概念。

定义3子程序覆盖。设P是一个析取回答集程序，I⊆IP且P′⊆P。当P′=SuppR(P，X) 对某回答集X∈AS(P∪I)成立时，I覆盖P′。

例4 设析取回答集程序P有例3 中的3 条规则：

其中IP=OP={a，b}，I={a，b}，有X∈AS(P∪I)={{a，b}}，P′={r1，r2，r3}，可知P′=SuppR(P，X)，I覆盖P′。按照计算覆盖率的方法，很容易知道对于任意的I⊆IP都有AS(P∪I)={{a，b}}，即对于任意的I⊆IP都覆盖了同一个SuppR(P，X)，根据上面的计算式有：

在结构化测试方法中，由于面向过程的编程语言并非每行代码都会执行，只能通过执行过的代码块占总代码的比率，判断测试用例的好坏。语句覆盖是结构化测试方法中的一个重要指标，要求测试过程中，测试用例尽可能地测试到每一条代码，以此衡量测试用例是否真正完全覆盖了应用程序代码中的各种可能以及在运行这些测试用例时执行了多少代码，所以通过测试规则体的是否满足来模拟语句覆盖。

定义4规则覆盖。给定一个析取回答集程序P，r∈P，I⊆IP。如果对某个回答集X∈AS(P∪I)时，有X⊨bd(r)成立，则规则r∈P被I正覆盖。如果对回答集X∈AS(P∪I)，有X⊭bd(r)，则r被I负覆盖。此外，r被测试用例T正覆盖，当且仅当r被I正覆盖。

例5 设析取回答集程序P为例3 中的程序，其中IP=OP={a，b}，I1={a，b}和I2={a}，则有AS(P∪I1)={{a，b}}，可知I1覆盖了规则r1，r2，r3；对于AS(P∪I2)={{a，b}}，可知I2覆盖规则r1，r2，r3。

在关注规则的满足性时主要用到的是规则覆盖，但是在计算不同规则头之间是否递归满足时，需要用到环覆盖的概念。

定义5环覆盖。设P是一个析取回答集程序，I⊆IP。LP是P的一个环当且仅当有某个回答集X∈AS(P∪I)，使得原子a由r∈SuppR(P，X)所定义，且对于定义的每个原子a都 有a∈LP，则P的 环LP被I正覆盖。若有一个规则r∈SuppR(P，X) 定义了a，但是对于某个回答集X∈AS(P∪I)，defP(a，X) ≠∅，若没有 规则SuppR(P，X)定义a，则LP被I负覆盖。

例6 以例3 中的程序为例，其中IP=OP={a，b}，该程序的回答集是AS(P∪I)={{a，b}}，该回答集对应的环除单环{a}，{b}外，还有环LP={a，b}。同理，在计算环覆盖时用如下方法：

参照例3 的程序，知道对于任意的I⊆IP都有AS(P∪I)={{a，b}}，设I={a，b}⊆IP，程 序P存在环LP=，根据上面的计算式计算环覆盖率，有：

与面向过程的编程语言不同，析取回答集程序的规则中包含了规则的头，为了测试每条规则的头是否满足，给出定义覆盖的概念。

定义6定义覆盖。设P是一个析取回答集程序，a∈A，I⊆IP。若对于某个回答集X∈AS(P∪I)，存在规则满 足r∈SuppR(P，X) 定义了原子a，记 为defP(a，X)={r∈P|a∈X∩hd(r)}，称原子a被I正覆盖。若defP(a，X) ≠∅且不存在规则r∈SuppR(P，X)定义的a，则称a被I负覆盖。

例7 以例3 中程序P为例，其中IP=OP={a，b}，该程序的回答集是AS(P∪I)={{a，b}}，该回答集对应的规则正覆盖了原子a，原子b。同理，对于任意的I⊆IP，可得其规则正覆盖函数coveredD+(I，P)=2，负覆盖函数coveredD-(I，P)=0，而coveredD({I}，P)=2，因此有：

环覆盖和定义覆盖有一定的相似性，原因是在于两者都是为了测试规则头的满足性，但是两者测试的规则头又有不同的特点。定义覆盖是针对单个的规则头，即单个的原子满足性。而环覆盖则是为了测试规则头的集合，在这个规则头集合中，原子之间存在着一定的递归满足关系。

由以上的各覆盖测试条件，设covered*+(I，P)表示规则（定义、环、子程序）的正覆盖，covered*-(I，P)表示规则（定义、环、子程序）的负覆盖，总结得到覆盖公式为：covered*(I，P)=covered*+(I，P)+covered*-(I，P)，其中* ∈{R，D，L，P}。

性质1covered*(∅，P)=0 对任意的逻辑程序P成立，其中* ∈{R，D，L，P}。

推论2P是析取回答集程序，若P∪I对任意I⊆IP都有唯一的回答集，则有SuppR(P，X)=P对于任意的和X∈{P，R}成立。

证明 采用反证法证明。假设SuppR(P，X) ≠P且P∪I有唯一的回答集，对于任意的I⊆IP成立。假设存在某条规则r∈P，并且使得对于回答集X∈AS(P∪I) 有r∉SuppR(P，X)。由于AS(P∪I)有唯一的回答集，则根据推 论1 可 知CR(I，P)=1。若此时r∉SuppR(P，X)，则 有coveredX(，P) ＞coveredX(I，P)，且CR(I，P) ≠1。这与假设矛盾。证毕。

定义7支撑规则比值函数。函数α是指对于某个析取回答集程序P和它的解释I⊆IP，其支撑规则集合的势与程序规则组成的集合的势之比。其中，支撑规则集合的势作为分子，析取回答集程序P的规则组成的集合的势作为分母。记为：

α是一个重要的指标，主要用于衡量和计算一个析取回答集程序中，其解释I对于某个回答集X∈AS(P∪I)中支撑规则与程序规则的势之比，由此可以评估出逻辑程序P在解释I的非支撑规则的冗余数量，此外还可以评估解释I的有效性。

例8 设逻辑程序P有如下规则：

I={a，b}，对该程序求解回答集得到回答集：AS(P∪I)={{d，b，a，e}}，其支撑集合的势为‖SuppR(P，X)‖=4，‖P‖=5，α=80%。

推论3P是一个析取回答集程序，若P∪I对任意I都有唯一的回答集，则对于任何非空的I⊆，则有α=100%。

证明由推论 2 可知，SuppR(P，X)=P，则有‖SuppR(P，X)‖=‖P‖。根据支撑规则函数的计算式有：

4 结语

本文推广了命题正规逻辑程序结构化测试基本思想到命题析取逻辑程序，提出了命题析取逻辑程序规则覆盖、子程序覆盖、定义覆盖、环覆盖等基本的结构化测试评价准则，并探讨了它们的一些基本性质。接下来将进一步推广这些基本概念到带变元、带聚合函数（sum、min、max 等），以及抽象约束原子的一般逻辑程序，并进一步实现一般回答集程序的自动结构化测试。