Article

Trace effects and object orientation

Author:

Christian SkalkaAuthors Info & Claims

PPDP '05: Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming

Pages 139 - 150

https://doi.org/10.1145/1069774.1069787

Published: 11 July 2005 Publication History

Abstract

Trace effects are statically generated program abstractions, that can be model checked for verification of assertions in a temporal program logic. In this paper we develop a type and effect analysis for obtaining trace effects of Object Oriented programs in Featherweight Java. We observe that the analysis is significantly complicated by the interaction of trace behavior with inheritance and other Object Oriented features, particularly overridden methods, dynamic dispatch, and downcasting. We propose an expressive type and effect inference algorithm, combining polymorphism and subtyping/subeffecting constraints, to obtain a flexible trace effect analysis in an Object Oriented setting.

References

[1]

Martín Abadi and Cédric Fournet. Access control based on execution history. In Proceedings of the 10th Annual Network and Distributed System Security Symposium (NDSS'03), feb 2003.

[2]

Rajeev Alur, Pavol Cerny, P. Madhusudan, and Wonhong Nam. Synthesis of interface specifications for java classes. In POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of programming languages, pages 98--109. ACM Press, 2005.

Digital Library

[3]

T. Amtoft, F. Nielson, and H. R. Nielson. Type and Effect Systems. Imperial College Press, 1999.

[4]

Thomas Ball and Sriram K. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN, pages 113--130, 2000.

Digital Library

[5]

Massimo Bartoletti, Pierpaolo Degano, and Gian Luigi Ferrari. Policy framings for access control. In WITS '05: Proceedings of the 2005 workshop on Issues in the theory of security, pages 5--11. ACM Press, 2005.

Digital Library

[6]

F. Besson, T. Jensen, D. Le Métayer, and T. Thorn. Model checking security properties of control flow graphs. J. Computer Security, 9:217--250, 2001.

Digital Library

[7]

Frédéric Besson, Thomas de Grenier de Latour, and Thomas Jensen. Secure calling contexts for stack inspection. In Proceedings of the Fourth ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'02), pages 76--87. ACM Press, 2002.

Digital Library

[8]

Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, Jonathan Eifrig, Scott F. Smith, Valery Trifonov, Gary T. Leavens, and Benjamin C. Pierce. On binary methods. Theory and Practice of Object Systems, 1(3):221--242, 1995.

Digital Library

[9]

O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification on infinite structures. In S. Smolka J. Bergstra, A. Pons, editor, Handbook on Process Algebra. North-Holland, 2001.

[10]

Robert Cartwright and Mike Fagan. Soft typing. In Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, pages 278--292. ACM Press, 1991.

Digital Library

[11]

Hao Chen and David Wagner. MOPS: an infrastructure for examining security properties of software. In Proceedings of the 9th ACM Conference on Computer and Communications Security, pages 235--244, Washington, DC, November~18--22, 2002.

Digital Library

[12]

Thomas Colcombet and Pascal Fradet. Enforcing trace properties by program transformation. In 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 54--66, 2000.

Digital Library

[13]

Luis Damas and Robin Milner. Principal type-schemes for functional programs. In ACM Symposium on Principles of Programming Languages (POPL), pages 207--212, 1982.

Digital Library

[14]

Jonathan Eifrig, Scott Smith, and Valery Trifonov. Type inference for recursively constrained types and its application to OOP. In Mathematical Foundations of Programming Semantics, volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 1995.

[15]

Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. Flow-Sensitive Type Qualifiers. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 1--12, Berlin, Germany, June 2002.

Digital Library

[16]

Gerard J. Holzmann and Margaret H. Smith. Software model checking: extracting verification models from source code. Software Testing, Verification & Reliability, 11(2):65--79, 2001.

[17]

Atsushi Igarashi and Naoki Kobayashi. Resource usage analysis. In Conference Record of POPL'02: The 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 331--342, Portland, Oregon, January 2002.

Digital Library

[18]

Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst., 23(3):396--450, 2001.

Digital Library

[19]

T. Jensen, D. Le Métayer, and T. Thorn. Verification of control flow based security properties. In Proceedings of the 1999 IEEE Symposium on Security and Privacy, 1999.

[20]

P. J. Stuckey K. Marriott and M. Sulzmann. Resource usage verification. In Proc. of First Asian Programming Languages Symposium, APLAS 2003, 2003.

[21]

Francesco Logozzo. Separate compositional analysis of class-based object-oriented languages. In Proceedings of the 10th International Conference on Algebraic Methodology And Software Technology (AMAST'2004), volume 3116 of Lectures Notes in Computer Science, pages 332--346. Springer-Verlag, July 2004.

[22]

Yitzhak Mandelbaum, David Walker, and Robert Harper. An effective theory of type refinements. In Proceedings of the the Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP'03), Uppsala, Sweden, August 2003.

Digital Library

[23]

Fred B. Schneider. Enforceable security policies. Information and System Security, 3(1):30--50, 2000.

Digital Library

[24]

Christian Skalka and Scott Smith. History effects and verification. In Asian Programming Languages Symposium, number 3302 in Lecture Notes in Computer Science. Springer, November 2004.

[25]

Christian Skalka, Scott Smith, and David Van Horn. A type and effect system for flexible abstract interpretation of Java. In Proceedings of the ACM Workshop on Abstract Interpretation of Object Oriented Languages, Electronic Notes in Theoretical Computer Science, January 2005.

Digital Library

[26]

B. Steffen and O. Burkart. Model checking for context-free processes. In CONCUR'92, Stony Brook (NY), volume 630 of Lecture Notes in Computer Science (LNCS), pages 123--137, Heidelberg, Germany, 1992. Springer-Verlag.

Digital Library

[27]

Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. In Seventh Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, pages 162--173, Los Alamitos, California, 1992. IEEE Computer Society Press.

[28]

Valery Trifonov and Scott Smith. Subtyping constrained types. In Proceedings of the Third International Static Analysis Symposium, volume 1145, pages 349--365. Springer Verlag, 1996.

Digital Library

[29]

David Walker. A type system for expressive security policies. In Conference Record of POPL'00: The 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 254--267, Boston, Massachusetts, January 2000.

Digital Library

Cited By

de Ferro CCogumbreiro TMartins F(2023)Shelley: A Framework for Model Checking Call Ordering on Hierarchical SystemsCoordination Models and Languages10.1007/978-3-031-35361-1_5(93-114)Online publication date: 15-Jun-2023
https://doi.org/10.1007/978-3-031-35361-1_5
Skalka CDarais DJaeger TCapobianco F(2020)Types and Abstract Interpretation for Authorization Hook Advice2020 IEEE 33rd Computer Security Foundations Symposium (CSF)10.1109/CSF49147.2020.00018(139-152)Online publication date: Jun-2020
https://doi.org/10.1109/CSF49147.2020.00018
Heidegger PThiemann P(2011)A heuristic approach for computing effectsProceedings of the 49th international conference on Objects, models, components, patterns10.5555/2025896.2025908(147-162)Online publication date: 28-Jun-2011
https://dl.acm.org/doi/10.5555/2025896.2025908
Show More Cited By

Index Terms

Trace effects and object orientation
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Polymorphism
      2. Language types
        Object oriented languages

Recommendations

Types and trace effects for object orientation

Trace effects are statically generated program abstractions, that can be model checked for verification of assertions in a temporal program logic. In this paper we develop a type and effect analysis for obtaining trace effects of Object Oriented ...
ML^F for everyone (users, implementers, and designers)
ML '07: Proceedings of the 2007 workshop on Workshop on ML

ML^F is an alternative to ML that permits second-order polymorphism as in System F but retains (partial) type inference a la ML. Type annotations are requested only on parameters of functions that are used polymorphically. Type abstractions and type ...
System F with coercion constraints
CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

We present a second-order λ-calculus with coercion constraints that generalizes a previous extension of System F with parametric coercion abstractions by allowing multiple but simultaneous type and coercion abstractions, as well as recursive coercions ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PPDP '05: Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming

July 2005

260 pages

ISBN:1595930906

DOI:10.1145/1069774

General Chair:
Pedro Barahona
Universidade Nova de Lisboa, Portugal
,
Program Chair:
Amy Felty
University of Ottawa, Canada

Copyright © 2005 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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 July 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PPDP05

Sponsor:

PPDP05: Principles and Practice of Declarative Programming 2005

July 11 - 13, 2005

Lisbon, Portugal

Acceptance Rates

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
213
Total Downloads

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

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

de Ferro CCogumbreiro TMartins F(2023)Shelley: A Framework for Model Checking Call Ordering on Hierarchical SystemsCoordination Models and Languages10.1007/978-3-031-35361-1_5(93-114)Online publication date: 15-Jun-2023
https://doi.org/10.1007/978-3-031-35361-1_5
Skalka CDarais DJaeger TCapobianco F(2020)Types and Abstract Interpretation for Authorization Hook Advice2020 IEEE 33rd Computer Security Foundations Symposium (CSF)10.1109/CSF49147.2020.00018(139-152)Online publication date: Jun-2020
https://doi.org/10.1109/CSF49147.2020.00018
Heidegger PThiemann P(2011)A heuristic approach for computing effectsProceedings of the 49th international conference on Objects, models, components, patterns10.5555/2025896.2025908(147-162)Online publication date: 28-Jun-2011
https://dl.acm.org/doi/10.5555/2025896.2025908
Heidegger PThiemann P(2011)A Heuristic Approach for Computing EffectsObjects, Models, Components, Patterns10.1007/978-3-642-21952-8_12(147-162)Online publication date: 2011
https://doi.org/10.1007/978-3-642-21952-8_12
Bartoletti MDegano PFerrari GZunino R(2009)Local policies for resource usage analysisACM Transactions on Programming Languages and Systems10.1145/1552309.155231331:6(1-43)Online publication date: 26-Aug-2009
https://dl.acm.org/doi/10.1145/1552309.1552313
Skalka C(2008)Types and trace effects for object orientationHigher-Order and Symbolic Computation10.1007/s10990-008-9032-621:3(239-282)Online publication date: 1-Sep-2008
https://dl.acm.org/doi/10.1007/s10990-008-9032-6
Bartoletti MDegano PFerrari GZunino R(2007)Types and Effects for resource usage analysisProceedings of the 10th international conference on Foundations of software science and computational structures10.5555/1760037.1760043(32-47)Online publication date: 24-Mar-2007
https://dl.acm.org/doi/10.5555/1760037.1760043
Skalka CLeuschel MPodelski A(2007)Type safe dynamic linking for JVM access controlProceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming10.1145/1273920.1273928(51-62)Online publication date: 14-Jul-2007
https://dl.acm.org/doi/10.1145/1273920.1273928
Higuchi TOhori A(2007)A static type system for JVM access controlACM Transactions on Programming Languages and Systems10.1145/1180475.118047929:1(4-es)Online publication date: 1-Jan-2007
https://dl.acm.org/doi/10.1145/1180475.1180479
Bartoletti MDegano PFerrari GZunino R(2007)Types and Effects for Resource Usage AnalysisFoundations of Software Science and Computational Structures10.1007/978-3-540-71389-0_4(32-47)Online publication date: 2007
https://doi.org/10.1007/978-3-540-71389-0_4
Show More Cited By

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