析取回答集程序設(shè)計(jì)結(jié)構(gòu)化測(cè)試方法

楊 東，王以松

（貴州大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，貴陽(yáng) 550025）

0 引言

回答集程序設(shè)計(jì)（Answer Set Programming，ASP）是語(yǔ)法上基于傳統(tǒng)邏輯程序設(shè)計(jì)（Prolog）而語(yǔ)義上基于穩(wěn)定模型語(yǔ)義的非單調(diào)的一種描述式程序設(shè)計(jì)范式［1］。在ASP 中，搜索問(wèn)題被簡(jiǎn)化為計(jì)算穩(wěn)定模型，通過(guò)回答集求解器（用于生成穩(wěn)定模型的程序）執(zhí)行搜索得到問(wèn)題的解。由于回答集程序的非單調(diào)特征、良好的表達(dá)能力以及各種有效的求解器（如clasp、dlv）的出現(xiàn)，ASP 已經(jīng)在眾多的人工智能領(lǐng)域得到了廣泛運(yùn)用，包括規(guī)劃［2］、機(jī)器人［3-4］、知識(shí)推理［5］、決策支持［6］、電路診斷以及硬件設(shè)計(jì)［7-8］、自動(dòng)駕駛［9］等。

回答集程序的工程化（包括軟件調(diào)試、軟件測(cè)試等）歷經(jīng)多年的發(fā)展取得了一定的成果：Janhunen 等［10］將過(guò)程式程序設(shè)計(jì)語(yǔ)言（包括C、Java 等）的測(cè)試覆蓋方法引入到正規(guī)回答集程序，提出正規(guī)回答集程序的測(cè)試?yán)碚摵?；Janhunen 等［11］在此理論基礎(chǔ)上實(shí)現(xiàn)了正規(guī)回答集程序的結(jié)構(gòu)化測(cè)試方法，與隨機(jī)測(cè)試實(shí)驗(yàn)結(jié)果的比較表明，雖然在測(cè)試結(jié)果上很難體現(xiàn)出隨機(jī)測(cè)試和結(jié)構(gòu)化測(cè)試的優(yōu)劣性，但在某些特定的代碼場(chǎng)景下，結(jié)構(gòu)化測(cè)試方法相較于隨機(jī)測(cè)試方法有著顯著的規(guī)則異常捕獲優(yōu)勢(shì)；Oetsch 等［12］提出了小范圍內(nèi)窮盡測(cè)試的測(cè)試方法測(cè)試正規(guī)回答集程序，在4 類包括增刪規(guī)則和文字、謂詞和變量重命名等共20 種回答集程序變異操作中，用不超過(guò)13 個(gè)個(gè)體符號(hào)的測(cè)試能達(dá)到99%的置信度；Febbraro等［13］提出了一種用于在ASP 中指定和運(yùn)行單元測(cè)試的語(yǔ)言，該測(cè)試語(yǔ)言是在回答集編程集成開發(fā)環(huán)境（Integrated Development Environment for Answer Set Programming，ASPIDE）中實(shí)現(xiàn)的，支持回答集程序的全生命周期開發(fā)，將回答集程序的測(cè)試、調(diào)試、分析、求解器執(zhí)行配置和輸出等功能集成在一個(gè)對(duì)用戶友好的圖形化工具中；Busoniu 等［14］開發(fā)了一個(gè)回答集編程的集成開發(fā)環(huán)境SeaLion，為Gringo 和DLV（DataLog with Disjunction，where the logical disjunction symbol V is used）提供源代碼編輯器，并提供如語(yǔ)法高亮顯示、語(yǔ)法檢查、代碼完成、可視化程序和代碼重構(gòu)功能，顯著提升了回答集程序開發(fā)人員的編程效率；Greβler 等［15］設(shè)計(jì)了正規(guī)回答集程序的測(cè)試工具Harvey，使用ASP 規(guī)則定義測(cè)試輸入空間，并使用異或抽樣實(shí)現(xiàn)測(cè)試輸入對(duì)正規(guī)回答集程序進(jìn)行隨機(jī)測(cè)試；Amendola 等［16］提出了一種基于ASP 的測(cè)試執(zhí)行機(jī)制以及在ASP 程序中進(jìn)行內(nèi)聯(lián)測(cè)試的單元測(cè)試規(guī)范語(yǔ)言，并用該語(yǔ)言開發(fā)提供了一個(gè)支持測(cè)試驅(qū)動(dòng)開發(fā)（Test-Driven Development，TDD）ASP 程序的編程環(huán)境。

