Danicic, Sebastian; Laurence, Michael and Hierons, Robert. 2009. Decidability of Strong Equivalence for Subschemas of a Class of Linear, Free, near-Liberal Program Schemas. Goldsmiths Department of Computing Technical Report, [Article]

Preview

Text (Decidability of Strong Equivalence for Subschemas of a Class of Linear, Free, near-Liberal Program Schemas) lin.f.near.l.pdf - Accepted Version Download (309kB) | Preview

Abstract or Description

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
de�ned 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 de�nes a correct
subschema of S with respect to the �nal 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.
P

Item Type:	Article
Departments, Centres and Research Units:	Computing
Dates:	Date Event 2009 UNSPECIFIED
Funders:	Funding body Funder ID Grant Number EPSRC UNSPECIFIED
Item ID:	2448
Date Deposited:	08 Jan 2010 10:14
Last Modified:	29 Apr 2020 15:27
Peer Reviewed:	Yes, this version has been peer-reviewed.
URI:	https://research.gold.ac.uk/id/eprint/2448

View statistics for this item...

Edit Record (login required)