A program P is data independent with respect to a data type X iff it
does
not use any operations and predicates involving values of type X other
than equality tests. It is also allowed to input, output and
nondeterministically
choose values of type X, as well as store them and copy them within its
variables. When P is data independent with respect to X, it is
parameterised
by X. In other words, any concrete data type can be instantiated for X
in P.
Given a specification S and a program P which are data independent
with
respect to a data type X, our main results on data independence enable
the problem of verifying whether S is satisfied by P for all instances
of X to be reduced to verifying the satisfaction for a finite number of
finite instances. The body of research by which such results are proved
is a semantic study of data independence consisting of symbolic
operational
semantics, logical relations, and symmetry elimination. Most of our
research
on data independence so far has been in terms of the CSP formalism.
The basic part of the work can be found in Section 15.2 of "The
Theory and Practice" book by A. W. Roscoe (available
electronically in our books
section) and, in more detail, in Lazic's
thesis.
There also are papers on the extension by arrays in the context
of determinism checking, and on the extension by generalised predicate
symbols (see the group's publications
page).
