Decidability of Strong Equivalence for Subschemas of a Class of Linear, Free, near-Liberal Program Schemas

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]

[img]
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:

DateEvent
2009UNSPECIFIED

Funders:

Funding bodyFunder IDGrant Number
EPSRCUNSPECIFIED

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 Edit Record (login required)