Operator Component Matrix Model for IMP Program Diagnosis

1 Introduction

Model-based diagnosis was first proposed in 1987 by Reiter [Reiter, 1987], this approach is mainly used to diagnose the systems composed of some physical components. Applying model-based diagnosis to program debugging is still a new field. Now, dependency model [Mateis et al., 1999] [Wieland, 2001] and value-base model [Mateis et al., 2000] are widely used in program diagnoses, both of which use program slicing technology [ Wotawa, 2002]: the former considers static slices of a program by analysing the dependency between variables, and the latter in fact uses dynamic slices depending on a special test by computing the valuation trajectory. But these methods are not competent in structural errors, and always result in very coarse diagnoses, i.e., too many candidate diagnoses.

This paper uses a simple imperative programming language-IMP which helps to focus on the important issues and avoid considering unnecessary detail. The syntax of IMP is shown in [Winskel, 1993]. For IMP programs, we present a new modeling approach with OCM, which can be used in IMP program diagnosis. Using this model and model-based diagnosis method, some logic errors can be found in IMP programs. The model can also be extended to all kinds of imperative programs. The advantages of this diagnosis method lie in its simple and regular presentation, uniform diagnosed objects, the usage of isomorphism assumptions in structure, and the usage of assertions about the expected program. These advantages make diagnoses more accurate, and even help to correct the faults by mutation of operator components.

In this paper, section 2 presents the operator component matrix model for programs. Section 3 further analyses the dependencies implied in the model, including black-box dependency and white-box dependency. Section 4 is the core of the paper, it defines such terms as isomorphism, abstract program, program specification and breakpoint, and under these terms, it also defines the model-based program diagnosis problem, diagnosis and conflict etc., and gives an example to illustrate them. Section 5 introduces related works, and the last section makes a conclusion.

2 Operator Component Matrix Model

2.1 Operator Component and 1-variable

Definition 1. In an n-ary function F n (x0,x1,…xn-1), we use a vector 0 1 1 , , ..., n n n n F F F to denote F n , then n k F (k=0,...n-1) is called the k-th operator component of n-ary function F n .

So, we can represent F n (x0,x1,…,xn-1) as

Where " " is called as operator-plus , " " is called as operator-times, and we stipulate that the symbol " " has associativity and exchangeability, and " " has associativity and distributivity to " ". So, we can also represent (1) as [ , , ... ][ , ,... ] n n n T F F F x x x .

We can prove that the above stipulation is reasonable, because under the stipulation, any legal expression in the form of operator components has a unique computable form, i.e. 0 0 1 1 1 1 ... n n F x F x F x is computable iff the sequence 1 2 ( , , , ) n F F F is a permutation of all the operator components of an n-ary function.

Definition 2. If a domain is composed of a single element 1, then we call the variable in the domain as 1-variable. i.e., we consider the constant 1 as a special variable.

Definition 3. Given two variables x and y, if the value of y is independent of x, we call x has a null operator component to y, represented as 0.

The arithmetic operators of IMP are defined as follows:

(1) n (x) n x , where n is a constant in N. Especially, we call 1 as identical operator component, which can also be represented as 1, but note that here 0 is different from null operator component 0.

x-y can be derived from and -1 i.e.,

Property 1. For a Aexp 1 , suppose x1, ..., xn are variables in a, then it can be represented in the form of

x-y=x+(-1) y= (x, -1(y))= 0 x ( 1 -1) y.

where F0, F1, F2, ..., Fn are operator component expressions. For instance, x (2 y+5)=( 1 1 5) 1 0 x ( 1 0 2) y

Property 2. For any F ,G ,H , m,n N

• F 0=0 F=0, F 1=1 F=F, F 0=0 F=F
• m n= m n

2.2 Presentation of Commands

In IMP programs, there are five types of commands: skip statement (skip), assignment statement (x:=a), compound statement (c0;c1), branch statement (if b then c0 else c1) and loop statement (while b do c). Here we present these statements in the form of OCM.

Assignment statement

Suppose the variable set of a program is 1 { ,..., } n x x then from property 1 and definition 3, each a Aexp takes the form of 0 1 1 1 ... n n F F x F x , where Fk=0 if variable xk does not occur in a.

So, we can denote assignment statement xk:=ak (k=1..n) as

When the program executes the assignment statement xk:=ak, only the value of variable xk will be changed. So we can consider that it implies such assignment statements as follows: xj:=xj (j=1,..n, j k),

i.e., xj:= 1 0 1 0 ... 1 0 j n x x x

