Behavioural types for memory and method safety in a core object-oriented language

DOI10.1007/978-3-030-64437-6_6MaRDI QIDQ2038074zbMATH OpenOpenAlexFDO

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

Publication date 8 July 2021

Full work available at URL https://arxiv.org/abs/2002.12793

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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

Recommendations

• Static Analysis
• A denotational approach for type-checking in object-oriented programming languages
• Stateful Behavioral Types for Active Objects
• A type-based complexity analysis of object oriented programs
• scientific article; zbMATH DE number 1760051

Cited in

(4)

• Practical void safety
• Avoid a void: The eradication of null dereferencing
• Masked types for sound object initialization
• Static Analysis

This page was built for publication: Behavioural types for memory and method safety in a core object-oriented language

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2038074)