Enumerating Minimally Revised Specifications Using Dualization
Enumerating Minimally Revised Specifications Using Dualization
复制标题
DOI：
10.1007/11780496_21
复制
发表时间：
2006-03
期刊：
影响因子：
--
通讯作者：
K. Satoh;T. Uno
中科院分区：
文献类型：
--
作者：
K. Satoh;T. Uno
We consider the problem of enumerating minimally revised specifications in software engineering in the situation where a new specification is added to the current specification and causes a conflict. We assume that a specification is expressed as a set of ground Horn clauses which is divided into two setsTpstandTtmpthat are the unchangeable and changeable parts of the specification, respectively. Since a minimal revision is obtained by removing a minimal set of clauses fromTtmpso that the remaining set is consistent, our task can be restated as enumerating maximal consistent subsets of a given set of Horn clauses. Moreover, consistency property is monotone, that is, if a set of Horn clauses is consistent then every subset of the set is also consistent. Then, we can apply our previous method of enumerating maximal frequent sets in data mining which can be used for any enumeration for maximal subsets w.r.t. a monotone property. We show that our algorithm performs a dualization only once for an enumeration of maximal subsets, and the number of consistency checks is at most $|{MinI_{T_{pst}}({T_{tmp}})}|+|{MaxC_{T_{pst}}({T_{tmp}})}|\cdot|T_{tmp}|$ and the necessary space iswhereis the number of minimal subsets ofTtmpthat are inconsistent withTpst, andis the number of maximal subsets ofTtmpthat are consistent withTpst.
We consider the problem of enumerating minimally revised specifications in software engineering in the situation where a new specification is added to the current specification and causes a conflict. We assume that a specification is expressed as a set of ground Horn clauses which is divided into two setsTpstandTtmpthat are the unchangeable and changeable parts of the specification, respectively. Since a minimal revision is obtained by removing a minimal set of clauses fromTtmpso that the remaining set is consistent, our task can be restated as enumerating maximal consistent subsets of a given set of Horn clauses. Moreover, consistency property is monotone, that is, if a set of Horn clauses is consistent then every subset of the set is also consistent. Then, we can apply our previous method of enumerating maximal frequent sets in data mining which can be used for any enumeration for maximal subsets w.r.t. a monotone property. We show that our algorithm performs a dualization only once for an enumeration of maximal subsets, and the number of consistency checks is at most $|{MinI_{T_{pst}}({T_{tmp}})}|+|{MaxC_{T_{pst}}({T_{tmp}})}|\cdot|T_{tmp}|$ and the necessary space iswhereis the number of minimal subsets ofTtmpthat are inconsistent withTpst, andis the number of maximal subsets ofTtmpthat are consistent withTpst.