Resumo | Intra-procedural data flow testing coverage data can be very expensive to collect, especially for long running programs tracking the assignment of a value to a variable and its subsequent use,i.e., a definition-use association (dua). Recently, a novel algorithm, called Bitwise Algorithm (BA), which utilizes efficient bitwise operations and inexpensive data structures to track intra-procedural duas, has been proposed. BA’s RAM memory requirements are restricted to three bit vectors the size of the number of duas. In terms of time complexity, its performance is at least as good as the most efficient previous algorithms and can be up to 100% more efficient. We present BA’s proof of correctness showing that it correctly determines the duas covered during the program execution. |