析取回答集程序的表達(dá)能力嚴(yán)格強(qiáng)于正規(guī)情形［17］，判斷一個(gè)析取回答集程序是否存在回答集是-完全的，而對(duì)正規(guī)回答集程序時(shí)是NP（Non-deterministic Polynomial）-完全的，因而析取回答集程序比正規(guī)回答集程序更復(fù)雜，應(yīng)用范圍也更廣。然而，目前國(guó)內(nèi)外仍缺少對(duì)析取回答集程序測(cè)試的深入研究，既缺乏其測(cè)試的理論基礎(chǔ)，更沒(méi)有系統(tǒng)化地析取邏輯程序自動(dòng)化測(cè)試工具。

本文通過(guò)初步構(gòu)建析取回答集程序的測(cè)試?yán)碚?，模擬結(jié)構(gòu)化測(cè)試方法中的語(yǔ)句覆蓋、分支覆蓋等覆蓋形式，并給出相應(yīng)的覆蓋率計(jì)算方法，為進(jìn)一步實(shí)現(xiàn)析取回答集程序自動(dòng)化測(cè)試提供理論支持。

本文的主要工作包括3 個(gè)方面：

1）將回答集程序結(jié)構(gòu)化測(cè)試的理論擴(kuò)展到析取回答集程序，進(jìn)一步擴(kuò)大原有的測(cè)試?yán)碚摵凸降膽?yīng)用范圍；由析取回答集程序的規(guī)則可知，正規(guī)回答集程序的規(guī)則頭滿足只有一個(gè)原子的情形，也就是說(shuō)正規(guī)回答集程序是析取回答集程序的特例。本文提出的析取回答集測(cè)試?yán)碚撌钦?guī)回答集程序測(cè)試?yán)碚摰姆夯幢疚牡臏y(cè)試?yán)碚摬粌H可以運(yùn)用于析取回答集程序，也可運(yùn)用于正規(guī)回答集程序，反之則不行。

2）對(duì)析取回答集程序的部分特殊性質(zhì)和定理進(jìn)行了提取、分析和證明。

3）提出了回答集程序的解釋I的重要指標(biāo)，通過(guò)該指標(biāo)可以衡量不同解釋I對(duì)回答集程序的規(guī)則滿足性，從而判斷解釋I的有效性。

1 預(yù)備知識(shí)

下面主要介紹析取回答集程序的基礎(chǔ)知識(shí)和定義，并給出析取回答集程序的實(shí)例和穩(wěn)定模型的具體計(jì)算方法。

1.1 析取回答集程序

假設(shè)命題語(yǔ)言L建立在原子集合A之上。一個(gè)析取回答集程序P由一系列規(guī)則（rule）組成，這些規(guī)則的形式是：

其中：ai(1 ≤i≤k)，bj(1 ≤j≤m)，ct(1 ≤t≤n) 都是原子公式。對(duì)于回答集程序P中的任一規(guī)則，有：

1）a1∨a2∨… ∨ak表示該規(guī)則的頭；

2）b1，b2，…，bm，notc1，notc2，…，notcn表示該規(guī)則的體。

特別地，當(dāng)k=1 時(shí)，析取邏輯規(guī)則轉(zhuǎn)為正規(guī)邏輯規(guī)則，即a1←b1，b2，…，bm，notc1，notc2，…，notcn?；卮鸺绦蛑械姆穸ㄐ问綖槿笔》穸?，即對(duì)于一個(gè)原子集合S，notS={notp|p∈S}，給定式（1）中的規(guī)則r，有如下定義：

