An Example of Intra-Function Debugging

Consider the following C program implementing bubblesort algorithm. The correct version should be as follows.

1:  bubblesort(p, n) {
2:    swp = true;
3:    while (swp) {
4:      swp = false;
5:      i = 1;
6:      q1 = p;
7:      q2 = p + 1;
8:      while (i < n) {
9:        if (*q1 > *q2) {
10:         x = *q1;
11:         *q1 = *q2;
12:         *q2 = x;
13:         swp = true;
14:       }
15:       i = i + 1;
16:       q1 = q1 + 1;
17:       q2 = q2 + 1;
18:     }
19:   }
20:   return p;
21: }

But the programmer written this program wrongly as follows.

1:  bubblesort(p, n) {
2:    swp = true;
3:    while (swp) {
4:      swp = false;
5:      i = 1;
6:      q1 = p;
7:      q2 = p + 1;
8:      while (i < n) {
9:        if (*q1 > *q2) {
10:         *q1 = *q2;
11:         *q2 = *q1;
12:         swp = true;
13:       }
14:       i = i + 1;
15:       q1 = q1 + 1;
16:       q2 = q2 + 1;
17:     }
18:   }
19:   return p;
20: }

If inputs of this program is p pointed to a list with five elements [5, 1, 4, 2, 8], then the output is [1, 1, 2, 2, 8]. But the expected results should be a pointer pointed to a list with elements [1, 2, 4, 5, 8].

Let us using our structural operational semantics based formal approach to debugging this program.

1. Tracing Procedure

Firstly, let us using the structural operational semantics of tracing to gather all necessary information in a trace stack. The reexecution of the ill-designed program is as follows.

1:  bubblesort(p, n) { ψ0 = (p ↦ r[0]) σ0 = (n ↦ 5, r[0] ↦ 5, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8) ε0 = { }
2:    swp = true; ψ1 = (p ↦ r[0]) σ1 = (n ↦ 5, r[0] ↦ 5, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true) ε1 = { }
3:    while (swp) { ψ2 = (p ↦ r[0]) σ2 = (n ↦ 5, r[0] ↦ 5, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true) ε2 = { }
4:      swp = false; ψ3 = (p ↦ r[0]) σ3 = (n ↦ 5, r[0] ↦ 5, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false) ε3 = {〈swp, ψ2, σ2〉}
5:      i = 1; ψ4 = (p ↦ r[0]) σ4 = (n ↦ 5, r[0] ↦ 5, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 1) ε4 = {〈swp, ψ2, σ2〉}
6:      q1 = p; ψ5 = (p ↦ r[0], q1 ↦ r[0]) σ5 = (n ↦ 5, r[0] ↦ 5, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 1) ε5 = {〈swp, ψ2, σ2〉}
7:      q2 = p + 1; ψ6 = (p ↦ r[0], q1 ↦ r[0], q2 ↦ r[1]) σ6 = (n ↦ 5, r[0] ↦ 5, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 1) ε6 = {〈swp, ψ2, σ2〉}
8:      while (i < n) { ψ7 = (p ↦ r[0], q1 ↦ r[0], q2 ↦ r[1]) σ7 = (n ↦ 5, r[0] ↦ 5, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 1) ε7 = {〈swp, ψ2, σ2〉}
9:        if (*q1 > *q2) { ψ8 = (p ↦ r[0], q1 ↦ r[0], q2 ↦ r[1]) σ8 = (n ↦ 5, r[0] ↦ 5, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 1) ε8 = {〈swp, ψ2, σ2〉, 〈i < n, ψ7, σ7〉}
10:         *q1 = *q2; ψ9 = (p ↦ r[0], q1 ↦ r[0], q2 ↦ r[1]) σ9 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 1) ε9 = {〈swp, ψ2, σ2〉, 〈i < n, ψ7, σ7〉, 〈*q1 > *q2, ψ8, σ8〉}
11:         *q2 = *q1; ψ10 = (p ↦ r[0], q1 ↦ r[0], q2 ↦ r[1]) σ10 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 1) ε10 = {〈swp, ψ2, σ2〉, 〈i < n, ψ7, σ7〉, 〈*q1 > *q2, ψ8, σ8〉}
12:         swp = true; ψ11 = (p ↦ r[0], q1 ↦ r[0], q2 ↦ r[1]) σ11 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 1) ε11 = {〈swp, ψ2, σ2〉, 〈i < n, ψ7, σ7〉, 〈*q1 > *q2, ψ8, σ8〉}
13:       }
14:       i = i + 1; ψ12 = (p ↦ r[0], q1 ↦ r[0], q2 ↦ r[1]) σ12 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 2) ε12 = {〈swp, ψ2, σ2〉, 〈i < n, ψ7, σ7〉}
15:       q1 = q1 + 1; ψ13 = (p ↦ r[0], q1 ↦ r[1], q2 ↦ r[1]) σ13 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 2) ε13 = {〈swp, ψ2, σ2〉, 〈i < n, ψ7, σ7〉}
16:       q2 = q2 + 1; ψ14 = (p ↦ r[0], q1 ↦ r[1], q2 ↦ r[2]) σ14 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 2) ε14 = {〈swp, ψ2, σ2〉, 〈i < n, ψ7, σ7〉}
17:     }
18:   }
19:   return p;
20: }

