Abstract | ||
---|---|---|
This paper revisits the idea of slicing programs based on their axiomatic semantics, rather than using criteria based on control/data dependencies. We show how the forward propagation of preconditions and the backward propagation of postconditions can be combined in a new slicing algorithm that is more precise than the existing specification-based algorithms. The algorithm is based on (a) a precise test for removable statements, and (b) the construction of a slice graph, a program control flow graph extended with semantic labels and additional edges that “short-circuit” removable commands. It improves on previous approaches in two aspects: it does not fail to identify removable commands; and it produces the smallest possible slice that can be obtained (in a sense that will be made precise). Iteration is handled through the use of loop invariants and variants to ensure termination. The paper also discusses in detail applications of these forms of slicing, including the elimination of (conditionally) unreachable and dead code, and compares them to other related notions. |
Year | DOI | Venue |
---|---|---|
2010 | 10.1007/s00165-011-0196-1 | Software Engineering and Formal Methods |
Keywords | Field | DocType |
removable statement,smallest possible slice,existing specification-based algorithm,precise test,removable command,additional edge,forward propagation,program control flow graph,axiomatic semantics,slice graph,program analysis | Program slicing,Axiomatic semantics,Control flow graph,Computer science,Slicing,Assertion,Algorithm,Theoretical computer science,Loop invariant,Program analysis,Dead code | Conference |
Volume | Issue | ISSN |
24 | 2 | 1433-299X |
ISBN | Citations | PageRank |
978-1-4244-8289-4 | 6 | 0.44 |
References | Authors | |
8 | 4 |
Name | Order | Citations | PageRank |
---|---|---|---|
José Bernardo Barros | 1 | 6 | 0.44 |
Daniela da Cruz | 2 | 9 | 3.19 |
Pedro Rangel Henriques | 3 | 277 | 57.91 |
Jorge Sousa Pinto | 4 | 160 | 23.19 |