Characterizing minimal semantics-preserving slices of predicate-linear, free, liberal program schemas

DOI10.1016/J.JLAP.2011.04.009MaRDI QIDQ649588zbMATH OpenOpenAlexFDO

Authors Sebastian Danicic, Robert M. Hierons, Michael R. Laurence

Publication date 2 December 2011

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1705.09615

zbMATH Keywords

program slicingprogram schemasHerbrand domainlinear schemasWeiser's algorithmfree and liberal schemas

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: A program schema defines a class of programs, all of which have identical statement structure, but whose functions and predicates may differ. A schema thus defines an entire class of programs according to how its symbols are interpreted. A subschema of a schema is obtained from a schema by deleting some of its statements. We prove that given a schema $S$ which is predicate-linear, free and liberal, such that the true and false parts of every if predicate satisfy a simple additional condition, and a slicing criterion defined by the final value of a given variable after execution of any program defined by $S$, the minimal subschema of $S$ which respects this slicing criterion contains all the function and predicate symbols `needed' by the variable according to the data dependence and control dependence relations used in program slicing, which is the symbol set given by Weiser's static slicing algorithm. Thus this algorithm gives predicate-minimal slices for classes of programs represented by schemas satisfying our set of conditions. We also give an example to show that the corresponding result with respect to the slicing criterion defined by termination behaviour is incorrect. This complements a result by the authors in which $S$ was required to be function-linear, instead of predicate-linear.

Recommendations

• Characterizing minimal semantics-preserving slices of function-linear, free, liberal program schemas
• On the computational complexity of dynamic slicing problems for program schemas
• Decidability of strong equivalence for subschemas of a class of linear, free, near-liberal program schemas
• Program Slicing
• A trajectory-based strict semantics for program slicing

Cites work

• scientific article; zbMATH DE number 3550181 (Why is no real title available?)
• scientific article; zbMATH DE number 3229496 (Why is no real title available?)
• An algorithm deciding functional equivalence in a new class of program schemes
• Characterizing minimal semantics-preserving slices of function-linear, free, liberal program schemas
• Decidability of strong equivalence for subschemas of a class of linear, free, near-liberal program schemas
• Equivalence of conservative, free, linear program schemas is decidable
• Equivalence of linear, free, liberal, structured program schemas is decidable in polynomial time
• On Ianov's Program Schemata
• On the Computational Complexity of Program Scheme Equivalence
• Random time evolution and direct integrals: Constants of the motion and the mass operator
• Theory of program structures: Schemes, semantics, verification
• Translating Program Schemas to While-Schemas

Cited in

(3)

• Decidability of strong equivalence for subschemas of a class of linear, free, near-liberal program schemas
• On the computational complexity of dynamic slicing problems for program schemas
• Characterizing minimal semantics-preserving slices of function-linear, free, liberal program schemas

This page was built for publication: Characterizing minimal semantics-preserving slices of predicate-linear, free, liberal program schemas

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q649588)