ψ14 = (p ↦ r[0], q1 ↦ r[1], q2 ↦ r[2]),
σ14 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 2),
ε14 = {〈swp, ψ2, σ2〉, 〈i < n, ψ7, σ7〉}

1:  bubblesort(p, n) {
2:    swp = true;
3:    while (swp) {
4:      swp = false;
5:      i = 1;
6:      q1 = p;
7:      q2 = p + 1;
8:      while (i < n) { ψ15 = (p ↦ r[0], q1 ↦ r[1], q2 ↦ r[2]) σ15 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 2) ε15 = {〈swp, ψ2, σ2〉}
9:        if (*q1 > *q2) { ψ16 = (p ↦ r[0], q1 ↦ r[1], q2 ↦ r[2]) σ16 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 2) ε16 = {〈swp, ψ2, σ2〉, 〈i < n, ψ15, σ15〉}
10:         *q1 = *q2;
11:         *q2 = *q1;
12:         swp = true;
13:       }
14:       i = i + 1; ψ17 = (p ↦ r[0], q1 ↦ r[1], q2 ↦ r[2]) σ17 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 3) ε17 = {〈swp, ψ2, σ2〉, 〈i < n, ψ15, σ15〉}
15:       q1 = q1 + 1; ψ18 = (p ↦ r[0], q1 ↦ r[2], q2 ↦ r[2]) σ18 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 3) ε18 = {〈swp, ψ2, σ2〉, 〈i < n, ψ15, σ15〉}
16:       q2 = q2 + 1; ψ19 = (p ↦ r[0], q1 ↦ r[2], q2 ↦ r[3]) σ19 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 3) ε19 = {〈swp, ψ2, σ2〉, 〈i < n, ψ15, σ15〉}
17:     }
18:   }
19:   return p;
20: }

ψ19 = (p ↦ r[0], q1 ↦ r[2], q2 ↦ r[3]),
σ19 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 3),
ε19 = {〈swp, ψ2, σ2〉, 〈i < n, ψ15, σ15〉}

