Article

Establishing object invariants with delayed types

Authors:

OOPSLA '07: Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems, languages and applications

Pages 337 - 350

https://doi.org/10.1145/1297027.1297052

Published: 21 October 2007 Publication History

Get Access

Abstract

Mainstream object-oriented languages such as C# and Java provide an initialization model for objects that does not guarantee programmer controlled initialization of fields. Instead, all fields are initialized to default values (0 for scalars and null for non-scalars) on allocation. This is in stark contrast to functional languages, where all parts of an allocation are initialized to programmer-provided values. These choices have a direct impact on two main issues: 1) the prevalence of null in object oriented languages (and its general absence in functional languages), and 2) the ability to initialize circular data structures. This paper explores connections between these differing approaches and proposes a fresh look at initialization. Delayed types are introduced to express and formalize prevalent initialization patterns in object-oriented languages.

References

[1]

Mike Barnett, K. Rustan, M. Leino, and Wolfram Schulte. The Spec# Programming System: an Overview. In Proceedings of the Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart devices, volume 3362 of LNCS, 2004.

Google Scholar

[2]

P. Chalin and P. James. Non-null References by Default in Java: Alleviating the Nullity Annotation Burden. In Proceedings of the 21st European Conference on Object-Oriented Programming, 2007.

Digital Library

Google Scholar

[3]

Derek Dreyer, Robert Harper, and Karl Crary. A Type System for Well--Founded Recursion. In Proceedings of the 31st Annual ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages, 2004.

Digital Library

Google Scholar

[4]

Manuel Fähndrich and K. Rustan M. Leino. Declaring and Checking Non-Null Types in an Object-Oriented Language. In Proceedings of the 2003 ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2003, pages 302--312. ACM, November 2003.

Digital Library

Google Scholar

[5]

Manuel Fåhndrich and K. Rustan M. Leino. Heap Monotonic Typestate. In Proceedings of the first International Workshop on Alias Confinement and Ownership (IWACO), July 2003.

Google Scholar

[6]

Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. Region-based Memory Management in Cyclone. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 282--293. ACM, May 2002.

Digital Library

Google Scholar

[7]

Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A notation for detailed design. In HaimKilov, Bernhard Rumpe, and Ian Simmonds, editors, Behavioral Specifications of Businesses and Systems, pages 175--188. Kluwer Academic Publishers, 1999.

Crossref

Google Scholar

[8]

The OCaml Programming Language. http://caml.inria.fr.

Google Scholar

[9]

Claudio Russo. Recursive Structures for Standard ML. In Proceedings of the 2001 International Conference on Functional Programming, pages 50--61, 2001.

Digital Library

Google Scholar

[10]

Frederick Smith, David Walker, and Greg Morrisett. Alias types. In Proceedings of the 14th European Symposium on Programming, volume 1782 of LNCS, pages 366--381. Springer, March 2000.

Digital Library

Google Scholar

[11]

Don Syme. An Alternative Approach to Initializing Mutually Referential Objects. Technical Report MSR-TR-2005-31, Microsoft Research, March 2005.

Google Scholar

[12]

Mads Tofte and Jean-Pierre Talpin. Implementation of the Typed Call-by--Value lambda-Calculus using a Stack of Regions. In Proceedings of the 1994 Symposium on Principles of Programming Languages, pages 188--201, 1994.

Digital Library

Google Scholar

[13]

David Walker and Greg Morrisett. Alias types for recursive data structures. In Proceedings of the 4th Workshop on Types in Compilation, September 2000.

Digital Library

Google Scholar

Cited By

View all

Parkinson MClebsch SWrigstad TBond MLee JPayer H(2024)Reference Counting Deeply Immutable Data Structures with Cycles: An Intellectual AbstractProceedings of the 2024 ACM SIGPLAN International Symposium on Memory Management10.1145/3652024.3665507(131-141)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3652024.3665507
Marron MStorm THirschfeld R(2023)Toward Programming Languages for Reasoning: Humans, Symbolic Systems, and AI AgentsProceedings of the 2023 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3622758.3622895(136-152)Online publication date: 18-Oct-2023
https://dl.acm.org/doi/10.1145/3622758.3622895
Blaudeau CLiu F(2022)A conceptual framework for safe object initialization: a principled and mechanized soundness proof of the Celsius modelProceedings of the ACM on Programming Languages10.1145/35633146:OOPSLA2(729-757)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563314
Show More Cited By

Index Terms

Establishing object invariants with delayed types
1. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Object oriented constructs
      2. Type structures
    2. Program reasoning
      1. Invariants

