论文标题
使用ACL2建模渐近复杂性
Modeling Asymptotic Complexity Using ACL2
论文作者
论文摘要
渐近复杂性理论提供了一种方法，可以根据执行或使用计算资源的计算步骤数量来表征程序的行为。 我们描述了使用ACL2的工作，以证明通过ACL2中的操作语义嵌入简单命令式编程语言中实现的程序的复杂性属性。 我们同时证明了程序的功能性能及其复杂性。 我们通过描述有关二进制搜索算法的证据来说明我们的方法，并证明它在排序列表上实现了二进制搜索，并且是o（log（log（n）），其中n是列表的长度。
The theory of asymptotic complexity provides an approach to characterizing the behavior of programs in terms of bounds on the number of computational steps executed or use of computational resources. We describe work using ACL2 to prove complexity properties of programs implemented in a simple imperative programming language embedding via an operational semantics in ACL2. We simultaneously prove functional properties of a program and its complexity. We illustrate our approach by describing proofs about a binary search algorithm, proving both that it implements binary search on a sorted list and that it is O(log(n)), where n is the length of the list.