1:  bubblesort(p, n) {
2:    swp = true;
3:    while (swp) {
4:      swp = false;
5:      i = 1;
6:      q1 = p;
7:      q2 = p + 1;
8:      while (i < n) { ψ20 = (p ↦ r[0], q1 ↦ r[2], q2 ↦ r[3]) σ20 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 3) ε20 = {〈swp, ψ2, σ2〉}
9:        if (*q1 > *q2) { ψ21 = (p ↦ r[0], q1 ↦ r[2], q2 ↦ r[3]) σ21 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 4, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 3) ε21 = {〈swp, ψ2, σ2〉, 〈i < n, ψ20, σ20〉}
10:         *q1 = *q2; ψ22 = (p ↦ r[0], q1 ↦ r[2], q2 ↦ r[3]) σ22 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 3) ε21 = {〈swp, ψ2, σ2〉, 〈i < n, ψ20, σ20〉, 〈*q1 > *q2, ψ21, σ21〉}
11:         *q2 = *q1; ψ23 = (p ↦ r[0], q1 ↦ r[2], q2 ↦ r[3]) σ23 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 3) ε21 = {〈swp, ψ2, σ2〉, 〈i < n, ψ20, σ20〉, 〈*q1 > *q2, ψ21, σ21〉}
12:         swp = true; ψ24 = (p ↦ r[0], q1 ↦ r[2], q2 ↦ r[3]) σ24 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 3) ε21 = {〈swp, ψ2, σ2〉, 〈i < n, ψ20, σ20〉, 〈*q1 > *q2, ψ21, σ21〉}
13:       }
14:       i = i + 1; ψ25 = (p ↦ r[0], q1 ↦ r[2], q2 ↦ r[3]) σ25 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 4) ε21 = {〈swp, ψ2, σ2〉, 〈i < n, ψ20, σ20〉}
15:       q1 = q1 + 1; ψ26 = (p ↦ r[0], q1 ↦ r[3], q2 ↦ r[3]) σ26 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 4) ε21 = {〈swp, ψ2, σ2〉, 〈i < n, ψ20, σ20〉}
16:       q2 = q2 + 1; ψ27 = (p ↦ r[0], q1 ↦ r[3], q2 ↦ r[4]) σ27 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 4) ε21 = {〈swp, ψ2, σ2〉, 〈i < n, ψ20, σ20〉}
17:     }
18:   }
19:   return p;
20: }

ψ27 = (p ↦ r[0], q1 ↦ r[3], q2 ↦ r[4]),
σ27 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 4),
ε21 = {〈swp, ψ2, σ2〉, 〈i < n, ψ20, σ20〉}

1:  bubblesort(p, n) {
2:    swp = true;
3:    while (swp) {
4:      swp = false;
5:      i = 1;
6:      q1 = p;
7:      q2 = p + 1;
8:      while (i < n) { ψ28 = (p ↦ r[0], q1 ↦ r[3], q2 ↦ r[4]) σ28 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 4) ε28 = {〈swp, ψ2, σ2〉}
9:        if (*q1 > *q2) { ψ29 = (p ↦ r[0], q1 ↦ r[3], q2 ↦ r[4]) σ29 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 4) ε29 = {〈swp, ψ2, σ2〉, 〈i < n, ψ28, σ28〉}
10:         *q1 = *q2;
11:         *q2 = *q1;
12:         swp = true;
13:       }
14:       i = i + 1; ψ30 = (p ↦ r[0], q1 ↦ r[3], q2 ↦ r[4]) σ30 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 5) ε30 = {〈swp, ψ2, σ2〉, 〈i < n, ψ28, σ28〉}
15:       q1 = q1 + 1; ψ31 = (p ↦ r[0], q1 ↦ r[4], q2 ↦ r[4]) σ31 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 5) ε31 = {〈swp, ψ2, σ2〉, 〈i < n, ψ28, σ28〉}
16:       q2 = q2 + 1; ψ32 = (p ↦ r[0], q1 ↦ r[4], q2 ↦ ⊥) σ32 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 5) ε32 = {〈swp, ψ2, σ2〉, 〈i < n, ψ28, σ28〉}
17:     }
18:   }
19:   return p;
20: }

ψ32 = (p ↦ r[0], q1 ↦ r[4], q2 ↦ ⊥),
σ32 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 5),
ε32 = {〈swp, ψ2, σ2〉, 〈i < n, ψ28, σ28〉}.

1:  bubblesort(p, n) {
2:    swp = true;
3:    while (swp) {
4:      swp = false;
5:      i = 1;
6:      q1 = p;
7:      q2 = p + 1;
8:      while (i < n) { ψ33 = (p ↦ r[0], q1 ↦ r[4], q2 ↦ ⊥) σ33 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 5) ε33 = {〈swp, ψ2, σ2〉}
9:        if (*q1 > *q2) {
10:         *q1 = *q2;
11:         *q2 = *q1;
12:         swp = true;
13:       }
14:       i = i + 1;
15:       q1 = q1 + 1;
16:       q2 = q2 + 1;
17:     }
18:   }
19:   return p;
20: }

