Brunel University Research Archive (BURA) >
University >
Publications >

Please use this identifier to cite or link to this item: http://bura.brunel.ac.uk/handle/2438/5644

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
Publication 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.
Sponsorship: This work was supported by a grant from the Engineering and Physical Sciences Research Council, Grant EP/E002919/1.
URI: http://www.sciencedirect.com/science/article/pii/S1567832610000688
http://bura.brunel.ac.uk/handle/2438/5644
DOI: http://dx.doi.org/10.1016/j.jlap.2010.08.001
ISSN: 1567-8326
Appears in Collections:School of Information Systems, Computing and Mathematics Research Papers
Publications
Computer Science

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.

 


Library (c) Brunel University.    Powered By: DSpace
Send us your
Feedback. Last Updated: September 14, 2010.
Managed by:
Hassan Bhuiyan