Practical pluggable types for java
Practical pluggable types for java
复制标题
java 实用的可插入类型
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Michael D. Ernst
中科院分区：
文献类型：
--
作者：
Matthew M. Papi;Mahmood Ali;Telmo Luis Correa;J. Perkins;Michael D. Ernst
本文介绍了Checker框架，它支持以向后兼容的方式将可插拔类型系统添加到Java语言中。类型系统设计器定义类型限定符及其语义，而编译器插件强制执行这些语义。程序员可以在他们的程序中编写类型限定符，并使用插件来检测或防止错误。Checker框架对于希望编写无错误代码的程序员和希望评估和部署其类型系统的类型系统设计人员都很有用。
Checker框架包括用于表示类型限定符的新Java语法；用于编写类型检查规则的声明性和过程性机制；以及对流敏感的本地类型限定符推理和对类型和限定符的多态的支持。Checker框架与Java语言和工具集完美集成。
我们已经通过编写5个检查器并在超过600K行的现有代码上运行它们来评估Checker框架。检验员发现了真正的错误，然后确认修复的代码中没有进一步的错误。这些案例研究还揭示了类型系统本身。
This paper introduces the Checker Framework, which supports adding pluggable type systems to the Java language in a backward-compatible way. A type system designer defines type qualifiers and their semantics, and a compiler plug-in enforces the semantics. Programmers can write the type qualifiers in their programs and use the plug-in to detect or prevent errors. The Checker Framework is useful both to programmers who wish to write error-free code, and to type system designers who wish to evaluate and deploy their type systems.
The Checker Framework includes new Java syntax for expressing type qualifiers; declarative and procedural mechanisms for writing type-checking rules; and support for flow-sensitive local type qualifier inference and for polymorphism over types and qualifiers. The Checker Framework is well-integrated with the Java language and toolset.
We have evaluated the Checker Framework by writing 5 checkers and running them on over 600K lines of existing code. The checkers found real errors, then confirmed the absence of further errors in the fixed code. The case studies also shed light on the type systems themselves.