ψ33 = (p ↦ r[0], q1 ↦ r[4], q2 ↦ ⊥),
σ33 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 5),
ε33 = {〈swp, ψ2, σ2〉}.

1:  bubblesort(p, n) {
2:    swp = true;
3:    while (swp) { ψ34 = (p ↦ r[0], q1 ↦ r[4], q2 ↦ ⊥) σ34 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ true, i ↦ 5) ε34 = {}
4:      swp = false; ψ35 = (p ↦ r[0], q1 ↦ r[4], q2 ↦ ⊥) σ35 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 5) ε35 = {〈swp, ψ34, σ34〉}
5:      i = 1; ψ36 = (p ↦ r[0], q1 ↦ r[4], q2 ↦ ⊥) σ36 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 1) ε36 = {〈swp, ψ34, σ34〉}
6:      q1 = p; ψ37 = (p ↦ r[0], q1 ↦ r[0], q2 ↦ ⊥) σ37 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 1) ε37 = {〈swp, ψ34, σ34〉}
7:      q2 = p + 1; ψ38 = (p ↦ r[0], q1 ↦ r[0], q2 ↦ r[1]) σ38 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 1) ε38 = {〈swp, ψ34, σ34〉}
8:      while (i < n) { ψ39 = (p ↦ r[0], q1 ↦ r[0], q2 ↦ r[1]) σ39 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 1) ε39 = {〈swp, ψ34, σ34〉}
9:        if (*q1 > *q2) { ψ40 = (p ↦ r[0], q1 ↦ r[0], q2 ↦ r[1]) σ40 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 1) ε40 = {〈swp, ψ34, σ34〉, 〈i < n, ψ39, σ39〉}
10:         *q1 = *q2;
11:         *q2 = *q1;
12:         swp = true;
13:       }
14:       i = i + 1; ψ41 = (p ↦ r[0], q1 ↦ r[0], q2 ↦ r[1]) σ41 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 2) ε41 = {〈swp, ψ34, σ34〉, 〈i < n, ψ39, σ39〉}
15:       q1 = q1 + 1; ψ42 = (p ↦ r[0], q1 ↦ r[1], q2 ↦ r[1]) σ42 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 2) ε42 = {〈swp, ψ34, σ34〉, 〈i < n, ψ39, σ39〉}
16:       q2 = q2 + 1; ψ43 = (p ↦ r[0], q1 ↦ r[1], q2 ↦ r[2]) σ43 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 2) ε43 = {〈swp, ψ34, σ34〉, 〈i < n, ψ39, σ39〉}
17:     }
18:   }
19:   return p;
20: }

ψ43 = (p ↦ r[0], q1 ↦ r[1], q2 ↦ r[2]),
σ43 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 2),
ε43 = {〈swp, ψ34, σ34〉, 〈i < n, ψ39, σ39〉}.

1:  bubblesort(p, n) {
2:    swp = true;
3:    while (swp) {
4:      swp = false;
5:      i = 1;
6:      q1 = p;
7:      q2 = p + 1;
8:      while (i < n) { ψ44 = (p ↦ r[0], q1 ↦ r[1], q2 ↦ r[2]) σ44 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 2) ε44 = {〈swp, ψ34, σ34〉}
9:        if (*q1 > *q2) { ψ45 = (p ↦ r[0], q1 ↦ r[1], q2 ↦ r[2]) σ45 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 2) ε45 = {〈swp, ψ34, σ34〉, 〈i < n, ψ44, σ44〉}
10:         *q1 = *q2;
11:         *q2 = *q1;
12:         swp = true;
13:       }
14:       i = i + 1; ψ46 = (p ↦ r[0], q1 ↦ r[1], q2 ↦ r[2]) σ46 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 3) ε46 = {〈swp, ψ34, σ34〉, 〈i < n, ψ44, σ44〉}
15:       q1 = q1 + 1; ψ47 = (p ↦ r[0], q1 ↦ r[2], q2 ↦ r[2]) σ47 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 3) ε47 = {〈swp, ψ34, σ34〉, 〈i < n, ψ44, σ44〉}
16:       q2 = q2 + 1; ψ48 = (p ↦ r[0], q1 ↦ r[2], q2 ↦ r[3]) σ48 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 3) ε48 = {〈swp, ψ34, σ34〉, 〈i < n, ψ44, σ44〉}
17:     }
18:   }
19:   return p;
20: }