通常規(guī)則r的表達(dá)式簡(jiǎn)寫為：hd(r) ←bd(r)。析取回答集程序示例如下。

例1 圖的著色問(wèn)題。給定一個(gè)圖G，有三種顏色可以用于對(duì)圖著色，要求相鄰兩個(gè)端點(diǎn)的顏色不同而且每個(gè)節(jié)點(diǎn)只有一種顏色。用node（X）表示頂點(diǎn)，邊edge（X，Y）表示X、Y兩個(gè)頂點(diǎn)之間有邊，顏色用col（C）表示，三種顏色分別是｛red，green，blue｝，某個(gè)點(diǎn)著色用color（X，C）表示，則表示著色的析取邏輯程序?yàn)椋?/p>

規(guī)則r1為析取規(guī)則，表示每一個(gè)節(jié)點(diǎn)可從三種顏色中選取一種顏色著色；規(guī)則r2表示相鄰兩個(gè)節(jié)點(diǎn)的顏色不能為同一個(gè)顏色；規(guī)則r3、r4、r5表示若點(diǎn)著了紅藍(lán)綠其中一種顏色后，就不能再著其他顏色。

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

命題語(yǔ)言L的解釋是一函數(shù)I：A→{0，1}，其中I(p)=1表示給命題p賦值為真，I(p)=0 表示命題p賦值為假。一個(gè)解釋I是來(lái)自集合A的原子的集合。若某個(gè)原子包含在I中，則表示該原子被賦值為真，否則賦值為假。

例2 若I=，P=b←a，則表示b賦值為真，且b為真時(shí)，命題P也為真。

若命題公式φ在解釋I下為真，則稱I?φ。若I滿足命題理論Σ中的所有公式，則稱I滿足Σ；若I滿足命題公式（集）則稱I是該命題公式集的模型。解釋I是邏輯程序P的模型（表示I滿足P），記為I?P，其中符號(hào)滿足(?)定義為：

1）對(duì)于一個(gè)原子p：I?p當(dāng)且僅當(dāng)p∈I；I?notp當(dāng)且僅當(dāng)I?p不成立；

2）對(duì)于一個(gè)集合S：I?S當(dāng)且僅當(dāng)I?s對(duì)于每一個(gè)s∈S，其中S的元素可以是原子p，或其缺省否定notp，或規(guī)則；

3）對(duì)于一條規(guī)則r：I?r當(dāng)且僅當(dāng)I?bd(r) 蘊(yùn)含I?hd(r)。

一個(gè)程序P的模型I是P的極小模型，當(dāng)且僅當(dāng)不存在另外一個(gè)模型I′使得I′ ?I。給定一個(gè)程序P和一個(gè)解釋I，PI={hd(r) ←pos(r)|r∈P，neg(r) ∩I=?}是P關(guān)于I的G-L（Gelfond-Lifschitz）規(guī)約；若解釋I是PI的極小模型，則稱I是程序P的回答集［18］。對(duì)于一個(gè)邏輯程序P和一個(gè)原子a∈A，程序P定義原子a的規(guī)則集合，記為defP(a)={r∈P|a∈hd(r)}，也 稱DefP(a) 中的規(guī)則定義了原子a。DefP(a，I)表示在解釋I下程序P中定義原子a的規(guī)則集合，記為：defP(a，I)={r∈P|a∈I∩hd(r)}。P關(guān)于I的支撐規(guī)則集合定義為：{r∈P|I?bd(r)}，記為SuppR(P，I)。

2 測(cè)試?yán)碚?/h2>

本章詳細(xì)介紹軟件工程中的測(cè)試方法，然后根據(jù)析取回答集程序的特點(diǎn)提出測(cè)試的思想和測(cè)試用例的概念，主要分為兩個(gè)部分：一是闡述析取回答集程序結(jié)構(gòu)化測(cè)試方法的技術(shù)路線；二是定義結(jié)構(gòu)化測(cè)試方法以及測(cè)試用例的概念。

