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

doi:10.1007/978-3-030-64437-6_6

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

NOVALincs

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

5 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 language	English
Title of host publication	Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings
Editors	Bruno C. Oliveira
Place of Publication	Cham
Publisher	Springer
Pages	105-124
Number of pages	20
ISBN (Electronic)	978-3-030-64437-6
ISBN (Print)	978-3-030-64436-9
DOIs	https://doi.org/10.1007/978-3-030-64437-6_6
Publication status	Published - 2020
Event	18th Asian Symposium on Programming Languages and Systems, APLAS 2020 - Fukuoka, Japan Duration: 30 Nov 2020 → 2 Dec 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publisher	Springer
Volume	12470 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	18th Asian Symposium on Programming Languages and Systems, APLAS 2020
Country/Territory	Japan
City	Fukuoka
Period	30/11/20 → 2/12/20

Access to Document

10.1007/978-3-030-64437-6_6

Cite this

Bravetti, M., Francalanza, A., Golovanov, I., Hüttel, H., Jakobsen, M. S., Kettunen, M. K., & Ravara, A. (2020). Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language. In B. C. Oliveira (Ed.), Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings (pp. 105-124). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12470 LNCS). Springer. https://doi.org/10.1007/978-3-030-64437-6_6

Bravetti, Mario ; Francalanza, Adrian ; Golovanov, Iaroslav et al. / Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language. Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings. editor / Bruno C. Oliveira. Cham : Springer, 2020. pp. 105-124 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{cd30de0e128945dc82b92874f4a67456,

title = "Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language",

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.",

author = "Mario Bravetti and Adrian Francalanza and Iaroslav Golovanov and Hans H{\"u}ttel and Jakobsen, {Mathias S.} and Kettunen, {Mikkel K.} and Ant{\'o}nio Ravara",

note = "info:eu-repo/grantAgreement/EC/H2020/778233/EU# info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDB%2F04516%2F2020/PT# UK EPSRC grant EP/K034413/1 (ABCD). ; 18th Asian Symposium on Programming Languages and Systems, APLAS 2020 ; Conference date: 30-11-2020 Through 02-12-2020",

year = "2020",

doi = "10.1007/978-3-030-64437-6_6",

language = "English",

isbn = "978-3-030-64436-9",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "105--124",

editor = "Oliveira, {Bruno C.}",

booktitle = "Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings",

address = "Netherlands",

}

Bravetti, M, Francalanza, A, Golovanov, I, Hüttel, H, Jakobsen, MS, Kettunen, MK & Ravara, A 2020, Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language. in BC Oliveira (ed.), Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12470 LNCS, Springer, Cham, pp. 105-124, 18th Asian Symposium on Programming Languages and Systems, APLAS 2020, Fukuoka, Japan, 30/11/20. https://doi.org/10.1007/978-3-030-64437-6_6

Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language. / Bravetti, Mario; Francalanza, Adrian; Golovanov, Iaroslav et al.
Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings. ed. / Bruno C. Oliveira. Cham: Springer, 2020. p. 105-124 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12470 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

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

AU - Bravetti, Mario

AU - Francalanza, Adrian

AU - Golovanov, Iaroslav

AU - Hüttel, Hans

AU - Jakobsen, Mathias S.

AU - Kettunen, Mikkel K.

AU - Ravara, António

N1 - info:eu-repo/grantAgreement/EC/H2020/778233/EU# info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDB%2F04516%2F2020/PT# UK EPSRC grant EP/K034413/1 (ABCD).

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85097642531&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-64437-6_6

DO - 10.1007/978-3-030-64437-6_6

M3 - Conference contribution

AN - SCOPUS:85097642531

SN - 978-3-030-64436-9

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 105

EP - 124

BT - Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings

A2 - Oliveira, Bruno C.

PB - Springer

CY - Cham

T2 - 18th Asian Symposium on Programming Languages and Systems, APLAS 2020

Y2 - 30 November 2020 through 2 December 2020

ER -

Bravetti M, Francalanza A, Golovanov I, Hüttel H, Jakobsen MS, Kettunen MK et al. Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language. In Oliveira BC, editor, Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings. Cham: Springer. 2020. p. 105-124. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-64437-6_6

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

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this