C is a matrix composed of operator components, such matrix is called as operator component matrix, abbreviated as OCM. We can treat C as a state transition matrix.

Property 3. The first row of any state transition matrix has the form of [1 0 ... 0].

Property 4. In any row of any state transition matrix, there is at least one operator component that is not 0.

We label the commands with 1, 2, ..., n by their occurrence order in a program. Let X (k-1) be the program state before the execution of the k-th command, and X (k) be the program state after the execution of the k-th command, then X (k) =CkX (k-1) , where Ck is the state transition matrix of the k-th command. The value of an expression a under program state X (k) is represented as (a, X (k) ).

1 Aexp is the set of arithmetic expressions in IMP.

Skip statement

In a unit matrix, if we look number 1 as operator component 1, and number 0 as operator component 0, we call such matrix as unit OCM, represented as E. We also call the OCM composed of all 0 as zero OCM, represented as O.

So, skip statement (skip) can be represented as X:=EX .

Presentation of compound statement

Compound statements take the form of c0;c1. Suppose command c0 can be represented as X:=C0X and c1 can be represented as X:=C1X, where C0 and C1 are all OCMs, then we can represent the command as X:= (C1C0)X .

Presentation of branch statement

Branch statements take the form of if b then c0 else c1. Suppose command c0 can be represented as X:=C0X and c1 can be represented as X:=C1X, where C0 and C1 are all OCMs. Then we can represent the command as X:= (mC0 (1-m)C1)X, where m=1 when (b,X (0) )=true, otherwise m=0, X (0) is the program state before the execution of the command. Note that we look the result of m and 1-m as operator component 1 or 0.

Presentation of loop statement

Loop statements take the form as while b do c. Suppose command c can be represented as X:=CX, where C is an OCM. Then we can denote the command as X:= C n X, where n is the number of executions of loop body c (i.e. n= min{k|(b, X (k) ) =false, k 0}, where X (k) is the program state after the k-th execution of command c).

According to structural induction, it can be proved that any IMP program can be denoted in the form of X:=CX. We call C as the OCM model of the program.

2.3 An example

To facilitate analysis, we use an example shown in Fig 1.

Figure 1: An IMP program

Let X=[1 from to start stop i s] T , we can get the OCM model of the program

where Cl is the state transition matrix of the command labeled with l; m=1 if ( from to, X (0) )=true or else m=0; n=min{k|( i stop, X (4.2,k) )=false, k 0}, where X (0) is the program state before execution of the command labeled with 1; X (4.2,k) is the program state after the k-th execution of the command labeled 4.2.

If a program includes branch statements or loop statements, there are some unknown "constants" appearing in its OCM model, such as m, n in the above example. Though their values are dependent on a given test case, we still look them as formal constants.

3 Dependency Analysis

3.1 Black-box Dependency

Definition 4. Such an operator component is called a characteristic operator component, if it satisfies that

An OCM K is called the characteristic matrix of C, if K is constructed by replacing all the operator components in C except 0 with .

= ,

= , 0=0 = , 0=0 = .

Theorem 1. For any OCM C1, C2, if K1 and K2 are respectively the characteristic matrix of C1 and C2, then K1K2 is the characteristic matrix of C1C2.

Theorem 2. For any characteristic matrix K , the chain K, K 2 , K 3 , ..., K n satisfies one of the two cases as below:

1. N, n>N, K n =K N ;

Since the set of all characteristic matrixes of a given dimension is limited, any chain K, K 2 , K 3 , ..., K n must reach a fixed point or enter into a ring. The theorem indicates that the dependency in a loop is definite.

Definition 5. Assume that X is the vector of all variables in program 2 P , C is the OCM model of P, K is the characteristic matrix of C, then K is called the black-box dependency matrix of P.

From the example shown in Figure 1, we can get its black-box dependency matrix

2 Here 'program' indicates IMP program without special note.

From K, we can get the dependencies of the final values of variables to the initial values of variables; we represent these dependencies as X (n) B KX (0) , where X (n) is the final program state, X (0) is the initial program state. For instance, we extend the variable s, we can get

which means the final value of s is decided by the initial value of from, the initial value of to, and the constant value of s assigned in the program. Especially, if the black-box dependency of a variable includes the item 1, it shows the variable has been assigned with a constant in the program.

In the black-box dependency, if we find a variable does not appear in the dependencies of any other variables and its final value is not concerned about, the variable is usually considered useless, which can be deleted from the program.

3.2 White-box Dependency

