Abstract diagnosis

June 13, 2017 | Autor: Marco Comini | Categoria: Abstract Interpretation, Logic Programming, Bottom Up, Top Down
Share Embed


Descrição do Produto

iHE.K~,JRNLA L ~

LOC~" P~OGRAMMING ELSEVIER

The Journal of Logic Programming 39 (1999) 43-93

Abstract diagnosis M a r c o C o m i n i a.*, G i o r g i o Levi ~, Maria Chiara M e o b Giuliana Vitiello c ,t Dipartimc~to di ln hJrmath'a. Unirt, rsitt'~ di Pisa. Corso Italia 40. 1-56125 Pisa. Italy h Diparthnento di l~latematica Ptu'a ed :lpplicata. UnicersitFt eli L'rlquiht. via I"t,toh~. iot'alitgt (.'~Jp,~ito. 6701t~ L'Aquila. l t a i r ¢ Diparthnento tfi b!/brt;utth'a ed ,-tpplica:ionL Unirer.vith tfi Salt,rno. Baroni.v.xi (Salerno). italy

Received 10 February 1997; received in revised form 1 September 1998: accepted 10 September 1998

Abstract

W e s h o w h o w d e c l a r a t i v e d i a g n o s i s t e c h n i q u e s c a n be e x t e n d e d to c o p e w i t h v e r i f i c a t i o n o f o p e r a t i o n a l p r o p e r t i e s , s u c h as c o m p u t e d a n d c o r r e c t a n s w e r s , a n d o f a b s t r a c t p r o p e r t i e s , s u c h as d e p t h ( k ) a n s w e r s a n d g r o u n d n e s s d e p e n d e n c i e s . T h e e x t e n s i o n is a c h i e v e d by usir, g a s i m p l e s e m a n t i c f r a m e w o r k , b a s e d ¢~n a b s t r a c t i n t e r p r e t a t i o n . T h e r e s u l t i n g t e c h n i q u e ( a b s t r a c t d i a g n o s i s ) l e a d s to e l e g a n t b o t t o m - u p a n d top-dowr~ v e r i f i c a t i o n m e t h o d s , w h i c h d o n o t r e q u i r e t o d e t e r m i n e t h e s y m p t o m s in a d v a n c e , a n d w h i c h a r e effective in t h e c a s e o f a b s t r a c t p r o p e r t i e s d e s c r i b e d by finite d o m a i n s . © 1999 E l s e v i e r S c i e n c e Inc. All r i s h t s r e s e r v e d . Keyword.w Logic programm2ug; Declarative diagnosis: Verification: Semantics: Debugging

1. Introduction 1.1. D e c l a r a t i v e

debugging,

p:-ogram

verification

and abst:'t~ct diagnosis

