A Type System for Reachability and Acyclicity
A Type System for Reachability and Acyclicity
复制标题
可达性和非循环性的类型系统
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
John Michael Potter
中科院分区：
文献类型：
--
作者：
Yi Lu;John Michael Potter
在许多领域，目前，人们对堆环境结构的汇编知识的渴望正在增加。但是，使用整个程序分析的方法在效率和准确性方面都过于弱。本文提出了一种新型的类型系统，该系统通过参考或指示对程序员定义的限制进行了定义的约束，并限制参考周期位于堆的可定义部分之内。此类限制对于程序理解和有关效果和不变性的推理，信息流安全性以及运行时优化和内存管理可能很有用。
The desire for compile-time knowledge about the structure of heap contexts is currently increasing in many areas. However, approaches using whole program analysis are too weak in terms of both efficiency and accuracy. This paper presents a novel type system that enforces programmer-defined constraints on reachability via references or pointers, and restricts reference cycles to be within definable parts of the heap. Such constraints can be useful for program understanding and reasoning about effects and invariants, for information flow security, and for run-time optimizations and memory management.