Please use this identifier to cite or link to this item:
Title: Decidability of strong equivalence for subschemas of a class of linear, free, near-liberal program schemas
Authors: Danicic, S
Hierons, RM
Laurence, MR
Keywords: Free and liberal program schemas;Herbrand domain;Program slicing;Linear schemas;Weiser's algorithm
Issue Date: 2011
Publisher: Elsevier Science Inc
Citation: Journal of Logic and Algebraic Programming, 80(2): 92-112, 2011
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. Two schemas are strongly equivalent if they always define the same function from initial states to final states for every interpretation. A subschema of a schema is obtained from a schema by deleting some of its statements. A schema S is liberal if there exists an initial state in the Herbrand domain such that the same term is not generated more than once along any executable path through S. In this paper, we introduce near-liberal schemas, in which this non-repeating condition applies only to terms not having the form g() for a constant function symbol g. Given a schema S that is linear (no function or predicate symbol occurs more than once in S) and a variable v, we compute a set of function and predicate symbols in S which is a subset of those defined by Weiser's slicing algorithm and prove that if for every while predicate q in S and every constant assignment w:=g(); lying in the body of q, no other assignment to w also lies in the body of q, our smaller symbol set defines a correct subschema of S with respect to the final value of v after execution. We also prove that if S is also free (every path through S is executable) and near-liberal, it is decidable which of its subschemas are strongly equivalent to S. For the class of pairs of schemas in which one schema is a subschema of the other, this generalises a recent result in which S was required to be linear, free and liberal.
Description: The article attached is a preprint version of the final published article which can be accessed at the link below. The article title has been changed. For referencing purposes please use the published details. Copyright © 2010 Elsevier B.V. All rights reserved.
ISSN: 1567-8326
Appears in Collections:Publications
Computer Science
Dept of Computer Science Research Papers

Files in This Item:
File Description SizeFormat 
Fulltext.pdf239.99 kBAdobe PDFView/Open

Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.