Declaratire debugging [43,35,28] is a t e c h n i q u e w h i c h , g i v e n a p r o g r a m P a n d a s p e c i f i c a t i o n . f o f t h e intended d e c l a r a t i v e s e m a n t i c s o f P, a l l o w s o n e t o d e t e r m i n e p r o g r a m bugs, when the actual semantics .yT[[p] and the ~pecification .J are different. Declarative d e b u g g i n g a l g o r i t h m s are based on a thet3ry which requires f to be specified extensionaily, H o w e v e r , since - f is in general infinite, practical d e b u g g i n g algorithms are driven by s y m p t o m s ( a t o m s on which .yT[[p~ and .9 d o not agree}, which are determined by using testing techniques. C~racles are used to m o d e l the acquisition (from the user) o f the subset o f J which is relevant to a s y m p t o m , Given a s y m p t o m , the algorithms query the oracles to locate the actual sources o f errors.

"Corresponding author. Tel.: +39 050 887248: fax: +39 050 887226: e-mail: comini~i,t~di.unipi.it. 0743-1066/99/S - see front matter © 1999 Elsevier Science Inc. All rights reserved. Pll: S 0 7 4 3 - 1 0 6 6 ( 9 8 ) I 013 ~ ; 3 - X

44

M. Combli et al. I J. Logic Programming 39 (1999) 43-93

O n e stronger alternative to s y m p t o m - d i r e c t e d declarative d e b u g g i n g can be obtained by extending the underlying t h e o ~ to the case where the specification J¢ is a finite represe,ltation o f the intended behavior. This is essentially the a p p r o a c h o f p r o g r a m verification [24,6,3,2], where the specification is a finite (intensional) representation o f a p r o g r a m p r o p e r t y . T h e p r o p e r t y is a n y a b s t r a c t i o n o f the semantics, including the semantics itself. T h e goal o f p r o g r a m verification is to p r o v e t h a t the p r o g r a m is partially correct, i.e., that it satisfies the specification. It is w o r t h noting Hint in p r o g r a m verification a specification is usually a pair o f pre- a n d post-conditions. T h e p r o p e r t y specified by the post-condition has to be satisfied only by those goals which satisfy tile pre-condition. In a d d i t i o n the partial correctness criteria m i g h t require all the p r o c e d u r e calls (call patterns) to satisfy their pre-conditions. T h e aim o f ab.s,'ract diagnosis is to extend declarative d e b u g g i n g to the case where SlC,eci~cations are finite a n d define a p r o g r a m p r o p e r t y rather t h a n its semantics. In o r d e r to be consistent with traditional declarative debugging, specifications are ass u m e d to consist o f p o s t - c o n d i t i o n s only. H o w e v e r the results can be generalized to the case o f pre- a n d post-conditions (see Section 9). Finite specifications lead to the systematic derivation o f the diagnosis a l g o r i t h m s from the u n d e r l y i n g t h e o r y with no need for s y m p t o m detection. M o r e o v e r , the theoretical results on partial correctness, completeness and bug derivation are valid for the diagnosis algorithms too. T h e a p p r o a c h o f abstract diagnosis is strongly related to the idea o f using assertions as finite specifications o f an a p p r o x i m a t i o n o f the intended declarative semantics in Ref. [25] and to the c o n c e p t o f an abstract oracle, introduced in Ref. [34] to specify a superset o f the intended p r o g r a m behavior, in the case o f c o n c u r r e n t logic p r o g r a m s . L2. P r o g r a m p r o p e r t i e s a n d abstract interpretation

P r o g r a m properties are l b r m u l a s in a logical theory. T h e y can be viewed as abstractions o f a suitable semantics. Their" relation to the semantics can be formalized within abstract i n t e r p r e t a t i o n t h e o r y [22,23]. However, abstract i n t e r p r e t a t i o n suggests a n o t h e r w a y o f looking at p r o g r a m properties, where the logical t h e o r y is replaced by a finite (or noetherian) model (the abstract d o m a i n ) . T h e relevant feature o f abstract i n t e r p r e t a t i o n is that, once the p r o p e r t y has been modeled by an a b s t r a c t d o m a i n , we have a m e t h o d o l o g y to systematically derive an abstract semantics, which in t u r n allows us to effectively c o m p u t e a (correct) a p p r o x i m a t i o n o f the p r o p e r t y . By using this a p p r o a c h , most o f the t h e o r e m - p r o v i n g , in the logical t h e o r y involved in p r o g r a m verification, boils d o w n to c o m p u t i n g on the abstract d o m a i n . This is o b t a i n e d in general at the expense o f precision. In p r o g r a m analysis, abstract interpretation t h e o r y is often used to establish the correctness o f specific analysis a l g o r i t h m s a n d abstract d o m a i n s . We are m o r e concerned instead in its application to the systematic derivation o f the (optimal) abstract semantics from the a b s t r a c t d o m a i n . Recent results on d o m a i n refinement o p e r a t o r s (see, for example, Refs. [30,42]) show that (optimal) a b s t r a c t d o m a i n s can systematically be derived from the p r o p e r t y to be proved. 1.3. The s e m a n t i c f r a m e w o r k

P r o g r a m properties we are interested in are o p e r a t i o n a l properties and nol necessarily declarative properties. T h e aim of the resulting m e t h o d is therefore closer to

3el. Comini el al. I J. Logic Programming 39 (1999) 43-93

45

the goal o f r a t i o n a l d e b u g g i n g [40] t h a n to the goal o f d e c l a r a t i v e debugging. T h i s also m e a n s t h a t we c a n n o t base the a b s t r a c t i o n f r a m e w o r k on the declarative s e m a n tics, since it is t o o a b s t r a c t to allow us to r e a s o n a b o u t s o m e o p e r a t i o n a l properties, such as g r o u n d n e s s o f variables. S o m e p r e l i m i n a r y versions o f a b s t r a c t diagnosis [17,19] were based on a m o r e c o n c r e t e s e m a n t i c f r a m e w o r k [I 3-15], w h o s e collecting s e m a n t i c s is a trace s e m a n tics [20]. In this p a p e r we are o n l y c o n c e r n e d with p r o p e r t i e s which a r e a b s t r a c tions o f the c o m p u t e d a n s w e r s semantics. W e will t h e r e f o r e i n t r o d u c e in Section 3 a simplified version o f the s e m a n t i c f r a m e w o r k , w h e r e the collecting sem a n t i c s is the s-semantics [27,7], given for a C L P - l i k e version o f positive logic p r o grams. P r o g r a m p r o p e r t i e s are o b s e r v a b l e s , i.e., G a l o i s insertions between the c o n c r e t e d o m a i n (the s e m a n t i c d o m a i n o f the collecting semantics) a n d the abstrac~ d o m a i n c h o s e n to m o d e l the p r o p e r t y . T h e a b s t r a c t s e m a n t i c s ( a b s t r a c t t r a n s i t i o n s y s t e m a n d a b s t r a c t d e n o t a t i o n a l semantics) are s y s t e m a t i c a l l y derived f r o m the collecting ser.~anfics a n d the observable. W e c o n s i d e r t w o classes o f observables, c o m p l e t e a n d a p p r o x i m a t e . F o r every c o m p l e t e o r a p p r o x i m a t e observable, the a b s t r a c t o p e r a t i o n a l s e m a n t i c s a n d the a b s t r a c t d e n o t a t i o n a l s e m a n t i c s are equivalent. This will allow us to define e q u i v a l e n t t o p - d o w n a n d b o t t o m - u p diagnosis a l g o r i t h m s . T h e a b o v e e q u i v a l e n c e p r o p e r t y requires the o b s e r v a b l e to be c o n d e n s i n g . C o n d e n s i n g is a c o m p o s i t i o n a l i t y p r o p e r t y which tells us that the a b s t r a c t s e m a n t i c s r~f a proced u r e call c a n be derived ( w i t h o u t losing precision) f r o m the a b s t r a c t semantics o f the p r o c e d u r e d e c l a r a t i o n . This p r o p e r t y is needed in a b s t r a c t diagnosis where the specification is a p o s t - c o n d i t i o n describing a ( g o a l - i n d e p e n d e n t ) p r o p e r t y o f a set o f p r o c e d u r e d e c l a r a t i o n s . It is w o r t h n o t i n g that the o b s e r v a b l e s c o r r e s p o n d i n g to the d e c l a r a t i v e s e m a n t i c s are co,~densing a n d t h a t the d e c l a r a t i v e s e m a n t i c s d o ,ndeed c h a r a c t e r i z e p r o c e d u r e d e c l a r a t i o n s . N o t e also t h a t several o b s e r v a b l e s used in p r o g r a m analysis (for m o d e , t y p e a n d g r o u n d n e s s analysis) are also c o n d e n s i n g a n d t h a t a n o n - c o n d e n s i n g o b s e r v a b l e can s y s t e m a t i c a l l y be t r a n s f o r m e d into a ( m o r e concrete) c o n d e n s i n g observable, by using d o m a i n refinement o p e r a t o r s (see, for e x a m pie, h o w the c o n d e n s i n g d o m a i n .~tr, ~/, for g r o u n d n e s s analysis can be derived [42] f r o m the n o n - c o n d e n s i n g d o m a i n ~ , ~ - ) . T h e results o f the diagnosis for a p p r o x i m a t e o b s e r v a b l e s are also valid for n o n - c o n d e n s i n g d o m a i n s , which a r e s o m e t i m e s c o n v e n i e n t to use in practice for efficiency reasons. As expected f r o m a b s t r a c t i n t e r p r e t a t i o n t h e o r y , the difference between c o m p l e t e a n d a p p r o x i m a t e o b s e r v a b l e s is related to precision. N a m e l y , the a b s t r a c t s e m a n t i c s coincides with the a b s t r a c t i o n o f the collecting semantics, in the case o f c o m p l e t e o b servables, while it is j u s t a correct a p p r o x i m a t i o n , in the case o f a p p r o x i m a t e observables. O n the o t h e r side, a p p r o x i m a t e o b s e r v a b l e s c o r r e s p o n d to n o e t h e r i a n d o m a i n s . H e n c e their a b s t r a c t semantics is finite, while (in general) it is infinite for c o m p l e t e observables. W e show t h a t the class o f c o m p l e t e o b s e r v a b l e s includes the o b s e r v a b l e s g r o u n d instances o f c o m p u t e d answers a n d correct answers which allow us to r e c o n s t r u c t the declarative semantics used in declarative debugging, i.e., the least H e r b r a n d m o d e l used in Ref. [43] a n d the least term m o d e l ( a t o m i c logical consequences o r c-semantics) used in Ref. [28]. O n the o t h e r h a n d , the class o f a p p r o x i m a t e o b s e r v a b l e s includes d e p t k ( k ) [41] a n d several d o m a i n s p r o p o s e d for type, m o d e a n d g r o u n d n e s s analysis (we will just consider the d o m a i n ~ r ; 9 ~ [38] for g r o u n d n e s s analysis).

46

M. Contini et al. I J. Logk" P r o g r a m m i n g 39 ( 1 9 9 9 ) 43.-93

1.4. A b s t r a c t diagnosis

In Section 4 we give the basic definitions o f abstract diagnosis, which are a s t r a i g h t f o r w a r d a d a p t a t i o n o f those given for declarative debugging. A preliminary version (without proofs) o f abstract diagnosis can be found in [17, ! 9, i 6]. P a r t i a l c o t rectness and cotr~pleteness of P w.r.t, the observable p r o p e r t y ~ are defined by comparing the abstract specification o f the i n t e n d e d b e h a v i o r ( o f P w.r.t. ~) ,¢~ and the a b s t r a c t i o n ~(.~-[[P~) o f the concrete semantics . ~ P ] ] . It is w o r t h noting that ~(.T[[P~) is in general m o r e precise than the abstract __-muntics . ~ [ P ~ , in the case of a p p r o x i m a t e observables. The diagnosis is based on the detection o f incortx, ct clauses and u n c o v e r e d elem e n t s , which have b o t h a b o t t o m - u p definition (in terms o f one application o f the " a b s t r a c t immediate consequence o p e r a t o r " to the a b s t r a c t specification, see Section 4.1) and a t o p - d o w n definition (in terms o f "'oracle s i m a l a t i o n " , see Sect i o n 4 . 2 ) . It is w o r t h noting that both the definitions use the (possibly a p p r o x i m a t e ) c o m p u t a t i o n vn the abstract d o m a i n , a n d that no fixpoint c o m p u t a tion is required, since the abst~ae~ semantics does not need to be c o m p u t e d . A n imp l e m e n t a t i o n o f the diagnosis a l g o r i t h m s ( p a r a m e t r i c w.r.t, the observable) by m e a n s o f P R O L O G m e t a - p r o g r a m s is described in Ref. [12]. In Section 5 we give the diagnosis t h e o r e m s for complete observables, which provide rather strong results. N a m e l y , e absence of incorrect clauses implies partial correctness, • absence o f uncovered elements implies completeness, for a large class o f p r o g r a m s ~,,cceptable p r o g r a m s ) , • incorrect clauses a n d uncovered elements always c o r r e s p o n d to a bug in the progrum. The results generalize to a n y complete observable lhe results given for declarative debugging and allow us to reconstruct the theory o f declarative debugging as an instance o f abstract diagnosis. In addition we have some new stronger results on the diagnosis o f completeness. However, since abstract specifications are often infinite in the case o f complete observables, these results have ~ purely theoretical interest and can be viewed as a f o u n d a t i o n for the effective diagnosis m e t h o d s considered in the following sections. The first effective diagnosis m e t h o d Q~artial diagnosis) is described in Section 6. Partial diagnosis (originally introduced in Rel: [18]) can be applied to m a k e the diagnosis effective in the case o f complete observables. A specification consists o f a finite set o f elements which are in the intended behavior and a finite set o f elements which are not in the intended behavior. The diagnosis is based on the detection o f p-incorrect clauses and p-uncovered elements, which generalize the definitions o f incorrect clause a n d uncovered element to the case o f partial specifications. T h e results we obtain are o f course weaker. N a m e l y , • p - i n c o n e c t clauses always c o r r e s p o n d to bugs in the p r o g r a m , • absence of p-uncovered elements implies completeness (w.r.t. the positive specification) for a large class of programs, • a p-uncovered element is a w a r n i n g a b o u t a possible incompleteness bug. We show that partial diagnosis can be viewed as a theoretical f o u n d a t i o n o f s y m p t o m - d i r e c t e d oracle-based debugging algorithms t~.sed in declarative debugging.

~[. Comini et ai. I J Logic PrtLgramm#~g 39 (1999) ,13-03

47

T h e s e c o n d effective d i a g n o s i s m e t h o d c a n b e a p p l i e d i f the p r o p e r t y c a n b e m o d eled b y a p p r o x i m a t e o b s e r v a b l e s . F o r e x a m p l e , o n e c a n c h o o s e to a p p r o x i m a t e t h e complete observable computed answers by the (approximate) observable depth(k) a n s w e r s , w h i c h lead~ to finite a b s t r a c t s p e c i f i c a t i o n s . U s i n g a b s t r a c t d i a g n o s i s w.r.t, a p p r o x i m a t e o b s e r v a b l e s o n e c a n effectively p r o v e p r o p e r t i e s r e l a t e d to m o d e s , t y p e s a n d g r o u n d n e s s d e p e n d e n c i e s . T h e results for a p p r o x i m a t e o b s e r v a b l e s a r e give n in S e c t i o n 7. A g a i n , the results a r e w e a k e r t h a n t h o s e for c o m p l e t e o b s e r v a b l e s (because of approximation). Namely, • absence of incorrect clauses implies partial correctness, • a n u n c o v e r e d e l e m e n t a h r a y s c o r r e s p o n d s to a b u g in t h e p r o g r a m , • all t h e i n c o r r e c t n e s s b u g s a r e c a p t u r e d b y i n c o r r e c t clauses, • a n i n c o r r e c t c l a u s e is a w a r n i n g a b o u t a p o s s i b l e i n c o r r e c t n e s s bug. It is w o r t h n o t i n g t h a t there exists a d u a l i t y b e t w e e n the r e s u l t s f o r p a r t i a l d i a g n o s i s a n d t h o s e f o r a p p r o x i m a t e o b s e r v a b l e s . T h i s is d u .~ , to the fact t h a t a p a r t i a l specific a t i o n is a s u b s e t o f the full s p e c i f i c a t i o n , w h i l e a n a b s t r a c t s p e c i f i c a t i o n c o r r e s p o n d ing to a n a p p r o x i m a t e o b s e r v a b l e r e p r e s e n t s ( t h r o u g h the c o n c r e t i z a t i o n f u n c t i o n ) a s u p e r s e t o f the c o n c r e t e full s p e c i f i c a t i o n . W e c e m p a r e the results o f a b s t r a c t d i a g n o s i s w.r.t, a p p r o x i m a t e o b s e r v a b l e s to t h o s e o f p r o g r a m v e r i f i c a t i o n ( w i t h p o s t - c o n d i t i o n s only). It t u r n s o u t t h e t the results a r e s i m i l a r for p a r t i a l c o r r e c t n e s s a n d c o m p l e t e n e s s . A b s t r a c t d i a g n o s ~ is m o r e useful for d e b u g g i n g p u r p o s e s , since it p r o v i d e s useful i n f o r m a t i o n o n " . : o g r a m b a g s . i n S e c t i o n 8 we c o n s i d e r the p r o b l e m o f m o d u l a r d i a g n o s i s a n d we f o r m a l l y p r o v e t h a t t h e d i a g n o s i s m e t h o d d o e s n o t n e e d to be e x t e n d e d to p e r f o r m the d i a g n o s i s in a m o d u l a r w a y . T h i s is d u e to tl~,e fact t h a t b o t h the t o p - d o w n a n d the b o t t o m - u p dia g n o s i s a l g o r i t h m s are es,:.enti::lly b a s e d o n t h e a p p l i c a t i o n o f t h e " ' a b s t r a c t i m m e d i ate c o n s e q u e n c e o p e r a t o r " whicla is i n t r i n s i c a l l y c o m p o s i t i o n a l . T h i s p r o p e r t y s h o w s t h a t we c a n v e r i l y a n d d e b u g i n c o m p l e t e p r o g r a m s , o n c e we h a v e the s p e c i f i c a t i o n s for the m i s s i n g p r o g r a m c o m p o n e n t s . F i n a l l y S e c t i o n 9 is d e v o t e d to s o m e c o n c l u s i v e r e m a r k s .

2. Preliminaries In the f o l l o w i n g sections, we a s s u m e L l m i l i a r i t y w i t h the s t a n d a r d n o t i o n s o f logic p r o g r a m m i n g as i n t r o d u c e d in Refs. [1,36]. 2.1. L o g i c p r o g r a m m i n g

T h r o u g h o u t the p a p e r we a s s u m e p r o g r a m s a n d g o a l s b e i n g d e f i n e d o n a first ord e r l a n g u a g e g i v e n b y a s i g n a t u r e Z" c o n s i s t i n g o f a finite set F o f J i m c t i o n s_rmbols, a finite set H o f p r e d i c a t e s y m b o l s a n d a d e n u m e r a b l e set V o f rariable s y m b o l s . T den o t e s the set o f t e r m s b u i l t o n F a n d II. A s u b s t i t u t i o n is a m a p p i n g 0 : V ~ T s u c h t h a t t h e set dora(i)) ::= {x I tg(x) ~ x} ( d o m a i n o f 0) is finite. A s u b s t i t u t i o n t9 is i d e m p o t e n t i f ~h9 ~- ~9. A r e . t a m i n g is a ( n o n i d e m p o t e n t ) subst.ituiion p for w h i c h t h e r e exists the i n v e r s e p-~, s u c h t h a t p p - i __ p - t p ._ id. T h e p r e o r d e r i n g ~< ( m o r e g e n e r a l t h a n ) o n s u b s t i t u t i o n s is s u c h t h a t 0 t 0, w h e r e H (the head) a n d A~ . . . . . ,4, (the body) a r e a t o m s . ~-- a n d , d e n o t e logical i m p l i c a t i o n a n d c o n j u n c t i o n respectively, a n d all v a r i a b l e s a r e u n i v e r s a l l y q u a n t i f i e d . A p r o g r a m is a finite set o f (definite) clauses. In the p a p e r we use s t a n d a r d r e s u h s o n the o r d i n a l p o w e r s T o f c o n t i n u o u s functions o n c o m p l e t e lattices. N a m e l y , given a n y m o n o t o n i c o p e r a t o r T o n (C, ~t 1. If, for a n y i E [l,n], v a r ( D ) f ' ) ( c a r ( D i ) U z ) C ( D l ~ - " . ~ D , , ) ~ D = l D , ~ . . . ~ D , , ) ~ D. 7. T h e n o e t h o r i a n i t y o f D is used to e n s u r e the finiteness o f ~ .

57 x

then

N o t e that, differently f r o m the case o f c o m p l e t e o b s e r v a b l e s , the class o f a p p r o x i m a t e o b s e r v a b l e s is also chara~:terized in t e r m s o f s o m e p r o p e r t i e s o f the a b s t r a c t o p e r a t o r s . A n e q u i v a l e n t c h a r a c t e r i z a t i o n , g iv en in t e r m s o f ~, 7 a n d the c o n c r e t e operators, is pos,~ibl¢ b u t w o u l d be h a r d e r to u n d e r s t a n d .

T h e o r e m 8. Let ~ : [E---, D be an a p p r o x i m a t e observable. P be a p r o g r a m , 6: : = D , , 4 1 , . . . ,,4n be an a b s t r a c t g o a l z : = v a r ( d ! . . . . . An) a n d Yi : l _ var(,4i) (for i E [[, n]). T h e n 2. a=~6: in P~ = ( D ~ ] . , t c ~ p ] ( A l ) ~ ] , , . - • - ~ . C~P~P])iA,,))],,