ψ48 = (p ↦ r[0], q1 ↦ r[2], q2 ↦ r[3]),
σ48 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 3),
ε48 = {〈swp, ψ34, σ34〉, 〈i < n, ψ44, σ44〉}.

1:  bubblesort(p, n) {
2:    swp = true;
3:    while (swp) {
4:      swp = false;
5:      i = 1;
6:      q1 = p;
7:      q2 = p + 1;
8:      while (i < n) { ψ49 = (p ↦ r[0], q1 ↦ r[2], q2 ↦ r[3]) σ49 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 3) ε49 = {〈swp, ψ34, σ34〉}
9:        if (*q1 > *q2) { ψ48 = (p ↦ r[0], q1 ↦ r[2], q2 ↦ r[3]) σ50 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 3) ε48 = {〈swp, ψ34, σ34〉, 〈i < n, ψ49, σ49〉}
10:         *q1 = *q2;
11:         *q2 = *q1;
12:         swp = true;
13:       }
14:       i = i + 1; ψ51 = (p ↦ r[0], q1 ↦ r[2], q2 ↦ r[3]) σ51 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 4) ε51 = {〈swp, ψ34, σ34〉, 〈i < n, ψ49, σ49〉}
15:       q1 = q1 + 1; ψ52 = (p ↦ r[0], q1 ↦ r[3], q2 ↦ r[3]) σ52 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 4) ε52 = {〈swp, ψ34, σ34〉, 〈i < n, ψ49, σ49〉}
16:       q2 = q2 + 1; ψ53 = (p ↦ r[0], q1 ↦ r[3], q2 ↦ r[4]) σ53 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 4) ε53 = {〈swp, ψ34, σ34〉, 〈i < n, ψ49, σ49〉}
17:     }
18:   }
19:   return p;
20: }

ψ53 = (p ↦ r[0], q1 ↦ r[3], q2 ↦ r[4]),
σ53 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 4),
ε53 = {〈swp, ψ34, σ34〉, 〈i < n, ψ49, σ49〉}.

1:  bubblesort(p, n) {
2:    swp = true;
3:    while (swp) {
4:      swp = false;
5:      i = 1;
6:      q1 = p;
7:      q2 = p + 1;
8:      while (i < n) { ψ54 = (p ↦ r[0], q1 ↦ r[3], q2 ↦ r[4]) σ54 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 4) ε54 = {〈swp, ψ34, σ34〉}
9:        if (*q1 > *q2) { ψ55 = (p ↦ r[0], q1 ↦ r[3], q2 ↦ r[4]) σ55 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 4) ε55 = {〈swp, ψ34, σ34〉, 〈i < n, ψ54, σ54〉}
10:         *q1 = *q2;
11:         *q2 = *q1;
12:         swp = true;
13:       }
14:       i = i + 1; ψ56 = (p ↦ r[0], q1 ↦ r[3], q2 ↦ r[4]) σ56 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 5) ε56 = {〈swp, ψ34, σ34〉, 〈i < n, ψ54, σ54〉}
15:       q1 = q1 + 1; ψ57 = (p ↦ r[0], q1 ↦ r[4], q2 ↦ r[4]) σ57 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 5) ε57 = {〈swp, ψ34, σ34〉, 〈i < n, ψ54, σ54〉}
16:       q2 = q2 + 1; ψ58 = (p ↦ r[0], q1 ↦ r[4], q2 ↦ ⊥) σ58 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 5) ε58 = {〈swp, ψ34, σ34〉, 〈i < n, ψ54, σ54〉}
17:     }
18:   }
19:   return p;
20: }

