Please use this identifier to cite or link to this item:
Full metadata record
DC FieldValueLanguage
dc.contributor.authorDanicic, S-
dc.contributor.authorHierons, RM-
dc.contributor.authorLaurence, MR-
dc.identifier.citationJournal of Logic and Algebraic Programming, 80(2): 92-112, 2011en_US
dc.descriptionThe 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.en_US
dc.description.abstractA 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.en_US
dc.description.sponsorshipThis work was supported by a grant from the Engineering and Physical Sciences Research Council, Grant EP/E002919/1.en_US
dc.publisherElsevier Science Incen_US
dc.subjectFree and liberal program schemasen_US
dc.subjectHerbrand domainen_US
dc.subjectProgram slicingen_US
dc.subjectLinear schemasen_US
dc.subjectWeiser's algorithmen_US
dc.titleDecidability of strong equivalence for subschemas of a class of linear, free, near-liberal program schemasen_US
dc.typeResearch Paperen_US
pubs.organisational-data/Brunel/Brunel (Active)-
pubs.organisational-data/Brunel/Brunel (Active)/School of Info. Systems, Comp & Maths-
pubs.organisational-data/Brunel/Research Centres-
pubs.organisational-data/Brunel/Research Centres/CIKM-
pubs.organisational-data/Brunel/School of Information Systems, Computing and Mathematics-
pubs.organisational-data/Brunel/School of Information Systems, Computing and Mathematics/CIKM-
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.