2.1 析取回答集程序結(jié)構(gòu)化測(cè)試技術(shù)路線

軟件測(cè)試是使用人工或自動(dòng)的手段來(lái)運(yùn)行或測(cè)定某個(gè)軟件系統(tǒng)的過(guò)程，其目的在于檢驗(yàn)它是否滿足規(guī)定的需求或弄清預(yù)期結(jié)果與實(shí)際結(jié)果之間的差別［19］。軟件工程領(lǐng)域的測(cè)試包括黑盒測(cè)試和白盒測(cè)試。黑盒測(cè)試是將軟件看成一個(gè)盒子，測(cè)試人員無(wú)須考慮其內(nèi)部邏輯結(jié)構(gòu)，根據(jù)規(guī)格說(shuō)明書設(shè)計(jì)測(cè)試用例。黑盒測(cè)試重點(diǎn)關(guān)注軟件實(shí)現(xiàn)和規(guī)格說(shuō)明書的一致性，根據(jù)輸入/輸出確定的邏輯關(guān)系設(shè)計(jì)測(cè)試數(shù)據(jù)，以檢查其是否正確。白盒測(cè)試又稱結(jié)構(gòu)測(cè)試、透明盒測(cè)試、邏輯驅(qū)動(dòng)測(cè)試或基于代碼的測(cè)試。白盒測(cè)試是一種測(cè)試用例設(shè)計(jì)方法，盒子指的是被測(cè)試的軟件，白盒指的是盒子是可視的，即清楚盒子內(nèi)部的東西以及里面是如何運(yùn)作的。白盒法全面了解程序內(nèi)部邏輯結(jié)構(gòu)，對(duì)所有邏輯路徑進(jìn)行測(cè)試［20］。

要采用白盒測(cè)試，首先就必須要設(shè)計(jì)合理的軟件測(cè)試用例。軟件測(cè)試用例是指對(duì)一項(xiàng)特定的軟件產(chǎn)品進(jìn)行測(cè)試任務(wù)的描述，體現(xiàn)測(cè)試方案、方法、技術(shù)和策略。測(cè)試用例是為某個(gè)特殊目標(biāo)而編制的一組測(cè)試輸入、執(zhí)行條件以及預(yù)期結(jié)果，用于核實(shí)是否滿足某個(gè)特定軟件需求［21］。因此，對(duì)析取邏輯程序測(cè)試的思路是：首先對(duì)析取回答集程序定義測(cè)試用例（Test Case）的概念，通過(guò)構(gòu)造析取回答集程序測(cè)試用例的輸入、輸出；然后利用軟件測(cè)試的各項(xiàng)覆蓋標(biāo)準(zhǔn)來(lái)實(shí)現(xiàn)析取回答集程序的測(cè)試覆蓋，在此過(guò)程中設(shè)計(jì)和提出析取回答集程序的測(cè)試相關(guān)概念。

此外，還考慮到析取回答集程序語(yǔ)法的兩個(gè)特點(diǎn)。

第一個(gè)特點(diǎn)是：規(guī)則（rule）是程序最重要的語(yǔ)法結(jié)構(gòu)之一，測(cè)試?yán)碚摰闹饕獙?duì)象為析取回答集程序的規(guī)則。對(duì)于析取回答集程序的規(guī)則測(cè)試，又可以細(xì)分出對(duì)規(guī)則體、規(guī)則頭、規(guī)則集合等測(cè)試對(duì)象。

第二個(gè)特點(diǎn)是：析取回答集程序不是順序執(zhí)行的特點(diǎn)，無(wú)法對(duì)析取回答集程序的某個(gè)斷點(diǎn)進(jìn)行測(cè)試。根據(jù)一個(gè)測(cè)試輸入的解釋I運(yùn)算出來(lái)的回答集與標(biāo)準(zhǔn)回答集進(jìn)行比對(duì)，以此來(lái)驗(yàn)證程序是否符合預(yù)期。

