research-article

Semantic predicate types and approximation for class-based object oriented programming

Authors:

Steffen van Bakel,

Reuben N. S. RoweAuthors Info & Claims

FTfJP '09: Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs

Article No.: 3, Pages 1 - 7

https://doi.org/10.1145/1557898.1557901

Published: 06 July 2009 Publication History

Abstract

We apply the principles of the intersection type discipline to the study of class-based object oriented programs and; our work follows from a similar approach (in the context of Abadi and Cardelli's ς-object calculus) taken by van Bakel and de'Liguoro. We define an extension of Featherweight Java, pFJ, and present a predicate system which we show to be sound and expressive. We also show that our system provides a semantic underpinning for the object oriented paradigm by generalising the concept of approximant from the Lambda Calculus and demonstrating an approximation result: all expressions to which we can assign a predicate have an approximant that satisfies the same predicate. Crucial to this result is the notion of predicate language, which associates a family of predicates with a class.

References

[1]

M. Abadi and L. Cardelli. A Theory Of Objects. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1996.

Digital Library

[2]

E. Albert, P. Arenas, M. Codish, S. Genaim, G. Puebla, and D. Zanardini. Termination Analysis of Java Bytecode. In FMOODS, pp. 2--18, 2008.

Digital Library

[3]

S. van Bakel. Complete restrictions of the Intersection Type Discipline. Theoretical Computer Science, 102(1):135--163, 1992.

Digital Library

[4]

S. van Bakel. Intersection Type Assignment Systems. Theoretical Computer Science, 151(2):385--435, 1995.

Digital Library

[5]

S. van Bakel and U. de'Liguoro. Logical Semantics for the First Order Sigma Calculus. In ICTCS'03, LNCS 2841, pp. 202--215. Springer-Verlag, 2003.

[6]

S. van Bakel and U. de'Liguoro. Logical Semantics for FOb₁<:μ. In ICTCS'05, LNCS 3701, pp. 66--80. Springer-Verlag, 2005.

[7]

S. van Bakel and U. de'Liguoro. Logical Equivalence for Subtyping Object and Recursive Types. Theory of Computing Systems, 42(3):306--348, 2008.

Digital Library

[8]

F. Barbanera and U. de'Liguoro. Type Assignment for Mobile Objects. ENTCS, 104:25--38, 2004.

Digital Library

[9]

H. Barendregt. The Lambda Calculus, Its Syntax and Semantics. North-Holland, 1981.

[10]

H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A Filter Lambda Model and the Completeness of Type Assignment. Journal of Symbolic Logic, 48(4):931--940, 1983.

[11]

L. Bettini, S. Capecchi, and B. Venneri. Featherweight Java with Multi-Methods. In PPPJ, volume 272 of ACM International Conference Proceeding Series, pp. 83--92. ACM, 2007.

Digital Library

[12]

G. Bierman, M. J. Parkinson, and A. Pitts. MJ: An Imperative Core Calculus for Java and Java with Effects. Technical Report 563, University of Cambridge Computer Laboratory, April 2003.

[13]

L. Cardelli. A Semantics of Multiple Inheritance. In Proc. of the international symposium on Semantics of data types, pp. 51--67, 1984, Springer-Verlag.

Digital Library

[14]

L. Cardelli and J. C. Mitchell. Operations on Records. In Proceedings of the fifth international conference on Mathematical foundations of programming semantics, pp. 22--52, Springer-Verlag.

Digital Library

[15]

G. Castagna and B. Pierce. Decidable bounded quantification. In POPL'94, pp. 151--162, 1994.

Digital Library

[16]

M. Coppo and M. Dezani-Ciancaglini. A New Type Assignment for Lambda-Terms. Archive für Mathematischer Logic und Grundlagenforschung, 19:139--156, 1978.

[17]

M. Coppo and M. Dezani-Ciancaglini. An Extension of the Basic Functionality Theory for the λ-Calculus. Notre Dame, Journal of Formal Logic, 21(4):685--693, 1980.

[18]

M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional Characters of Solvable Terms. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 27:45--58, 1981.

[19]

Ugo de'Liguoro. Subtyping in Logical Form. ENTCS, 70(1), 2002.

[20]

M. Dezani-Ciancaglini, D. Mostrous, N. Yoshida, and S. Drossopoulou. Session Types for Object-Oriented Languages. In Proceedings of ECOOP'06, LNCS, pp. 328--352. Springer-Verlag, 2006.

Digital Library

[21]

E. Ernst, K. Ostermann, and W. R. Cook. A Virtual Class Calculus. In POPLŠ06, pp. 270--282. ACM Press, 2006.

Digital Library

[22]

K. Fisher, F. Honsell, and J. C. Mitchell. A Lambda Calculus of Objects and Method Specialization. Nordic J. of Computing, 1(1):3--37, 1994.

Digital Library

[23]

J. Y. Girard. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris VII, 1972.

[24]

J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specification (3rd Edition). Prentice Hall, 2005.

Digital Library

[25]

C. Grothoff. Expressive Type Systems for Object-oriented Languages. PhD thesis, UCLA, 2006.

Digital Library

[26]

A. Igarashi, B. Pierce, and P. Wadler. Featherweight Java: A Minimal Core Calculus for Java and GJ. In ACM Transactions on Programming Languages and Systems (TOPLAS), 23(3), May 2001.

Digital Library

[27]

A. Igarashi and B. C. Pierce. On Inner Classes. In Information and Computation, 2000.

Digital Library

[28]

T. P. Jensen and F. Spoto. Class analysis of object-oriented programs through abstract interpretation. In FoSSaCS, pp. 261--275, 2001.

Digital Library

[29]

F. Logozzo. Automatic inference of class invariants. In VMCAI, pp. 211--222, 2004.

[30]

F. Logozzo. Separate compositional analysis of class-based object-oriented languages. In AMAST, pp. 334--348, 2004.

[31]

F. Logozzo and A. Cortesi. Abstract interpretation and object-oriented programming: Quo vadis? Electr. Notes Theor. Comput. Sci., 131:75--84, 2005.

Digital Library

[32]

J. C. Mitchell. Polymorphic type inference and containment. Inf. Comput., 76(2/3):211--249, 1988.

Digital Library

[33]

J. C. Mitchell. Toward A Typed Foundation for Method Specialization and Inheritance. In POPL '90, pp. 109--124, 1990. ACM.

Digital Library

[34]

B. C. Pierce. Intersection types and bounded polymorphism. In M. Bezem and J. F. Groote, editors, TLCA'93, LNCS 664, pp. 346--360. Springer-Verlag, 1993.

Digital Library

[35]

B. C. Pierce. Bounded quantification is undecidable. Information and Computation, 112(1):131--165, 1994.

Digital Library

[36]

J. C. Reynolds. Towards a theory of type structure. In Symposium on Programming, pp. 408--423, 1974.

Digital Library

[37]

A. Rountev, A. Milanova, and B. G. Ryder. Points-to analysis for java using annotated constraints. In OOPSLA, pp. 43--55, 2001.

Digital Library

[38]

W. Tait. Intensional interpretation of functionals of finite type i. Journal of Symbolic Logic, 32, 2:198--223, 1967.

[39]

C. Wadsworth. The relation between computational and denotational properties for scott's D_∞-models of the lambda-calculus. SIAM J. Comput., 5:488--521, 1976.

[40]

T. Zhao, J. Palsberg, and J. Vitek. Lightweight Confinement for Featherweight Java. In OOPSLAŠ03, pp. 135--148. ACM Press, 2003.

Digital Library

Cited By

Rowe RVan Bakel S(2011)Approximation semantics and expressive predicate assignment for object-oriented programmingProceedings of the 10th international conference on Typed lambda calculi and applications10.5555/2021953.2021974(229-244)Online publication date: 1-Jun-2011
https://dl.acm.org/doi/10.5555/2021953.2021974
Rowe RVan Bakel S(2011)Approximation Semantics and Expressive Predicate Assignment for Object-Oriented ProgrammingTyped Lambda Calculi and Applications10.1007/978-3-642-21691-6_19(229-244)Online publication date: 2011
https://doi.org/10.1007/978-3-642-21691-6_19

Index Terms

Semantic predicate types and approximation for class-based object oriented programming
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Classes and objects
      2. Language types
        Object oriented languages
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Inter-deriving semantic artifacts for object-oriented programming

We present a new abstract machine for Abadi and Cardelli's untyped non-imperative calculus of objects. This abstract machine mechanically corresponds to both the reduction semantics (i.e., small-step operational semantics) and the natural semantics (...
Order-sorted logic programming with predicate hierarchy

Order-sorted logic has been formalized as first-order logic with sorted terms where sorts are ordered to build a hierarchy (called a sort-hierarchy). These sorted logics lead to useful expressions and inference methods for structural knowledge that ...
Semantic Types and Approximation for Featherweight Java

@?We consider semantics for the class-based object-oriented calculus Featherweight Java (without casts) based upon approximation. We also define an intersection type assignment system for this calculus and show that it satisfies subject reduction and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

FTfJP '09: Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs

July 2009

64 pages

ISBN:9781605585406

DOI:10.1145/1557898

Conference Chair:
Anindya Banerjee
IMDEA Software, Spain

Copyright © 2009 ACM.

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]

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 July 2009

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Conference

ECOOP '09

ECOOP '09: European Conference on Object-Oriented Programming

July 6, 2009

Genova, Italy

Acceptance Rates

FTfJP '09 Paper Acceptance Rate 10 of 15 submissions, 67%;

Overall Acceptance Rate 51 of 75 submissions, 68%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
137
Total Downloads

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

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Rowe RVan Bakel S(2011)Approximation semantics and expressive predicate assignment for object-oriented programmingProceedings of the 10th international conference on Typed lambda calculi and applications10.5555/2021953.2021974(229-244)Online publication date: 1-Jun-2011
https://dl.acm.org/doi/10.5555/2021953.2021974
Rowe RVan Bakel S(2011)Approximation Semantics and Expressive Predicate Assignment for Object-Oriented ProgrammingTyped Lambda Calculi and Applications10.1007/978-3-642-21691-6_19(229-244)Online publication date: 2011
https://doi.org/10.1007/978-3-642-21691-6_19

View Options

Get Access

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents