Ownership, encapsulation and the disjointness of type and effect

被引：42

作者：

Clarke, D ^{[1
]}

Drossopoulou, S

机构：

[1] Univ Utrecht, Inst Informat & Comp Sci, Utrecht, Netherlands

[2] Univ London Imperial Coll Sci Technol & Med, Dept Comp, London, England

来源：

ACM SIGPLAN NOTICES | 2002年 / 37卷 / 11期

关键词：

languages; theory; ownership types; encapsulation; aliasing; type-and-effects systems;

D O I：

10.1145/583854.582447

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Ownership types provide a statically enforceable notion of object-level encapsulation. We extend ownership types with computational effects to support reasoning about object-oriented programs. The ensuing system provides both access control and effects reporting. Based on this type system; we codify two formal systems for reasoning about aliasing and the disjointness of computational effects. The first can be used to prove that evaluation of two expressions will never lead to aliases, while the latter can be used to show the non-interference of two expressions.

引用

页码：292 / 310

页数：19