# Incremental Formula-Based Fix Localization
## 2 Background
### Fault Localization Problem  
Fault localization is the problem of identifying program statements that responsible for an observed failure in a software program. Without knowing the correct program in advance, it is impractical to automatically pinpoint the faults with absolute accuracy. Indeed, any program statement or subset of program statements, that, if suitably modified, can remove the failure, is considered possibly faulty [12; 14; 16]. Since checking the existence of an actual syntactic fix for a program is extremely computation expensive [7; 21], we check for the existence of an _angelic fix_ that removes the failure in an angelically way by replacing program expressions with suitable non-deterministic values (i.e., _angelic values_). In the context of this paper, we consider fault localization to be the problem of finding angelic fix candidates for an observed failure in a software program. An _angelic fix candidate (AFC)_ consists of (1) a fix locations set (i.e., a set of suspicious statements) and (2) angelic values (i.e., set of values that, if substituted for these statements, would make the given failure execution become a success). Essentially, the angelic values represents an _angelic execution_ that is diverted from the original program execution by replacing the value of specific variables at the fix locations with their corresponding angelic values. Becausethere may exist a large number of angelic fix candidates, providing the developer with a set containing only minimal angelic fix candidates (i.e., angelic fix candidates that have a minimal fix location set) is more referable. Thus, given a faulty program and a failing test case that, in its execution, demonstrates a failure, we produce a set of minimal angelic fix candidates (MFCs) that make the given test execution become a success. Figure 1 shows a method _foo_ and a unit test method _testFoo_, which checks if _foo_ returns a certain value when it is called on a particular input. The unit test method _testFoo_ calls _foo_ with an input \(x=3,y=5\) and asserts that the output is equal to \(-2\). However, because of a fault at line 3, where the assignment \((a=2*x)\) is accidentally written as \((a=x)\), the method _foo_ returns 8, thus violating the assertion, and the test fails. After running the test case _testFoo_, we know there is fault in the program _foo_. However, without knowledge about the correct program, a program statement can be considered possibly faulty if there exists a suitable replacement for these statements to make the observed error disappear. We use \(x=(L,V)\) to denote an angelic fix candidates x, where \(L=\{l_{1},...,l_{n}\}\) is its fix locations set, and \(V=\{\textit{``v${}_{1}\textit{''}=val${}_{1},...,\textit{``v${}_{m}\textit{''} =val${}_{m}$}\}\}\) is the corresponding set of angelic values. In reality, the size of set L and set V may different, e.g., a statement may have multiple instances in an execution. However, for simplifying the representation, we assume \(m=n\); thus, the angelic values \(V[i]\) corresponds to the statement at fix location \(L[i]\). Each item \"\(\textit{``v${}_{i}\textit{''}=val${}_{i}$}\) in an the angelic values set \(V\) is a mapping from an angelic value \(val${}_{i}\) to variable \(v${}_{i}\) at the fix location point i. Given the program and a failing test case in Figure 1, our approach produces five minimal angelic fix candidates, which are: \(mfc_{1}=(\{8\},\{\textit{``return''}=-2\})\); \(mfc_{2}=(\{6\},\{\textit{``guard''}=\textit{True}\})\); \(mfc_{3}=(\{3\},\{\textit{``a''}=5\})\); \(mfc_{4}=(\{1\},\{\textit{``b''}=-2\})\); and \(mfc_{5}=(\{2,4\},\{\textit{``guard''}=False${}_{\textit{``a''}=5\}$})\). Consider MFC \(mfc_{3}=(\{3\},\{\textit{``a${}_{1}\textit{''}=5\}\})\). This MFC states that the failure can be removed by modifying the assignment \((a=x)\) at line 3 such that it assigns the angelic value 5 to the variable \(a\).