ψ58 = (p ↦ r[0], q1 ↦ r[4], q2 ↦ ⊥),
σ58 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 5),
ε58 = {〈swp, ψ34, σ34〉, 〈i < n, ψ54, σ54〉}.

1:  bubblesort(p, n) {
2:    swp = true;
3:    while (swp) {
4:      swp = false;
5:      i = 1;
6:      q1 = p;
7:      q2 = p + 1;
8:      while (i < n) { ψ59 = (p ↦ r[0], q1 ↦ r[4], q2 ↦ ⊥) σ59 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 5) ε59 = {〈swp, ψ34, σ34〉}
9:        if (*q1 > *q2) {
10:         *q1 = *q2;
11:         *q2 = *q1;
12:         swp = true;
13:       }
14:       i = i + 1;
15:       q1 = q1 + 1;
16:       q2 = q2 + 1;
17:     }
18:   }
19:   return p;
20: }

ψ59 = (p ↦ r[0], q1 ↦ r[4], q2 ↦ ⊥),
σ59 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 5),
ε59 = {〈swp, ψ34, σ34〉}.

1:  bubblesort(p, n) {
2:    swp = true;
3:    while (swp) { ψ60 = (p ↦ r[0], q1 ↦ r[4], q2 ↦ ⊥) σ60 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 5) ε60 = { }
4:      swp = false;
5:      i = 1;
6:      q1 = p;
7:      q2 = p + 1;
8:      while (i < n) {
9:        if (*q1 > *q2) {
10:         *q1 = *q2;
11:         *q2 = *q1;
12:         swp = true;
13:       }
14:       i = i + 1;
15:       q1 = q1 + 1;
16:       q2 = q2 + 1;
17:     }
18:   }
19:   return p; ψ61 = (p ↦ r[0], q1 ↦ r[4], q2 ↦ ⊥) σ61 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 5) ε61 = { }
20: }

ψ61 = (p ↦ r[0], q1 ↦ r[4], q2 ↦ ⊥),
σ61 = (n ↦ 5, r[0] ↦ 1, r[1] ↦ 1, r[2] ↦ 2, r[3] ↦ 2, r[4] ↦ 8, swp ↦ false, i ↦ 5),
ε61 = { }.

If we denote 〈S, ψi, σi, εi〉 as Ci, then π = {C1, C3, C4, C5, C6, C8, C9, C10, C11, C12, C13, C14, C17, C18, C19, C22, C23, C24, C25, C26, C27, C30, C31, C32, C35, C36, C37, C38, C41, C42, C43, C46, C47, C48, C51, C52, C53, C56, C57, C58}.

2. Locating Procedure

We know that the execution result of this program is list with elements [1, 1, 2, 2, 8] pointed by p which is not as expected. The expected results of this program is a sorted list with elements [1, 2, 4, 5, 8].

The locating procedure of this program is as follows.

1. From the expected results of this program, we know that the third element of the list is not as expected, i.e. the value of r[2] is not as expected.

2. According the locating rule for variable, the first assignment S-configuration which change the value of r[2] should be checked next, that is, C22 = 〈*q1 = *q2, ψ22, σ22, ε22〉.

3. We can verify that what q1 and q2 point to is as expected, and the value of *p2 is also as expected. But the value of the right-hand side arithmetic expression is not as expected. According to locating rules for assignment, a bug is found and the right-hand arithmetic expression should be reconstructed to meet the expected value.

4. However, no matter how you reconstruct the arithmetic expression to fix this bug, a new bug can be found by re-run the tracing and locating procedure, i.e. there exists a structure design error in this program. To fix this bug, the structure of this program should be changed. In this case,

10:         *q1 = *q2;
11:         *q2 = *q1;

should be changed to

10:         x = *q1;
11:         *q1 = *q2;
12:         *q2 = x;

 

    Last update: May 2, 2012