Efficient Type-Checking for Amortised Heap-Space Analysis
Efficient Type-Checking for Amortised Heap-Space Analysis
复制标题
DOI：
10.1007/978-3-642-04027-6_24
复制
发表时间：
2009-09
影响因子：
7.5
通讯作者：
M. Hofmann;Dulma Rodriguez
中科院分区：
文献类型：
--
作者：
M. Hofmann;Dulma Rodriguez
在过去的几年里，对程序中资源消耗的预测引起了人们的兴趣。它对许多领域都很重要，特别是嵌入式系统和安全关键系统。分析了实现有限资源消耗的不同方法。其中之一，摊销的复杂性分析的基础上，已经研究了霍夫曼和Jost在2006年的Java类language.In本文中，我们提出了这种类型系统的扩展，包括更一般的子类型和共享关系，使我们能够类型更多的例子。此外，我们描述了一个有限的，注释版本的系统高效的自动类型检查。我们证明了类型检查算法的可靠性和完备性，并展示了它的有效性。
The prediction of resource consumption in programs has gained interest in the last years. It is important for a number of areas, notably embedded systems and safety critical systems. Different approaches to achieve bounded resource consumption have been analysed. One of them, based on an amortised complexity analysis, has been studied by Hofmann and Jost in 2006 for a Java-like language.In this paper we present an extension of this type system consisting of more general subtyping and sharing relations that allows us to type more examples. Moreover we describe efficient automated type-checking for a finite, annotated version of the system. We prove soundness and completeness of the type checking algorithm and show its efficiency.