article

A core calculus for Java exceptions

Authors:

D. Ancona,

G. Lagorio,

E. ZuccaAuthors Info & Claims

ACM SIGPLAN Notices, Volume 36, Issue 11

Pages 16 - 30

https://doi.org/10.1145/504311.504284

Published: 01 October 2001 Publication History

Get Access

Abstract

In this paper we present a simple calculus (called CJE) in ourder to fully investigate the exception mechanism of Java, and in particular its interaction with inheritance, which turns out to be non trivial. Moreover, we show that the type system for the calculus directly dirven by the Java language specification (called FULL) uses too many types, in the sense that there are different types which rpovide exactly the same information. Hence, we obtain from FULL a simplified type system called MIN where equivalent types have been identified. We show that is useful both for type-checking optimization and for clarifying the static semantics of the language. The two type systems are proved to satisfy the subject reduction property

References

[1]

D. Ancona, G. Lagorio, and E. Zucca. A core calculus for Java exceptions (extended abstract), In 2th Intl. Workshop on Formal Techniques for java Programs 2000, June 2000.]]

Google Scholar

[2]

D. Ancona, G. Lagorio, and E. Zucca. Jam: A smooth extension of Java with mixins. In E. Bertino, editor ECO OP'00 - European Conference on Object-Oriented Programming, number 1850 in Lecture Notes in Computer Science, pages 154-178, Berlin, 2000. Springer Verlag.]]

Digital Library

Google Scholar

[3]

D. Ancona, G. Lagorio, and E. Zucca. Symplifying types for a calculus of Java exceptions. Technical report, Dipartimento di Informatica e Scienze dell'Informazione, Universita di Genova, July 2001.]]

Google Scholar

[4]

S. Drossopoulou and S. Eisenbach. Describing the semantics of Java and proving type soundness. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, number 1523 in Lecture Notes in Computer Science, pages 41-82. Springer Verlag, Berlin, 1999.]]

Digital Library

Google Scholar

[5]

S. Drossopoulou and T. Valkevych. Java exceptions throw no surprises. Technical report, Dept. of Computing- Imperial College of Science, Technology and Medicine, March 2000.]]

Google Scholar

[6]

S. Drossopoulou, T. Valkevych, and S. Eisenbach, Java type soundness revisited. Technical report, Dept. of Computing - Imperial College of Science, Technology and Medicine, September 2000.]]

Google Scholar

[7]

J. Gosling, B. Joy, G. Steele, and G. Bracha. The JavaTM Language Specification, Second Edition. Addison-Wesley, 2000.]]

Digital Library

Google Scholar

[8]

A. Igarashi, B. Pierce, and P. Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In ACM Symp. on Object-Oriented Programming: Systems, Languages and Applications 1999, pages 132-146, November 1999.]]

Digital Library

Google Scholar

Cited By

View all

Hutton GWright J(2018)What is the meaning of these constant interruptions?Journal of Functional Programming10.1017/S095679680700636317:6(777-792)Online publication date: 24-Dec-2018
https://dl.acm.org/doi/10.1017/S0956796807006363
Giannini PServetto MZucca E(2016)Coupling catch clauses with local declarationsProceedings of the 18th Workshop on Formal Techniques for Java-like Programs10.1145/2955811.2955817(1-6)Online publication date: 17-Jul-2016
https://dl.acm.org/doi/10.1145/2955811.2955817
Giannini PServetto MZucca EOssowski S(2016)Initialize-and-catchProceedings of the 31st Annual ACM Symposium on Applied Computing10.1145/2851613.2851943(1819-1822)Online publication date: 4-Apr-2016
https://dl.acm.org/doi/10.1145/2851613.2851943
Show More Cited By

Index Terms

A core calculus for Java exceptions
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

A core calculus for Java exceptions
OOPSLA '01: Proceedings of the 16th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications

In this paper we present a simple calculus (called CJE) in ourder to fully investigate the exception mechanism of Java, and in particular its interaction with inheritance, which turns out to be non trivial. Moreover, we show that the type system for the ...
Java bytecode as a typed term calculus
PPDP '02: Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming

We propose a type system for the Java bytecode language, prove the type soundness, and develop a type inference algorithm. In contrast to the existing proposals, our type system yields a typed term calculus similar to type systems of lambda calculi. ...
Java Type Unification with Wildcards
Applications of Declarative Programming and Knowledge Management

With the introduction of Java 5.0 the type system has been extended by parameterized types, type variables, type terms, and wildcards. As a result very complex types can arise. The term

