Publication

A Type-and-Effect System for Object Initialization

Abstract

Every newly created object goes through several initialization states: starting from a state where all fields are uninitialized until all of them are assigned. Any operation on the object during its initialization process, which usually happens in the constructor via \emph{this}, has to observe the initialization states of the object for correctness, i.e.~only initialized fields may be used. Checking safe usage of \emph{this} statically, without manual annotation of initialization states in source code, is a challenge, due to aliasing and virtual method calls on \emph{this}. Mainstream languages either do not check initialization errors, like Java, C++, Scala, or they defend against them by not supporting useful initialization patterns, such as Swift. In parallel, past research has shown that safe initialization can be achieved for varying degrees of expressiveness but by sacrificing syntactic simplicity. We approach the problem by upholding \emph{local reasoning} of initialization which avoids whole-program analysis, and we achieve \emph{typestate polymorphism} via subtyping. On this basis, we put forward a novel type-and-effect system that can effectively ensure initialization safety while allowing flexible initialization patterns with almost zero annotation burden.

About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.
Related concepts (32)
Type system
In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type (for example, integer, floating point, string) to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer program, such as variables, expressions, functions, or modules. A type system dictates the operations that can be performed on a term. For variables, the type system determines the allowed values of that term.
Object lifetime
In object-oriented programming (OOP), the object lifetime (or life cycle) of an object is the time between an object's creation and its destruction. Rules for object lifetime vary significantly between languages, in some cases between implementations of a given language, and lifetime of a particular object may vary from one run of the program to another. In some cases, object lifetime coincides with variable lifetime of a variable with that object as value (both for static variables and automatic variables), but in general, object lifetime is not tied to the lifetime of any one variable.
Virtual method table
In computer programming, a virtual method table (VMT), virtual function table, virtual call table, dispatch table, vtable, or vftable is a mechanism used in a programming language to support dynamic dispatch (or run-time method binding). Whenever a class defines a virtual function (or method), most compilers add a hidden member variable to the class that points to an array of pointers to (virtual) functions called the virtual method table.
Show more
Related publications (47)

Electroadhesive gripping system and method for gripping an object

Herbert Shea, Vito Cacucciolo, Krishna Manaswi Digumarti

An electroadhesive gripping system and a method for gripping and manipulating an object are disclosed. The invention provides a novel approach particularly useful to pick fabrics or otherwise flat and flexible objects including a method relying on electroa ...
2023

The company town palimpsest: space, life and politics in Dalmine, Italy

Anna Karla De Almeida Milani

This article proposes a reflection on the company towns’ actual conditions, presenting as a case study an up-to-date and articulated reconstruction of the conditions of habitability in Dalmine, Italy. The research strives on the phenomenon of company towns ...
Marsilio2022

Wrist-driven passive grasping: interaction-based trajectory adaption with a compliant anthropomorphic hand

Josephine Anna Eleanor Hughes, Kieran Daniel Gilday

The structure of the human musculo-skeletal systems shows complex passive dynamic properties, critical for adaptive grasping and motions. Through wrist and arm actuation, these passive dynamic properties can be exploited to achieve nuanced and diverse envi ...
IOP Publishing Ltd2021
Show more
Related MOOCs (22)
Projet de programmation en java
The purpose of this MOOC is to offer a complementary capstone project to our existing MOOCs in introduction to programming. This will offer the students the possibility to both stabilize the already a
Introduction to Object-Oriented Programming in Java
Le cours suivi propose une introduction aux concepts de base de la programmation orientée objet tels que : encapsulation et abstraction, classes/objets, attributs/méthodes, héritage, polymorphisme, ..
Parallelism and Concurrency
(merge of parprog1, scala-reactive, scala-spark-big-data)
Show more

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.