綜上，結(jié)構(gòu)化測(cè)試方法使得測(cè)試人員更加清楚地了解軟件的內(nèi)部結(jié)構(gòu)和運(yùn)行機(jī)制，從而更好地設(shè)計(jì)測(cè)試用例，為后續(xù)的測(cè)試實(shí)驗(yàn)設(shè)計(jì)提供方便，而且結(jié)構(gòu)化測(cè)試方法通過(guò)統(tǒng)計(jì)代碼覆蓋率、路徑覆蓋率等技術(shù)指標(biāo)對(duì)代碼的測(cè)試更加明確。

2.2 析取回答集程序的測(cè)試用例

首先給出析取回答集程序的測(cè)試用例的定義。設(shè)P是一個(gè)析取回答集程序，IP、OP分別是程序P的輸入原子集合字母表和輸出原子集合字母表，假設(shè)I?IP，P[I]是邏輯程序P在解釋I下的回答集，表示為定義一個(gè)P的規(guī)約滿足映射關(guān)系σP，即程序P從集合IP到集合OP上的映射關(guān)系是σP，定義為σP：IP→。則給定一個(gè)輸入I后，P的正確輸出為σP(I)。由此對(duì)測(cè)試用例的定義如下。

定義1測(cè)試用例。P是一個(gè)任意的析取回答集程序，σP是P的一個(gè)規(guī)約，P和σP定義的測(cè)試用例為一對(duì)序偶T=I，O，其中I?IP，O=σP(I)。程序P通過(guò)測(cè)試用例的條件為P[I]=O。

例3 設(shè)析取回答集程序P有如下3 條規(guī)則：

通過(guò)程序P及其映射σP，很容易驗(yàn)證程序P在每一個(gè)測(cè)試用例T=I，O下測(cè)試均通過(guò)。一個(gè)析取回答集程序P和σP的測(cè)試套件S是P和σP的測(cè)試用例的集合。程序P測(cè)試通過(guò)測(cè)試套件S的條件是P測(cè)試通過(guò)S中的每一個(gè)測(cè)試用例。程序P關(guān)于σP正確的條件是：當(dāng)且僅當(dāng)P測(cè)試通過(guò)P和σP的每一個(gè)測(cè)試用例。

3 覆蓋函數(shù)以及覆蓋率

通過(guò)實(shí)例分析，確定相關(guān)的測(cè)試覆蓋指標(biāo)，以此衡量測(cè)試用例的覆蓋情況。

3.1 結(jié)構(gòu)化測(cè)試的覆蓋形式

結(jié)構(gòu)化測(cè)試在測(cè)試執(zhí)行時(shí)需要每一行代碼至少執(zhí)行一次（語(yǔ)句覆蓋）、遍歷所有的程序分支（分支覆蓋）或者其他的可能的分支，其覆蓋標(biāo)準(zhǔn)有邏輯覆蓋、循環(huán)覆蓋和基本路徑測(cè)試。根據(jù)析取回答集程序的語(yǔ)法規(guī)則和測(cè)試對(duì)象的差異性，給出相應(yīng)的覆蓋函數(shù)定義以及各覆蓋條件下的函數(shù)，并給出具體的計(jì)算方法。

3.2 覆蓋函數(shù)

定義2覆蓋函數(shù)。邏輯程序P和測(cè)試輸入集合的覆蓋函數(shù)γ定義為γ：I×P→[0，1]，對(duì)于每個(gè)程序P和每個(gè)關(guān)于P的輸入集合I ?，以下性質(zhì)成立：

1）γ(I，P)=1，當(dāng)且僅當(dāng)I=；

2）γ(I′，P) ≤γ(I，P)，當(dāng)且僅當(dāng)P的每一個(gè)輸入集合I′?I。