<InlineEquation ID="IEq1"> <InlineMediaObject><ImageObject FileRef="...

Reviews

Reviewer: Arthur Gittleman

The authors present a simple calculus, CJE, to be used to fully investigate the exception mechanism of Java and its interaction with inheritance. They show that the type system for the calculus derived from the Java Language Specification contains different types that provide exactly the same information. They obtain a simplified type system in which equivalent types have been identified. CJE includes all mechanisms for handling exceptions, except the finally clause, which makes no sense in a functional setting. CJE omits fields, constructors, super, and assignment. The calculus has four constructs: method invocation, object creation, and throw and try-catch expressions. A motivating example including an interface and two abstract classes illustrates the complexity of the rules for the compatibility checks of throw clauses and their impact on the type system. After an interesting analysis, the authors conclude that a slight change in the Java specification would noticeably simplify its semantics. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGPLAN Notices Volume 36, Issue 11

11/01/2001

380 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/504311

Issue’s Table of Contents

OOPSLA '01: Proceedings of the 16th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications
October 2001
382 pages
ISBN:1581133359
DOI:10.1145/504282
Conference Chair:
Linda Northrop
Software Engineering Institute
,
Program Chair:
John Vlissides
IBM T.J. Watson Research Center

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: 01 October 2001

Published in SIGPLAN Volume 36, Issue 11

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
416
Total Downloads

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

Reflects downloads up to 19 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Hutton GWright J(2018)What is the meaning of these constant interruptions?Journal of Functional Programming10.1017/S095679680700636317:6(777-792)Online publication date: 24-Dec-2018
https://dl.acm.org/doi/10.1017/S0956796807006363
Giannini PServetto MZucca E(2016)Coupling catch clauses with local declarationsProceedings of the 18th Workshop on Formal Techniques for Java-like Programs10.1145/2955811.2955817(1-6)Online publication date: 17-Jul-2016
https://dl.acm.org/doi/10.1145/2955811.2955817
Giannini PServetto MZucca EOssowski S(2016)Initialize-and-catchProceedings of the 31st Annual ACM Symposium on Applied Computing10.1145/2851613.2851943(1819-1822)Online publication date: 4-Apr-2016
https://dl.acm.org/doi/10.1145/2851613.2851943
Steffen M(2016)A Small-Step Semantics of a Concurrent Calculus with Goroutines and Deferred FunctionsEssays Dedicated to Frank de Boer on Theory and Practice of Formal Methods - Volume 966010.1007/978-3-319-30734-3_26(393-406)Online publication date: 1-Jan-2016
https://dl.acm.org/doi/10.1007/978-3-319-30734-3_26
Johnsen EMai Thuong Tran TOwe OSteffen M(2012)Safe locking for multi-threaded Java with exceptionsThe Journal of Logic and Algebraic Programming10.1016/j.jlap.2011.11.00281:3(257-283)Online publication date: Apr-2012
https://doi.org/10.1016/j.jlap.2011.11.002
Inostroza Pvan der Storm TBoix EGabriel R(2018)JEff: objects for effectProceedings of the 2018 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3276954.3276955(111-124)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276954.3276955
Giannini PServetto MZucca E(2016)Coupling catch clauses with local declarationsProceedings of the 18th Workshop on Formal Techniques for Java-like Programs10.1145/2955811.2955817(1-6)Online publication date: 17-Jul-2016
https://dl.acm.org/doi/10.1145/2955811.2955817
Giannini PServetto MZucca EOssowski S(2016)Initialize-and-catchProceedings of the 31st Annual ACM Symposium on Applied Computing10.1145/2851613.2851943(1819-1822)Online publication date: 4-Apr-2016
https://dl.acm.org/doi/10.1145/2851613.2851943
Zhou XZhang ZZhu YLi YKumar SVahdat AZhao BZheng H(2012)Mirror mirror on the ceilingACM SIGCOMM Computer Communication Review10.1145/2377677.237776142:4(443-454)Online publication date: 13-Aug-2012
https://dl.acm.org/doi/10.1145/2377677.2377761
Bodík PMenache IChowdhury MMani PMaltz DStoica I(2012)Surviving failures in bandwidth-constrained datacentersACM SIGCOMM Computer Communication Review10.1145/2377677.237776042:4(431-442)Online publication date: 13-Aug-2012
https://dl.acm.org/doi/10.1145/2377677.2377760
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