Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language

Mario Bravetti, Adrian Francalanza, Iaroslav Golovanov, Hans Hüttel, Mathias S. Jakobsen, Mikkel K. Kettunen, António Ravara

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

3 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings
EditorsBruno C. Oliveira
Place of PublicationCham
PublisherSpringer
Pages105-124
Number of pages20
ISBN (Electronic)978-3-030-64437-6
ISBN (Print)978-3-030-64436-9
DOIs
Publication statusPublished - 2020
Event18th Asian Symposium on Programming Languages and Systems, APLAS 2020 - Fukuoka, Japan
Duration: 30 Nov 20202 Dec 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer
Volume12470 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference18th Asian Symposium on Programming Languages and Systems, APLAS 2020
CountryJapan
CityFukuoka
Period30/11/202/12/20

Fingerprint

Dive into the research topics of 'Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language'. Together they form a unique fingerprint.

Cite this