在這里說(shuō)I 是解釋的集合，當(dāng)γ(I，P)=1 時(shí)，滿足的條件為I=，可以生成所有邏輯程序P的覆蓋。其次，析取回答集程序的覆蓋函數(shù)的形式雖然與正規(guī)回答集程序相似，但是二者的含義卻有不同，析取回答集程序產(chǎn)生的輸入、輸出集合的涵蓋范圍比正規(guī)回答集程序的范圍大。

在軟件工程中，如果一個(gè)測(cè)試用例使得被測(cè)試的文件（類或者函數(shù)）中所有的語(yǔ)句（判定）至少被執(zhí)行到一次，那么這種測(cè)試覆蓋準(zhǔn)則被稱為語(yǔ)句（判定）覆蓋。軟件工程中測(cè)試覆蓋率的計(jì)算方法［20］如下：

考慮到析取回答集程序中沒(méi)有語(yǔ)句、分支的概念，因此假設(shè)在輸入I ?的情況下，其規(guī)則、定義、環(huán)以及子程序的覆蓋數(shù)量與全部輸入案例產(chǎn)生的規(guī)則、定義、環(huán)以及子程序的覆蓋數(shù)量比值作為覆蓋率。析取回答集程序的覆蓋率公式定義為：

根據(jù)以上的覆蓋率計(jì)算公式，可以計(jì)算出析取回答集程序的結(jié)構(gòu)化測(cè)試方法中各覆蓋形式下的覆蓋率。

3.3 析取回答集程序的測(cè)試覆蓋率

由于在析取回答集程序測(cè)試中，代碼被邏輯規(guī)則替代，在回答集程序中，每行規(guī)則都會(huì)執(zhí)行，因此需要測(cè)試回答集程序中的每一條規(guī)則。而測(cè)試覆蓋率是測(cè)試在給定的解釋I下，規(guī)則r是否滿足，并且規(guī)則又可分為規(guī)則的頭、規(guī)則的體、規(guī)則集合等不同的測(cè)試對(duì)象，根據(jù)測(cè)試對(duì)象的滿足情況，得到析取回答集程序的以下各種覆蓋。

在面向過(guò)程的程序測(cè)試方法中，路徑覆蓋法主要是通過(guò)測(cè)試用例的執(zhí)行，覆蓋程序中所有可能的路徑。由于在析取回答集程序中，規(guī)則與規(guī)則不會(huì)產(chǎn)生分支執(zhí)行，因此使用部分規(guī)則組成的集合作為一個(gè)子程序，通過(guò)對(duì)子程序的覆蓋來(lái)模擬路徑覆蓋的概念。

定義3子程序覆蓋。設(shè)P是一個(gè)析取回答集程序，I?IP且P′?P。當(dāng)P′=SuppR(P，X) 對(duì)某回答集X∈AS(P∪I)成立時(shí)，I覆蓋P′。

例4 設(shè)析取回答集程序P有例3 中的3 條規(guī)則：

其中IP=OP={a，b}，I={a，b}，有X∈AS(P∪I)={{a，b}}，P′={r1，r2，r3}，可知P′=SuppR(P，X)，I覆蓋P′。按照計(jì)算覆蓋率的方法，很容易知道對(duì)于任意的I?IP都有AS(P∪I)={{a，b}}，即對(duì)于任意的I?IP都覆蓋了同一個(gè)SuppR(P，X)，根據(jù)上面的計(jì)算式有：

在結(jié)構(gòu)化測(cè)試方法中，由于面向過(guò)程的編程語(yǔ)言并非每行代碼都會(huì)執(zhí)行，只能通過(guò)執(zhí)行過(guò)的代碼塊占總代碼的比率，判斷測(cè)試用例的好壞。語(yǔ)句覆蓋是結(jié)構(gòu)化測(cè)試方法中的一個(gè)重要指標(biāo)，要求測(cè)試過(guò)程中，測(cè)試用例盡可能地測(cè)試到每一條代碼，以此衡量測(cè)試用例是否真正完全覆蓋了應(yīng)用程序代碼中的各種可能以及在運(yùn)行這些測(cè)試用例時(shí)執(zhí)行了多少代碼，所以通過(guò)測(cè)試規(guī)則體的是否滿足來(lái)模擬語(yǔ)句覆蓋。