3. :~=[P] is c o n t i n u o u s on OA ( a n d t h e r e f o r e : ~ , [ P ] = ~#,[P] T ,,,),

T h e o r e m 8 sh o ws that a p p r o x i m a t e o b s e r v a b l e s are c o n d e n s i n g (Point 2) a n d t h a t the a b s t r a c t t o p - d o w n a n d b o t t o m - u p s e m a n t i c s a re e q u i v a l e n t ( P o i n t 6). H o w e v e r , the d e n o t a t i o n s are j u s t correct a p p r o x i m a t i o n s , yet the y are not precise ( P o i n t s 1 a n d 5). N o t e that the a b o v e c h a r a c t e r i z a t i o n o f a p p r o x i m a t e o b s e r v a b l e s g u a r a n t e e s the o p t i m a l i t y o f the a b s t r a c t i m m e d i a t e c o n s e q u e n c e o p e r a t o r (see P o i n t 4). 3. 4.1. T h e .~tf .9 ~ o b s e r v a b l e f o r g r o u n d n e s s d e p e n d e n c i e s o f c o m p u t e d a n s w e r s W e s h o w n o w h ow to m o d e l the d o m a i n :#t;eA/', d e s i g n e d for the g r o u n d n e s s analy s i s o f logic p r o g r a m s [21,38]. ~tr~9" is a d o m a i n o f e q u i v a l e n c e classes o f p r o p o s i t i o n a l f o r m u l a s , built using the logical c o n n e c t i v e s ~-% A a n d v, a n d o r d e r e d by i m p l i c a t i o n . T h e p r o p o s i t i o n a l f o r m u l a s represent g r o u n d n e s s d e p e n d e n c i e s a m o n g variab l e s. T h e d o m a i n .~e~,9° for two v a r i a b l e s is s h o w n in Fig. 2. First o f all we h a v e to define the a b s t r a c t i o n F ( t ) o f a c o n c r e t e t e r m t. I f var(t) = { x l , . . . ,xn} then r ( t ) := xt ^ - . - A x , . T h e i n t u i t i o n is that, in o r d e r for t to be g r o u n d , all its v a r i a b l e s :q . . . . . x, m u s t be g r o u n d . W e c a n e x t e n d F to solved t b r m e q u a t i o n sets to o b t a i n a b s t r a c t f o r m u l a s as follows. F ( E ) : = A,=,~E(x ~ r ( t ) ) , w h e r e r(0) : = tl~ze. A b s t r a c t f o r m u l a s a re p r o p o s i tional f o r m u l a s w h i c h express the g r o u n d n e s s d e p e n d e n c i e s a m o n g the e l i m i n a b l e v a r i a b l e s a n d the o t h e r v a r i a b l e s o f the c o n c r e t e solved f o r m e q u a t i o n set. T h e g r o u n d n e s s d e p e n d e n c i e s observable ~r : IF --, .~#d%~' is

~r(8) := V r(E), EE¢~

w h e r e ~ r ( 0 ) : = f a l s e . By a p p l y i n g the definition, the a b s t r a c t o p e r a t o r s turn out to be

58

M. Com#K et ai. l J. Log&" Programming 39 (1999) 43-93

true

Y--o

X

X---r Y

X

Y

),

