Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language
APLAS(2020)
摘要
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.
更多查看译文
关键词
method safety,types,core,object-oriented
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络