定義4規(guī)則覆蓋。給定一個(gè)析取回答集程序P，r∈P，I?IP。如果對(duì)某個(gè)回答集X∈AS(P∪I)時(shí)，有X?bd(r)成立，則規(guī)則r∈P被I正覆蓋。如果對(duì)回答集X∈AS(P∪I)，有X?bd(r)，則r被I負(fù)覆蓋。此外，r被測(cè)試用例T正覆蓋，當(dāng)且僅當(dāng)r被I正覆蓋。

例5 設(shè)析取回答集程序P為例3 中的程序，其中IP=OP={a，b}，I1={a，b}和I2={a}，則有AS(P∪I1)={{a，b}}，可知I1覆蓋了規(guī)則r1，r2，r3；對(duì)于AS(P∪I2)={{a，b}}，可知I2覆蓋規(guī)則r1，r2，r3。

在關(guān)注規(guī)則的滿足性時(shí)主要用到的是規(guī)則覆蓋，但是在計(jì)算不同規(guī)則頭之間是否遞歸滿足時(shí)，需要用到環(huán)覆蓋的概念。

定義5環(huán)覆蓋。設(shè)P是一個(gè)析取回答集程序，I?IP。LP是P的一個(gè)環(huán)當(dāng)且僅當(dāng)有某個(gè)回答集X∈AS(P∪I)，使得原子a由r∈SuppR(P，X)所定義，且對(duì)于定義的每個(gè)原子a都 有a∈LP，則P的 環(huán)LP被I正覆蓋。若有一個(gè)規(guī)則r∈SuppR(P，X) 定義了a，但是對(duì)于某個(gè)回答集X∈AS(P∪I)，defP(a，X) ≠?，若沒(méi)有 規(guī)則SuppR(P，X)定義a，則LP被I負(fù)覆蓋。

例6 以例3 中的程序?yàn)槔?，其中IP=OP={a，b}，該程序的回答集是AS(P∪I)={{a，b}}，該回答集對(duì)應(yīng)的環(huán)除單環(huán){a}，外，還有環(huán)LP={a，b}。同理，在計(jì)算環(huán)覆蓋時(shí)用如下方法：

參照例3 的程序，知道對(duì)于任意的I?IP都有AS(P∪I)={{a，b}}，設(shè)I={a，b}?IP，程 序P存在環(huán)LP=，根據(jù)上面的計(jì)算式計(jì)算環(huán)覆蓋率，有：

與面向過(guò)程的編程語(yǔ)言不同，析取回答集程序的規(guī)則中包含了規(guī)則的頭，為了測(cè)試每條規(guī)則的頭是否滿足，給出定義覆蓋的概念。

定義6定義覆蓋。設(shè)P是一個(gè)析取回答集程序，a∈A，I?IP。若對(duì)于某個(gè)回答集X∈AS(P∪I)，存在規(guī)則滿 足r∈SuppR(P，X) 定義了原子a，記 為defP(a，X)={r∈P|a∈X∩hd(r)}，稱原子a被I正覆蓋。若defP(a，X) ≠?且不存在規(guī)則r∈SuppR(P，X)定義的a，則稱a被I負(fù)覆蓋。

例7 以例3 中程序P為例，其中IP=OP={a，b}，該程序的回答集是AS(P∪I)={{a，b}}，該回答集對(duì)應(yīng)的規(guī)則正覆蓋了原子a，原子b。同理，對(duì)于任意的I?IP，可得其規(guī)則正覆蓋函數(shù)coveredD+(I，P)=2，負(fù)覆蓋函數(shù)coveredD-(I，P)=0，而coveredD({I}，P)=2，因此有：