Definition 6. For an OCM C, after replacing all its operator components except 0 and 1 with formal operator component represented as [p](p is the label set of the commands where the actual operators occur), the new components matrix H is called as the formal matrix of C. The properties of [p] are shown as follows:

Definition 7. Assume that X is the vector of all variables in program P , C is the model of P, H is the formal matrix of C, then we call H is the white-box dependency matrix of P.

From the example shown in Figure 1, we can get its white-box dependency matrix

From H, we can get the dependency of variables to commands which is represented as X (n) W HX (0) , where X (n) is the final program state, X (0) is the initial program state. For any variable in X, we can get its dependency to commands from H. For instance, we extend the variable s, and get

Then we establish a set s which is composed of all the command labels appearing in the right part, i.e.,

We call s as the white-box dependency of variable s, which means the final value of s is decided by the command set {1.1,1.3,2,3,4.1,4.2}. It can be proved to be equivalent with the program slice about the slicing criterion (s, 5) [Wotawa, 2002]. Note that white-box dependencies include data dependencies and control dependencies which are implied in the formal constants related to a branch statement or a loop statement.

3.3 Complexity analysis

In this model, the dimension of each OCM is (n+1) (n+1) where n is the number of variables in the program. It seems that the size of the matrix model would grow quickly with the number of variables. However, it is not a big problem, because when we diagnose a program, at one time, a diagnosed object is generally a program module (a procedure or a function) where the number of variables won't be too big. Moreover, we can store all state transition matrixes in the dense mode of sparse matrix.

4 Model-based Program Diagnosis

4.1 Isomorphism Assumption and Abstract Program

Definition 8. Two commands c and c are isomorphic, represented as Isomorph(c, c ), iff one of the following cases is satisfied:

1. c::=skip c ::=skip;
2. c::= x:=a0 c ::= y:=a1 x y VS(a0) = VS(a1) where x y means that x and y are the same variable, VS(a) means the set of all the variables in a;
3. c::= c0; c1 c ::= c0 ; c1 Isomorph(c0, c0 ) Isomorph(c1, c1 );
4. c::= if b then c0 else c1 c ::= if b then c0 else c1 Isomorph(c0, c0 ) Isomorph(c1, c1 );
5. c::= while b do c0 c ::= while b do c0 Isomorph(c0, c0 ).

Generally, a diagnosed program should be close to an expected program. That is to say, it is possible that minor revisions will make the diagnosed program correct. So, we always suppose that for any diagnosed program, there exists a "correct" program which is isomorphic with the diagnosed program. This assumption is called isomorphism assumption.

In some diagnosed programs, it is possible that some variable is lost in the right-side expression of an assignment statement, such that the isomorphism assumption cannot hold any more. But fortunately, we can extend the expression to a new equivalent expression which includes the lost variable by adding a null operator component. For instance, if x:=x+i is written as x:=x+1 by mistake, we can extend the expression x+1 to x+1 0 i. We call this case as extendable isomorphism, so it assures that many diagnosed programs are at least extendable isomorphic with a correct program.

Definition 9. For a given program (OCM model), if we replace all the operator components of the program with abstract operator components, the new program is called an abstract program. An abstract operator component is only a marker which does not refer to any concrete operator component.

For example, there is a command l: s:=s+i in a program (where l is the label), whose model is represented as s:= 0 (l) s 1 (l) i, and whose abstract model is represented as s:= 0 (l) s 1 (l) i, where 0 (l) and 1 (l) are abstract operator components. Suppose the mapping from the abstract model to the actual model is MAP, then MAP={{( 0 (l) , 0 (l) ), ( 1 (l) , 1 (l) )}}. In order to identify the operator components which have the same form, we add the command label to them. Suppose the command l: s:=s+i should be l: s:= s i , it is known that the abstract model of the "correct" command has the same form of the abstract model of the "wrong" command. Given a mapping MAP ={( 0 (l) , 0 (l) ), ( 1 (l) , 1 (l) )}, we can get the correct command from the abstract model.

Under the isomorphism assumption, we can construct the abstract model of expected program from the concrete model of the diagnosed program by replacing components in the concrete model with abstract components.

Note that each extended null operator component must be replaced by an abstract operator component in the abstract model.

4.2 Program Specification and Breakpoint

Program specification

To further describe the abstract program, we need offer some assertions about the static properties of it, each assertion is called a program specification [Morgan, 1998].

Definition 10. A program specification has the form as below:

where X is the set of variables, precond(X) is a description of the initial state of X, frame(X) indicates a piece of the abstract program including X, and postcond(X) gives a description of the final state of X after the "execution " of the piece of abstract program.

( precond(X), frame(X), postcond(X)),

