Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                          Salle Lions 1, bâtiment C
                           Lundi 16 octobre, 10h30

                               Clément Blaudeau
                                 Inria Paris

            A Conceptual Framework for Safe Object Initialization

An object under initialization does not fulfill its class specification yet
and can be unsafe to use, as it may have uninitialized fields. Yet, it is
sometimes useful to (1) call methods on such a partially initialized object
in order to compute a complex initial value, or (2) to let the object escape
its constructor in order to create mutually recursive objects. However,
inadvertent usage of uninitialized fields can lead to run-time
crashes. Those subtle programming errors are not statically detected by most
modern compilers.

While many other features of object-oriented programming languages have been
thoroughly studied over the years, object initialization lacks a simple,
systematic, and principled treatment. Building on the insights of previous
work, we identify a set of four core principles for safe initialization:
monotonicity, authority, stackability, and scopability. We capture the
essence of the principles with a minimal calculus, Celsius, and show that
the principles give rise to a practical initialization system that strikes a
balance between expressiveness and simplicity. The meta-theory of the system
is entirely mechanized using the Coq proof assistant. We believe that our
approach based on well-identified core principles sheds new light on the
underlying mechanisms ensuring safety and could serve as a basis for
language design when faced with similar challenges.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct:
                     https://bbb.inria.fr/pot-xb8-cq4-y6w