環(huán)覆蓋和定義覆蓋有一定的相似性，原因是在于兩者都是為了測(cè)試規(guī)則頭的滿足性，但是兩者測(cè)試的規(guī)則頭又有不同的特點(diǎn)。定義覆蓋是針對(duì)單個(gè)的規(guī)則頭，即單個(gè)的原子滿足性。而環(huán)覆蓋則是為了測(cè)試規(guī)則頭的集合，在這個(gè)規(guī)則頭集合中，原子之間存在著一定的遞歸滿足關(guān)系。

由以上的各覆蓋測(cè)試條件，設(shè)covered*+(I，P)表示規(guī)則（定義、環(huán)、子程序）的正覆蓋，covered*-(I，P)表示規(guī)則（定義、環(huán)、子程序）的負(fù)覆蓋，總結(jié)得到覆蓋公式為：covered*(I，P)=covered*+(I，P)+covered*-(I，P)，其中* ∈{R，D，L，P}。

性質(zhì)1covered*(?，P)=0 對(duì)任意的邏輯程序P成立，其中* ∈{R，D，L，P}。

推論2P是析取回答集程序，若P∪I對(duì)任意I?IP都有唯一的回答集，則有SuppR(P，X)=P對(duì)于任意的和X∈{P，R}成立。

證明 采用反證法證明。假設(shè)SuppR(P，X) ≠P且P∪I有唯一的回答集，對(duì)于任意的I?IP成立。假設(shè)存在某條規(guī)則r∈P，并且使得對(duì)于回答集X∈AS(P∪I) 有r?SuppR(P，X)。由于AS(P∪I)有唯一的回答集，則根據(jù)推 論1 可 知CR(I，P)=1。若此時(shí)r?SuppR(P，X)，則 有coveredX(，P) ＞coveredX(I，P)，且CR(I，P) ≠1。這與假設(shè)矛盾。證畢。

定義7支撐規(guī)則比值函數(shù)。函數(shù)α是指對(duì)于某個(gè)析取回答集程序P和它的解釋I?IP，其支撐規(guī)則集合的勢(shì)與程序規(guī)則組成的集合的勢(shì)之比。其中，支撐規(guī)則集合的勢(shì)作為分子，析取回答集程序P的規(guī)則組成的集合的勢(shì)作為分母。記為：

α是一個(gè)重要的指標(biāo)，主要用于衡量和計(jì)算一個(gè)析取回答集程序中，其解釋I對(duì)于某個(gè)回答集X∈AS(P∪I)中支撐規(guī)則與程序規(guī)則的勢(shì)之比，由此可以評(píng)估出邏輯程序P在解釋I的非支撐規(guī)則的冗余數(shù)量，此外還可以評(píng)估解釋I的有效性。

例8 設(shè)邏輯程序P有如下規(guī)則：

I={a，b}，對(duì)該程序求解回答集得到回答集：AS(P∪I)={{d，b，a，e}}，其支撐集合的勢(shì)為‖SuppR(P，X)‖=4，‖P‖=5，α=80%。

推論3P是一個(gè)析取回答集程序，若P∪I對(duì)任意I都有唯一的回答集，則對(duì)于任何非空的I?，則有α=100%。

證明由推論 2 可知，SuppR(P，X)=P，則有‖SuppR(P，X)‖=‖P‖。根據(jù)支撐規(guī)則函數(shù)的計(jì)算式有：

4 結(jié)語(yǔ)

本文推廣了命題正規(guī)邏輯程序結(jié)構(gòu)化測(cè)試基本思想到命題析取邏輯程序，提出了命題析取邏輯程序規(guī)則覆蓋、子程序覆蓋、定義覆蓋、環(huán)覆蓋等基本的結(jié)構(gòu)化測(cè)試評(píng)價(jià)準(zhǔn)則，并探討了它們的一些基本性質(zhì)。接下來(lái)將進(jìn)一步推廣這些基本概念到帶變?cè)?、帶聚合函?shù)（sum、min、max 等），以及抽象約束原子的一般邏輯程序，并進(jìn)一步實(shí)現(xiàn)一般回答集程序的自動(dòng)結(jié)構(gòu)化測(cè)試。