In this paper, we present the first fully-automated expected amortised cost analysis of self-adjusting data structures, that is, of randomised splay trees, randomised splay heaps and randomised meldable heaps, which so far have only (semi-) manually been analysed in the literature. Our analysis is stated as a type-and-effect system for a first-order functional programming language with support for sampling over discrete distributions, non-deterministic choice and a ticking operator. The latter allows for the specification of fine-grained cost models. We state two soundness theorems based on two different -- but strongly related -- typing rules of ticking, which account differently for the cost of non-terminating computations. Finally we provide a prototype implementation able to fully automatically analyse the aforementioned case studies.

翻译：本文首次实现了自调整数据结构的全自动期望摊销成本分析，即随机伸展树、随机伸展堆和随机可合并堆的分析，这些结构此前在文献中仅通过（半）人工方式完成分析。我们的分析以类型与效应系统的形式呈现，该系统基于支持离散分布采样、非确定性选择及计时操作符的一阶函数式编程语言。计时操作符支持细粒度成本模型的规范。基于两种不同但紧密关联的计时类型规则，我们提出了两个可靠性定理，这两种规则对非终止计算成本的核算方式存在差异。最后，我们提供了能够全自动分析上述案例的原型实现。