无界尺寸与任意高度跳表的可判定理论

本文提出了任意高度跳表的理论，并证明了无量词公式的可满足性问题的可判定性。跳表是一种命令式软件数据结构，它通过在内存中维护若干层有序的单链表来实现集合，其中每一层都是其较低层的子表。跳表在实践中被广泛使用，因为它们提供与平衡二叉树相当的性能，并且可以更高效地实现。为了实现这种性能，大多数实现会动态增加高度（层数）。由于动态尺寸（节点数）以及不同层之间的共享，跳表很难进行推理。此外，对动态高度的推理增加了处理任意多层的挑战。本文的第一个贡献是理论 TSL，它允许表达任意高度跳表的堆内存布局。第二个贡献是无量词 TSL 公式的可满足性问题的判定过程。最后一个贡献是利用该判定过程展示了一个实用跳表实现的形式化验证。