Recommendations

A conceptual framework for safe object initialization: a principled and mechanized soundness proof of the Celsius model

An object under initialization does not fulfill its class specification yet and can be unsafe to use as it may have uninitialized fields. It can sometimes be useful to call methods on such a partially initialized object in order to compute a complex ...
Establishing object invariants with delayed types
Proceedings of the 2007 OOPSLA conference

Mainstream object-oriented languages such as C# and Java provide an initialization model for objects that does not guarantee programmer controlled initialization of fields. Instead, all fields are initialized to default values (0 for scalars and null ...
On assertion-based encapsulation for object invariants and simulations
Abstract
In object-oriented programming, reentrant method invocations and shared references make it difficult to achieve adequate encapsulation for sound modular reasoning. This tutorial paper surveys recent progress using auxiliary state (ghost fields) to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

OOPSLA '07: Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems, languages and applications

October 2007

728 pages

ISBN:9781595937865

DOI:10.1145/1297027

General Chair:
Richard P. Gabriel
IBM Research, USA
,
Program Chairs:
David F. Bacon
IBM Research, USA
,
Cristina Videira Lopes
University of California, Irvine, USA
,
Guy L. Steele
Sun Labs, USA

ACM SIGPLAN Notices Volume 42, Issue 10
Proceedings of the 2007 OOPSLA conference
October 2007
686 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1297105
Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 October 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

OOPSLA07

Sponsor:

OOPSLA07: ACM SIGPLAN Object Oriented Programming Systems and Applications Conference

October 21 - 25, 2007

Quebec, Montreal, Canada

Acceptance Rates

OOPSLA '07 Paper Acceptance Rate 33 of 156 submissions, 21%;

Overall Acceptance Rate 268 of 1,244 submissions, 22%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

59
Total Citations
View Citations
420
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Parkinson MClebsch SWrigstad TBond MLee JPayer H(2024)Reference Counting Deeply Immutable Data Structures with Cycles: An Intellectual AbstractProceedings of the 2024 ACM SIGPLAN International Symposium on Memory Management10.1145/3652024.3665507(131-141)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3652024.3665507
Marron MStorm THirschfeld R(2023)Toward Programming Languages for Reasoning: Humans, Symbolic Systems, and AI AgentsProceedings of the 2023 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3622758.3622895(136-152)Online publication date: 18-Oct-2023
https://dl.acm.org/doi/10.1145/3622758.3622895
Blaudeau CLiu F(2022)A conceptual framework for safe object initialization: a principled and mechanized soundness proof of the Celsius modelProceedings of the ACM on Programming Languages10.1145/35633146:OOPSLA2(729-757)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563314
Bierhoff K(2022)Wildcards need witness protectionProceedings of the ACM on Programming Languages10.1145/35633016:OOPSLA2(373-394)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563301
Kabir ILi YLhoták O(2020)ιDOT: a DOT calculus with object initializationProceedings of the ACM on Programming Languages10.1145/34282764:OOPSLA(1-28)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428276
Liu FLhoták OBiboudis AGiarrusso POdersky M(2020)A type-and-effect system for object initializationProceedings of the ACM on Programming Languages10.1145/34282434:OOPSLA(1-28)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428243
Banerjee SClapp LSridharan MDumas MPfahl DApel SRusso A(2019)NullAway: practical type-based null safety for JavaProceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3338906.3338919(740-750)Online publication date: 12-Aug-2019
https://dl.acm.org/doi/10.1145/3338906.3338919
Kabir ILhoták OErdweg SOliveira B(2018)κDOT: scaling DOT with mutation and constructorsProceedings of the 9th ACM SIGPLAN International Symposium on Scala10.1145/3241653.3241659(40-50)Online publication date: 17-Sep-2018
https://dl.acm.org/doi/10.1145/3241653.3241659
Brotherston DDietl WLhoták OWu PHack S(2017)Granullar: gradual nullable types for JavaProceedings of the 26th International Conference on Compiler Construction10.1145/3033019.3033032(87-97)Online publication date: 5-Feb-2017
https://dl.acm.org/doi/10.1145/3033019.3033032
Rama GKomondoor R(2017)Detecting Full Initialization Points of Objects to Support Code Refactorings2017 24th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC.2017.17(110-119)Online publication date: Dec-2017
https://doi.org/10.1109/APSEC.2017.17
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

A conceptual framework for safe object initialization: a principled and mechanized soundness proof of the Celsius model

Establishing object invariants with delayed types

On assertion-based encapsulation for object invariants and simulations