[發明專利]一種基于極小不協調集合的R縮減求解方法

無效

• 申請號: 200910243037.6
• 申請日: 2009-12-22
• 公開（公告）號: CN101719094A
• 公開（公告）日: 2010-06-02
• 發明（設計）人: 羅杰;李未;李賀;劉祥龍;蔣東辰
• 申請（專利權）人: 北京航空航天大學
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 北京科迪生專利代理有限責任公司 11251
• 代理人: 李新華

發明領域

本發明涉及一種在命題邏輯的范疇下，基于不協調語句集合的極小不協調子集的R縮減求解方法。

發明背景

軟件測試是保證軟件開發質量的不可缺少的重要環節，只有經過嚴格測試的軟件才能被使用。為此人們研制了大量測試工具來幫助提高軟件測試的效率，但到目前為止，測試樣例的設計和對軟件錯誤的定位和修改，仍需大量人力投入，而且測試質量仍與測試人員的經驗緊密相關，軟件測試仍被視為一門“工藝”技術。

R演算系統的提出就是為了解決這一問題。R演算系統是在國際上首次提出的對邏輯連接詞符號和量詞符號進行形式化演算的錯誤定位和修正系統。R演算系統使用一階語言作為軟件需求說明的描述語言，它是一個關于一階語言的邏輯連接詞符號和量詞符號的形式演算系統。R演算系統構建的基本思路是：首先給出一個測試樣例結果組成的集合E，作為對現有軟件需求說明S中的語句修正的標準，并且E對S所作的每一次修正都是一次邏輯推理，而且都是必要的，所以這樣的修正對于需求說明S的改動也是極小的，其次由于修正的方式有多種可能，R演算系統應將所有可能的修正都推導出來。

所以提出一個能求解所有R縮減的方法，在計算機上實現R演算，對于軟件的測試和調試具有重要的意義。

發明內容

本發明要解決的技術問題：填補了現有技術的空白，提供一種在命題邏輯的范疇下，基于不協調語句集合的極小不協調子集的R縮減求解方法。

本發明采用的技術方案：一種基于極小不協調集合的R縮減求解方法，其特征在于步驟如下：

(1)獲取輸入的協調原子語句和原子語句的否定的集合，存于Δ中，獲取輸入的被修正語句集合，存于Γ中；

(2)將Γ中的所有公式轉換為否定范式(NNF)，然后再轉換為析取范式(DNF)，存入Γ′中；

(3)求解出Δ∪Γ′的所有極小不協調集合，存于中；

(4)根據求解出Δ∪Γ′的所有極小刪除集合，存于中；

(5)對于中的每一個極小刪除集合Θ′，如果它對應的Γ中的語句集合是Θ并且那么Γ-Θ就是Γ關于Δ的R縮減，并將其加入集合中。

根據本發明的又一個方面，其中步驟(3)又進一步包括：

(a)Δ∪Γ′只包含原子語句和原子語句的否定。枚舉出Δ∪Γ′所有形如{A，～A}的子集{A₁，～A₁}，...，{A_m，～A_m}，則

(b)Δ∪Γ′包含A∧B。記Ξ＝Δ∪Γ′-{A∧B}。遞歸的使用此方法求解Ξ∪{A，B}的所有極小不協調集合，存于中。遍歷中的所有元素，如果并且那么將Λ加入中；如果并且那么將(Λ-{A，B})∪{A∧B}加入中；

(c)Δ∪Γ′包含A∨B。記Ξ＝Δ∪Γ′-{A∨B}。遞歸的使用此方法求解Ξ∪{A}和Ξ∪{B}的所有極小不協調集合，分別存于和中。如果那么將Λ加入集合遍歷和中的所有元素，如果A∈Λ₁并且B∈Λ₂，那么(Λ₁-{A})∪(A₂-{B})∪{A∨B}加入集合遍歷中的所有元素，如果并且不存在使得那么將Λ加入中；

根據本發明的又一個方面，其中步驟(4)又進一步包括：

(a)若集合不是空集，則：

(i)選取集合中的第一個極小不協調子集Λ；

(ii)對于Λ中的任何一個語句A，

對遞歸的使用這一方法求出它的所有極小刪除集合

(iii)記對任意{A}∪Φ，如果不存在一個使得那么

(b)若集合是空集，則

附圖說明

圖1為本發明的方法基本流程圖。

具體實施方式

下面參考附圖，對本發明的實施例進行詳細的說明。

首先對本發明的方法原理進行說明。

研究表明，語句集合Γ關于Δ的R縮減與Δ∪Γ的極小不協調子集之間存在聯系，若是能夠將Δ∪Γ的極小不協調子集全部枚舉出來，那么語句集合Γ關于Δ的所有R縮減就能夠計算出來。而在命題邏輯的范疇內，語句集合Δ∪Γ的極小不協調子集是可以全部枚舉得到的。這就為計算R縮減提供了一種計算的方法。

具體而言，本發明所提出的方法基本流程如圖1所示。

本發明主要包括的核心思想：通過枚舉Δ∪Γ的所有極小不協調子集，一次求出語句集合Γ關于Δ的所有R縮減。

在描述方法前先定義如下變量及方法：

1.設Δ是一個由原子語句或原子語句的否定組成的集合；