We identify a class of programs manipulating lists of data items for which
checking functional equivalence and pre/post verification conditions is
decidable. Lists are modeled as data words, (unbounded) sequences of data
values, tagged with symbols from a finite set, over a potentially infinite data
domain that supports only the operations of equality and ordering. First, we
introduce streaming data-word transducers that map input data words to output
data words in a single left-to-right pass in linear time. The transducer uses a
finite set of states, a finite set of variables ranging over data domain, and a
finite set of variables ranging over data words. At every step, it can make
decisions based on the next input symbol, updating its state, remembering the
input data value in its data variables, and updating data-word variables by
concatenating data-word variables and new symbols formed from data variables,
while avoiding duplication. Second, we establish Pspace bounds for the problems
of checking functional equivalence of two streaming transducers, and of
checking whether a streaming transducer satisfies pre/post verification
conditions specified by streaming acceptors over data-words. Third, we identify
a class of imperative programs that manipulate heap-based singly-linked list
data structure, that is expressively equivalent to streaming transducers. Such
programs dynamically modify the heap by adding new nodes and changing
next-pointers of heap-nodes, but are restricted in how the next-pointers can be
used for traversal. Finally, we identify an expressively equivalent fragment of
list-processing functional programs with syntactically restricted recursive
calls. Our results lead to algorithms for checking functional equivalence of
two programs, written possibly in different programming styles, for commonly
used routines such as insert or reverse.