Model-Based Debugger Illustration

To give an impression of how automatic model-based debugging can aid fault localization, we illustrate a small debugging session using our prototype debugger.

Consider the following program:

class Point {
    int x;
    int y;
    Point(int x, int y) {
          this.x = x;
          this.y = y;
    Point plus(Point p) {
          int newX = x + p.x;
          int newY = x + p.y; // faulty
          Point r = new Point(newX, newY);
          return r;
    static void demo() {
          Point a = new Point(0,1);
          Point b = new Point(2,3);
          a.x = 4;
          a.y = 5;
          Point s =;

If we run the program, it becomes evident that the computed result is incorrect: the expression s.y evaluates to 7, which does not match the expected value 8. The reason for the misbehaviour of the program is found in line 10, where newY is computed using the values of x and p.y. Instead, y and p.y should have been used. In the following we show how to locate the fault using our debugger.

The first step is to load the program’s source into the debugger and to select the program entry point. The source code of the selected method is shown in the right half of the window.

Next, the program is run and the final values for variables are displayed in the observations window. The user can now examine the values and specify the expected values of variables in case the computed result is incorrect. In our example, only the value of s.y is incorrect and we specify the correct value 8.

Continuing the debugging session, the debugger computes the set of possibly faulty statements and prompts us with a series of questions, with the ultimate goal to identify a single part of the program which causes the problem. The questions are chosen such that the amount of user interaction is minimised, while discriminating between different fault candidates. In the figure below, statements that are possibly faulty are coloured green, while other statements are displayed in black. The part of the program that is selected in the observations window is displayed with a dark background.

The first question we are asked is to confirm that variable b points to an object that was created in that line and is of type Point. As this is correct, we simply click ‘Continue’.

Our answer to the previous question eliminated line 16 from our list of fault candidates. Similarly, statement 15 is excluded. After that, the debugger has identified the expression as the single cause of the erroneous behaviour.

The debugger automatically descends into the method and computes the fault candidates using the specified and inferred values from the calling method.

As we can see, the debugger locates the statements newY=x+p.y and new Point(newX,newY) as possible causes of the fault. Continuing debugging, we are asked to investigate the expected value of newY after line 10 has executed. We enter the expected value 8 in the observations window and click continue:

Knowing the correct value of newY, the debugger can eliminate the new expression in line 11 and the assignment to newY in line 10. Thus, the expression on the right hand side of the assignment is the only remaining valid explanation for the program‘s misbehaviour.

While we could stop at this point and let the user figure out how the statement is faulty, faulty subexpressions can be identified using similar reasoning principles. Continuing debugging, the debugger descends the computation tree and asks us to confirm whether the values of p.y and x are correct.

At this point it has become obvious that the only explanation for the erroneous behaviour is the expressions x in line 10. The debugger displays the identified fault and stops the debugging process.

While this example is trivial and the fault can easily be located without the help of our tool, for more complex programs this process quickly becomes more involved and requires tool assistance to track assumptions, correct and faulty computations, and possible faults.

While interactive debugging is suitable for isolating a single fault from a small set of fault candidates, other debugging strategies are necessary to deal with larger programs and multiple test cases. Our debugging prototype provides means to deal with multiple test cases without the need for the user to specify expected values for each case. This is done by loading test case definitions from a file and select the test cases that should be applied.

The following example deals with a program that simulates a binary full adder hardware circuit. For example, a program very similar to this could be generated as intermediate code for a more high-level description when developing hardware circuits. The fault is in line 16, where and(b,s5) has been replaced by not(b). The javadoc-like tags in comments are used to mark the locations in the program where the assertions from test cases are inserted.

class Adder {
    public static void test(boolean a, boolean b, boolean c)
        boolean s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13;
        boolean z, cn;

        s1 = and(b,c);
        s2 = and(a,c);
        s3 = and(a,b);
        s4 = or(s1,s2);
        cn = or(s3,s4);

        s5 = not(a);
        s6 = not(b);  // should be and(b,s5)
        s7 = not(b);
        s8 = and(a,s7);
        s9 = or(s6,s8);

        s10 = not(s9);
        s11 = and(c,s10);
        s12 = not(c);
        s13 = and(s9,s12);
        z = or(s11,s13);


    static boolean not(boolean x)
        return !x;

    static boolean and(boolean x, boolean y)
        return x && y;

    static boolean or(boolean x, boolean y)
        return x || y;

Instead of specifying inputs and expected results for the variables manually, we load test case definitions from a file and select the first four test cases to be applied to our program. While we could also select the remaining tests, this does not help the debugging process as the computed values match the expected values.

Using the selected test cases, our debugger identifies three statements as possible bugs (without questioning the user). Discriminating between those is not possible without further information provided by the user.

In case the fault needs to be narrowed down further, the interactive debugging process described in the first example can be applied.