Computer Science – Programming Languages
Scientific paper
2010-07-28
Computer Science
Programming Languages
Scientific paper
We introduce streaming data string transducers that map input data strings to output data strings in a single left-to-right pass in linear time. Data strings are (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. The transducer uses a finite set of states, a finite set of variables ranging over the data domain, and a finite set of variables ranging over data strings. 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-string variables by concatenating data-string variables and new symbols formed from data variables, while avoiding duplication. We establish that 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 input/output data-strings, are in PSPACE. We identify a class of imperative and a class of functional programs, manipulating lists of data items, which can be effectively translated to streaming data-string transducers. The imperative programs dynamically modify a singly-linked heap by changing next-pointers of heap-nodes and by adding new nodes. The main restriction specifies how the next-pointers can be used for traversal. We also identify an expressively equivalent fragment of functional programs that traverse a list using syntactically restricted recursive calls. Our results lead to algorithms for assertion checking and for checking functional equivalence of two programs, written possibly in different programming styles, for commonly used routines such as insert, delete, and reverse.
Alur Rajeev
Cerny Pavol
No associations
LandOfFree
Algorithmic Verification of Single-Pass List Processing Programs does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Algorithmic Verification of Single-Pass List Processing Programs, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Algorithmic Verification of Single-Pass List Processing Programs will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-74227