核心面向对象语言中内存和方法安全的行为类型
Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language
摘要：
我们提出了一个基于类型的分析，确保内存安全和对象协议完成的Java类语言蒙戈。对象被标注了方法调用的可接受序列的用法、类似于类型状态的规范。该分析将使用检查与静态检查结合在一起，使用检查控制方法被调用的顺序，静态检查确定引用是否可能包含空值。该分析防止了空指针解引用和内存泄漏，并确保每个对象的预期使用协议得到遵守和完成。类型系统以类型检查器的形式实现。
英文摘要：
We present a type-based analysis ensuring memory safety and object protocol completion in the Java-like language Mungo. Objects are annotated with usages, typestates-like specifications of the admissible sequences of method calls. The analysis entwines usage checking, controlling the order in which methods are called, with a static check determining whether references may contain null values. The analysis prevents null pointer dereferencing and memory leaks and ensures that the intended usage protocol of every object is respected and completed. The type system has been implemented in the form of a type checker.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
