The Java[1] and C#[2] programming language specifications require that the compiler report a compile-time error if the analysis fails.
In Java, this analysis was formalized by Stärk et al.,[3] and some correct programs are rejected and must be altered to introduce explicit unnecessary assignments.
[5] The second way to solve the problem is to automatically initialize all locations to some fixed, predictable value at the point at which they are defined, but this introduces new assignments that may impede performance.
The verifier repeatedly iterates over the abstract syntax tree and uses the data-flow equations to migrate information between the sets until a fixed point can be reached.
When these are introduced, the resulting data flow may have multiple fixed points, as in this example: Since the label L can be reached from two locations, the control-flow equation for goto dictates that before(2) = after(1) intersect before(3).
An additional issue is that a control-flow jump may render certain control flows infeasible; for example, in this code fragment the variable i is definitely assigned before it is used: The data-flow equation for if says that after(2) = after(return) intersect after(i = j).