单遍列表处理程序的计算机验证
Algorithmic Verification of Single-Pass List Processing Programs
摘要：
我们引入了流数据串转换器，其在线性时间中以单次从左到右通过将输入数据串映射到输出数据串。数据字符串是数据值的（无界）序列，标记有有限集合中的符号，在一个潜在的无限数据域上，只支持相等和排序的操作。传感器使用有限的状态集、在数据域上的有限的变量集和在数据串上的有限的变量集。在每一步，它可以根据下一个输入符号做出决定，更新其状态，记住其数据变量中的输入数据值，并通过连接数据串变量和由数据变量形成的新符号来更新数据串变量，同时避免重复。我们建立的问题，检查两个流式传感器的功能等效性，并检查是否流传感器满足前/后验证条件流接收器指定的输入/输出数据串，在PSPACE。我们确定了一类命令和一类函数程序，操纵列表的数据项，可以有效地转换为流数据串换能器。命令式程序通过改变堆节点的下一个指针和添加新节点来动态修改单链堆。主要限制指定了下一个指针如何用于遍历。我们还确定了一个表达等效的函数程序片段，遍历一个列表使用语法限制递归调用。我们的研究结果导致算法的断言检查和检查功能等价的两个程序，写在不同的编程风格，常用的例程，如插入，删除，和反向。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
