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. It prevents null pointer dereferencing in a typestate-aware manner and memory leaks and ensures that the intended usage protocol of every object is respected and completed. The type system admits an algorithm that infers the most general usage with respect to a simulation preorder. The type system is implemented in the form of a type checker and a usage inference tool.
Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language / Bravetti M.; Francalanza A.; Golovanov I.; Huttel H.; Jakobsen M.S.; Kettunen M.K.; Ravara A.. - STAMPA. - 12470:(2020), pp. 105-124. (Intervento presentato al convegno 18th Asian Symposium on Programming Languages and Systems, APLAS 2020 tenutosi a Fukuoka, Japan nel November 30-December 2, 2020) [10.1007/978-3-030-64437-6_6].
Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language
Bravetti M.;
2020
Abstract
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. It prevents null pointer dereferencing in a typestate-aware manner and memory leaks and ensures that the intended usage protocol of every object is respected and completed. The type system admits an algorithm that infers the most general usage with respect to a simulation preorder. The type system is implemented in the form of a type checker and a usage inference tool.File | Dimensione | Formato | |
---|---|---|---|
APLAS2020.pdf
accesso aperto
Tipo:
Postprint
Licenza:
Licenza per accesso libero gratuito
Dimensione
661.43 kB
Formato
Adobe PDF
|
661.43 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.