A model for Java']Java with wildcards

被引：0
|
作者：
Cameron, Nicholas [1 ]
Drossopoulou, Sophia [1 ]
Ernst, Erik [2 ]
机构：
[1] Imperial Coll London, London SW7 2AZ, England
[2] Univ Aarhus, DK-8000 Aarhus C, Denmark
来源：
ECOOP 2008 - OBJECT-ORIENTED PROGRAMMING, PROCEEDINGS | 2008年 / 5142卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Wildcards are a complex and subtle part of the Java type system, present since version 5.0. Although there have been various formalisations and partial type soundness results concerning wildcards, to the best of our knowledge, no system that includes all the key aspects of Java wildcards has been proven type sound. This paper establishes that Java wildcards are type sound. We describe a new formal model based on explicit existential types whose pack and unpack operations are handled implicitly, and prove it type sound. Moreover, we specify a translation from a subset of Java to our formal model, and discuss how several interesting aspects of the Java type system are handled.
引用
收藏
页码：2 / +
页数：4
相关论文
共 50 条
  • [21] Java']Java RMI performance and object model interoperability: experiments with Java']Java/HPC++
    Breg, F
    Diwan, S
    Villacis, J
    Balasubramanian, J
    Akman, E
    Gannon, D
    [J]. CONCURRENCY-PRACTICE AND EXPERIENCE, 1998, 10 (11-13): : 941 - 955
  • [22] An authentication server in Java']Java - Implementation of an encryption framework model and DES algorithm in Java']Java
    de Almeida, LB
    Godoy, W
    Kovaleski, JL
    [J]. ITS '98 PROCEEDINGS - SBT/IEEE INTERNATIONAL TELECOMMUNICATIONS SYMPOSIUM, VOLS 1 AND 2, 1998, : 627 - 631
  • [23] A quality assessment model for Java']Java code
    Benedicenti, L
    Wang, VW
    Paranjape, R
    [J]. IEEE CCEC 2002: CANADIAN CONFERENCE ON ELECTRCIAL AND COMPUTER ENGINEERING, VOLS 1-3, CONFERENCE PROCEEDINGS, 2002, : 687 - 690
  • [24] A model for slicing JAVA']JAVA programs hierarchically
    Li, BX
    Fan, XC
    Pang, J
    Zhao, JJ
    [J]. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2004, 19 (06) : 848 - 858
  • [25] Model checking the Java']Java metalocking algorithm
    Basu, Samik
    Smolka, Scott A.
    [J]. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2007, 16 (03) : C1 - C35
  • [26] Making the Java']Java Memory Model Safe
    Lochbihler, Andreas
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2013, 35 (04):
  • [27] Model checking programs with Java']Java PathFinder
    Visser, W
    Mehlitz, P
    [J]. MODEL CHECKING SOFTWARE, PROCEEDINGS, 2005, 3639 : 27 - 27
  • [28] A Type Graph Model for Java']Java Programs
    Rensink, Arend
    Zambon, Eduardo
    [J]. FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, PROCEEDINGS, 2009, 5522 : 237 - 242
  • [29] Empowerment model of biomass in west java']java
    Mulyana, C.
    Fitriani, N. I.
    Saad, A.
    Yuliah, Y.
    [J]. INTERNATIONAL CONFERENCE ON BIOMASS: TECHNOLOGY, APPLICATION, AND SUSTAINABLE DEVELOPMENT, 2016, 2017, 65
  • [30] Model generation for distributed Java']Java programs
    Boulifa, R
    Madelaine, E
    [J]. SCIENTIFIC ENGINEERING OF DISTRIBUTED JAVA APPLICATIONS, 2004, 2952 : 139 - 152
12345