Note that frame(X) cannot be executed until a concrete implementation is given. If slice(X) is a concrete implementation of frame(X), postcond(X) must come true after execution of slice(X) under the condition precond(X), and we denote it as {precond(X)} slice(X){ postcond(X)}.

precond(s, i)={s>0, i>0},

For example, to such a specification,

frame(s, i)={ s:= 0 s 1 i},

postcond(s, i)={s>1},

slice {s:=s+i} is an implementation of frame(s,i), but slice {s:=s i} is not .

Breakpoint

The position of a program is called a breakpoint, if where there is an assertion. The assertions about the variables in a breakpoint are called intermediate results. The value of variable x in a breakpoint B is represented as x(B).

In program diagnosis, a kind of special position is often used as breakpoints, and those positions are closely followed with a boolean expression, we call them as key points. For example, in Figure 1, there are two key points in the positions of label 1 and label 4.

Note that in a runtime of a program, a breakpoint may be passed by several times or zero times, but it corresponds to a unique position in a program.

For a given breakpoint, if all test cases should pass it, we call the assertions in this breakpoint as invariant ("always") assertion, otherwise, we call them as intermittent ("sometime") assertion [ Mayer and Stumptner, 2003].

So, it is known that any program specification must relate to two breakpoints, and the program code between the two breakpoints must be a legal (compound) command. For example, in Figure 1, the codes between breakpoint 1.3 and breakpoint 3 are not legal commands. If B1 and B2 are the breakpoints related to frame(X), we also represent frame(X) as frame(B1,B2, X). If X includes all the variables of the program, X can be omitted.

4.3 Program Diagnosis

Definition 11. A program diagnosis problem is a triple (SD, COMPS, SPECS) where SD is the OCM model of the actual program to be diagnosed, COMPS is the set of operator components in SD, SPECS is the set of program specifications.

Definition 12. Suppose (SD, COMPS, SPECS) is a program diagnosis problem. Let AD be the abstract program of SD, ACOMPS be the abstract operator components in AD, and MAP be the mapping from COMPS to ACOMPS. Then COMPS is a diagnosis iff there exists MAP : SA where is the set of all operator components and SA is a subset of ACOMPS, such that

• C COMPS\ , MAP (MAP -1 (C))=C.
• AD MAP SPECS is consistent, and

Under isomorphism assumption, AD SPECS is always consistent, that is, the expected program is an interpretation of AD.

Since any operator component corresponds to a command in the program, components in indicate the possible faults in the program.

Definition 13. Let be a diagnosis. If there exists no ' such that ' is also a diagnosis, then is a minimal diagnosis.

Definition 14. Suppose (SD, COMPS, SPECS) is a program diagnosis problem. Let AD be the abstract program of SD, ACOMPS be the abstract operator components in AD, and MAP be the mapping from COMPS to ACOMPS. Then C COMPS is a conflict set iff for any MAP : ACOMPS where MAP (C)=MAP(C), AD MAP SPECS is inconsistent.

Definition 15. Let C be a conflict set. If there exists no C' C such that C' is also a conflict set, then C is a minimal conflict set.

Theorem 3. If C1, C2,... Cn are all minimal conflict sets of program P, then all the least hitting sets of {C1, C2,... Cn} are minimal diagnoses of P.

The definitions about hitting set can be found in [Lin et al., 2003].

Theorem 4. Suppose PS=(precond(X), frame(B1,B2), postcond(X)) is a program specification. Let slice(B1,B2) be the implementation of frame(B1,B2) in the diagnosed program P. Given a program input, if (1) the program state in B1 is consistent with precond(X), (2) Y is the set of variables whose states in B2 are inconsistent with postcond(X) , and (3) C is the white-box dependency set of Y in slice(B1,B2), then C is a conflict set.

Theorem 5. Suppose PS=(precond(X), frame(B1,B2), postcond(X)) be a program specification. Let slice(B1,B2) be the implementation of frame(B1,B2) in the diagnosed program P. Suppose there is an equation y=f(W (0) ) in postcond(X), where y X, W X, and W (0) denotes the state of W in B1. If the black-box dependency set of y in slice(B1,B2) is not equal to W, then the white-box dependency set of y in slice(B1,B2) is a conflict set.

The conclusions of theorem 4 and 5 are obvious; theorem 5 is a special case of theorem 4.

4.4 A Diagnosis Example

Program diagnosis problem

Consider the program shown in Figure 1. Suppose command 4.1 is written as s:=s i by mistake. Then the program diagnosis problem is given as below:

SD=(X,C),