false Fig. 2. The domain ,'/'(' .'t' for two variables X. Y.

F,~,F_, = F , A ~ , --

F[., = { F

if c a r ( F ) C {x}.

(Fb' ~ true] v F b ' ~

fidse])i.,

for s o m e y ~ ,,a,'(F) \ {x}.

where FLy , ~ E] is o b t a i n e d by replacing each o c c u r r e n c e o f the v a r i a b l e v in F by E. N o t e that the a b s t r a c t n o t i o n o[ restriction o f an a b s t r a c t f o r m u l a c o r r e s p o n d s to S c h r S d e r ' s edimination principle.

T h e ~ o p e r a t i o n is p e r f o r m e d by first r e n a m i n g the s e c o n d a r g u m e n t a n d then c o m p u t i n g the c o n j u n c t i o n . We omit its formal definition because it is n o t needed to define the semantics, since, in a n y expression we use, it collapses to ~ . ~r is an a p p r o x i m a t e observable. T h e a b s t r a c t i m m e d i a t e c o n s e q u e n c e o p e r a t o r . ~ , ~P~ is

•~,-~[P~("/,, ) = :.P(~).

V p ( x ) ~ F..-I | ...... .t,,

(

~,,.(1 E l ) ,,, A . ¢ , , . ( A , ) i.. l

)

[.,.

r e n a m e d ~.'l:D.use ol" P

N o t e that .¢~, [[P]~ is defined o n l y in t e r m s o f a b s t r a c t restriction i a n d o f the iub a n d g l b o p e r a t o r s on .¢(' if' (A a n d v, respectively).

E x a m p l e 9. C o n s i d e r the p r o g r a m P o f Fig. 3 a n d the g r o u n d n e s s d e p e n d e n c i e s observable. T h e a b s t r a c t d e n o t a t i o n o f P is _

[ p(.v,)') ~--~x V y ,

I

. r(x,y)~xAv.

which t m n ~ out to be precise since .~-,, [[P]] = ~tf(JT~P~]). N o t e that, if we c h o o s e to represent g r o u n d n e s s d e p e n d e n c i e s using the d o m a i n ~ ? , . T , which does not c o n t a i n disjuvctive f o r m u l a s ( a n d whose c o r r e s p o n d i n g o b s e r v a b l e is not a p p r o x i m a t e ) , we

:Vl.

r ( X , ~) p(a,Y). p(X,b). q(X,X).

Comini et aLI J. Logic Programming 39 (1999) 43-93

:- p(X,Y),

59

q(X,Y).

Fig. 3. The program of Examples 9. 44 and 50.

w o u l d o b t a i n a less precise a b s t r a c t s e m a n t i c s , w h e r e the s e m a n t i c s o f p ( x , y ) w o u l d be true a n d t h e s e m a n t i c s o f r(x,y) w o u l d be x ~ ),.

3.4.2. The depth(k) observable W e s h o w n o w h o w to a p p r o x i m a t e a n infinite set o f c o m p u t e d a n s w e r s b y m e a n s o f a depth(k) cut, i.e., b y c u t t i n g t e r m s w h i c h h a v e a d e p t h g r e a t e r t h a n k. T e r m s a r e c u t by r e p l a c i n g e a c h s u b - t e r m r o o t e d a t d e p t h k w i t h a n e w v a r i a b l e t a k e n f r o m a set I? ( d i s j o i n t f r o m V). A depth(k) t e r m r e p r e s e n t s all t h e t e r m s o b t a i n e d by i n s t a n t i a t i n g t h e v a r i a b l e s o f f" w i t h t e r m s built o v e r V. F i r s t o f all w e h a v e to d e f i n e t h e a b s t r a c t i o n t& a s t h e depth(k) r e d u c t i o n o f t h e c o n c r e t e t e r m t. W e c a n e x t e n d kk to s o l v e d f o r m e q u a t i o n sets to o b t a i n a b s t r a c t f o r m u l a s as follows. Ekk : = {x = t& ] x = t E E}. W e a s s u m e t h a t , f o l a n y e q u a t i o n in E, a n y c u t is p e r f o r m e d by u s i n g d i s t i n c t v a r i a b l e s o f It'. W e d e n o t e b y IF,~ t h e set o f s o l v e d f o r m e q u a t i o n sets w i t h depth(k) t e r m s a n d e l i m i n a b l e v a r i a b l e s in V. T h e depth(k) o b s e r v a b l e r~ : E ~ IF~.~. is

,:~(e,)

:=

{E~ I E c e,}.

In t h e f o l l o w i n g we a s s u m e t h a t , f o r a n y e x p r e s s i o n . T ~ ; . T ' , we r e n a m e v a r i a b l e s in V a n d I? w i t h v a r i a b l e s still in F a n d V r e s p e c t i v e l y . F u r t h e r m o r e we c o n s i d e r o n l y s o l v e d f o r m s w i t h e l i m i n a b l e v a r i a b l e s in V. U n d e r these a s s u m p t i o n s , b y a p p l y i n g t h e d e f i n i t i o n , t h e a b s t r a c t o p e r a t o r s t u r n o u t to be JZ"

=

=

r~ is a n a p p r o x i m : ~ e :~',, [[P]] is

observable. The abstract immediate consequence

{-.~

I," = p(-,:)

-

E,..4,

operator

..... ~,,

is a r e n a m e d c , a u s e o f P, z -- rat(c), f o r i E [i, n ] , ) ' i

-~-

t~cll'(.4i),

= (({E'}~,, o,., .J,'~,(A,) o.~._~....~.~..¢,,(.~,,))~,01.,}. E x a m p l e 1O. C o n s i d e r t h e p r o g r a n a / ' o f Fig. 4 a n d the depth(2) o b s e r v a b l e . T h e a b s t r a c t d e n o t a t i o n o f P is = ,.(x) -

=/(..=)}.

lid. CombH et al. I J. Logh" Programming 39 (1999) 43-93

60

r(X). rCf(X))

:- r(X). Fig. 4. T h e p r o g r a m o f E x a m p l e 10.

4. Abstract diagnos~ In the f o l l o w i n g , t h e o b s e r v a b l e ~ will a l w a y s be a s s u m e d to be at least a p p r o x i m a t e , since we k n o w t h a t for t h e s e o b s e r v a b l e s the a c t u a l a n d the i n t e n d e d b e h a v i o r s f o r all the g o a l s o f a p r o g r a m a r e m f i q u e l y d e t e r m i n e d b y the b e h a v i o r s for p u r e a t o m i c goals. T h e f o l l o w i n g D e f i n i t i o n 11 e x t e n d s to a b s t r a c t d i a g n o s i s the defiz~it i o n s g i v e n in Refs. [43,28,35] for d ~ c l a r a t i v e d i a g n o s i s , i n the f o l l o w i n g : ~ is the s p e c i f i c a t i o n o f the i n t e n d e d b e h a v i o r o f a p r o g r a m for p u r e a t o m s w.r.t, the n b s e r v a b l e ~t. D e f i n i t i o n 11. Let P be a p r o g r a m a n d 2 b e a n o b s e r v a b l e . !. P is p a r t i a l l y c o r r e c t w . r . t . . / if ~t(.~P]]) ~< ./~. 2. P is c o m p l e t e w . r . t . . / i f ¢
Lihat lebih banyak...

Comentários

Copyright © 2017 DADOSPDF Inc.