where X=[1 from to start stop i s] T

where Cl denotes the OCM model of the command labeled with l in the diagnosed program;

• = (C4.2C4.1) n C3C2(mC1.2C1.1 (1-m)C1.4C1.3)

COMPS={1 (1.1) , 1 (1.2) , 1 (1.3) , 1 (1.4) , 1 (2) , 0 (3) , 0 (4.1) , 1 (4.1) , 0 (4.2) , 1 (4.2) };

SPECS={PS1, PS2, PS3}, where

PS1=( {from to}, frame(1,3), {i=from}),

PS2=( {from to}, frame(1,3), {i=to}),

PS3=( {i stop}, frame(3,5),

where i (0) and stop (0) denote respectively the initial values of i and stop before the execution of the frame.

{i=stop (0) +1, s=(i (0) +stop (0) ) (i-i (0) )/2})

Diagnosis AD=(X,F),

where X=[1 from to start stop i s] T

F=F4F3F2F1

=(F4.2F4.1) n F3F2(mF1.2F1.1 (1-m)F1.4F1.3)

where Fi denotes the abstract OCM model of the command labeled with l in the expected program;

Given a set of inputs of the diagnosed program

INPUT={from=6, to=3} (i.e., from(1)=6 and to(1)=3) which satisfy the precondition of PS2, by running the diagnosed program with the inputs, we can get the results of i(3)=3 and to(3)=3, which are consistent with the postcond of PS2. In this case, we cannot get a conflict set.

We go on checking the other program specifications. By observing the values of the variables of the precondition of PS3 in breakpoint 3, we get i(3)=3 and stop(3)=6, which satisfy the precondition of PS3. And after applying PS3, s(5) should be (3+6) (7-3)/2=18. But s(5) equals to 360 actually, so there is a conflict. In frame(3,5), the white-box dependency of s is {3, 4.1, 4.2} which makes a conflict set. If we go on observing i, i(5) is always consistent with the postcondition of PS3, so the white-box dependency of i (i.e., {4.2}) must not be included in a conflict set. If we have another assertion to assure that statement 3 is right, we can finally get the diagnosis {4.1}.

We can correct the faults by mutating some operator components in the diagnoses, because the number of operator components is very limited except the operator components m (m N). Generally, we can assume that Max m 0 where Max is a finite number given in advance. When the mutations f0 (4.1) 0 (4.1) , f1 (4.1) 1 (4.1) take place, we can find the correct program.

5. Related Work

There are a lot of works developed in model-based program diagnosis during the years, among which the most important work is about program slicing [Wotawa, 2002]. Our model gives a new and simpler method of computing program slices (i.e. white-box dependency).

In the presentation of the abstract model of the expected program, in order to improve the diagnosis capabilities, [Chen et al., 2005] also uses assertions to specify an abstract model. But it does not deal with abstraction in program structure and it only works on the value-based model. Our model has stronger presentation capability, which uses more information about the existing program structure under the isomorphism assumption.

In correcting the faults, [Wotawa, 2001] also discusses a different mutation method, which cannot assure us of finding the correct program by mutation since the mutation scope is too large.

We have also developed the presentation of an array in the form of operator components. For example, array x with x[0]=a, x[1]=b, x[2]=c can be represented as x=[0] a [1] b [2] c where [0], [1] and [2] are all operator components; x[0]:=a can be represented as : [0] [0] a x x under the property [ ] [ ] 0 n n , [ ] [ ] [ ] ( ) n m m n m ; expression x[0] can be represented as {0} x where {0} is an operator component under the property{ } [ ] 1 n n , { } [ ] 0 ( ) n m n m . Due to the space limitation, we don't discuss it in detail.

6. Conclusion

This paper presents a new model for IMP programs with OCM. OCM model and isomorphism assumption are the basis of abstract programs, and we use the assertions of program specifications to describe the abstract programs. Acquisition of program specifications is a key problem, which needs more knowledge about the expected program. Obviously, the more specifications are achieved, the more accurate diagnoses are.

OCM model has a uniform presentation, which comply with the rules for matrix operations. We can got the dependency easily from the OCM model by using characteristic operator component and formal operator component.

Due to the space limitation, we cannot discuss more diagnosis cases in detail. For example, we do not consider the diagnosis for the condition parts of branch statements and loop statements. Generally, we put these conditions into the program specifications.

Moreover, by using black-box dependency and extending null operator components, we can find some structural faults such as variable missing. In dependency models, structural faults always result in the mistakes of program slicing [Wotawa, 2002], thereby result in wrong diagnoses.