Article

Synthesis of interface specifications for Java classes

Authors:

Wonhong NamAuthors Info & Claims

POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 98 - 109

https://doi.org/10.1145/1040305.1040314

Published: 12 January 2005 Publication History

Abstract

While a typical software component has a clearly specified (static) interface in terms of the methods and the input/output types they support, information about the correct sequencing of method calls the client must invoke is usually undocumented. In this paper, we propose a novel solution for automatically extracting such temporal specifications for Java classes. Given a Java class, and a safety property such as "the exception E should not be raised", the corresponding (dynamic) interface is the most general way of invoking the methods in the class so that the safety property is not violated. Our synthesis method first constructs a symbolic representation of the finite state-transition system obtained from the class using predicate abstraction. Constructing the interface then corresponds to solving a partial-information two-player game on this symbolic graph. We present a sound approach to solve this computationally-hard problem approximately using algorithms for learning finite automata and symbolic model checking for branching-time logics. We describe an implementation of the proposed techniques in the tool JIST--- Java Interface Synthesis Tool---and demonstrate that the tool can construct interfaces accurately and efficiently for sample Java2SDK library classes.

References

[1]

S. Abramsky. Semantics of interaction. Technical report, Oxford University, 2002.

[2]

R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):1--42, 2002.

Digital Library

[3]

G. Ammons, R. Bodík, and J. Larus. Mining specifications. In Proc. 29th ACM POPL, pages 4--16, 2002.

Digital Library

[4]

D. Angluin. Learning regular sets from queries and counterexamples. Information and Computation, 75:87--106, 1987.

Digital Library

[5]

T. Ball, R. Majumdar, T.D. Millstein, and S.K. Rajamani. Automatic predicate abstraction of C programs. In Proc. PLDI, ACM SIGPLAN Notices 36(5), pages 203--213, 2001.

Digital Library

[6]

T. Ball and S.K. Rajamani. The SLAM project: Debugging system software via static analysis. In Proc. 29th ACM POPL, pages 1--3, 2002.

Digital Library

[7]

H. Barringer, C.S. Pasareanu and D. Giannakopolou. Proof rules for automated compositional verification through learning. In Proc. of the 2nd Int'l Workshop on Specification and Verification of Component Based Systems, 2003.

[8]

T. Berg, B. Jonsson, M. Leucker, and M. Saksena. Insights to Angluin's learning. In Proc. of International Workshop on Software Verification and Validation, 2003.

[9]

A. Chakrabarti, L. de Alfaro, T.A. Henzinger, M. Jurdzinski, and F. Mang. Interface compatibility checking for software modules. In Proc. 14th CAV, LNCS 2404, Springer, pages 428--441, 2002.

Digital Library

[10]

A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV Version 2: An Opensource tool for symbolic model checking. In Proc. 14th CAV, LNCS 2404, Springer, pages 359--364, 2002.

Digital Library

[11]

E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. of Workshop on Logic of Programs, pages 52--71, 1981.

Digital Library

[12]

J.M. Cobleigh, D. Giannakopoulou, and C.S. Pasareanu. Learning assumptions for compositional verification. In Proc. 9th TACAS, LNCS 2619, Springer, pages 331--346, 2003.

Digital Library

[13]

J. Corbett, M. Dwyer, J. Hatcliff, S. Laubach, C.S. Pasareanu, Robby, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In Proc. 22nd ICSE, pages 439--448, 2000.

Digital Library

[14]

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4th ACM POPL, pages 238--252, 1977.

Digital Library

[15]

P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proc. 5th ACM POPL, pages 84--96, 1978.

Digital Library

[16]

L. de Alfaro and T.A. Henzinger. Interface automata. In Proc. 9th ACM FSE, pages 109--120, 2001.

Digital Library

[17]

R. DeLine and M. Fähndrich. Enforcing high-level protocols in low-level software. In Proc. ACM POPL, pages 59--69, 2001.

Digital Library

[18]

D. Giannakopoulou, C.S. Pasareanu and H. Barringer. Assumption generation for software component verification. In Proc. 17th ASE, pages 3--12, 2002.

Digital Library

[19]

S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In Proc. 9th CAV, LNCS 1254, pages 72--83, 1997.

Digital Library

[20]

T.A. Henzinger, R. Jhala, R. Majumdar, K.L. McMillan. Abstractions from proofs. In Proc. 31st ACM POPL, pages 232--244, 2004.

Digital Library

[21]

T.A. Henzinger, R. Jhala, R. Majumdar, G. Necula, G. Sutre, and W. Weimer. Temporal-safety proofs for systems code. In Proc. of CAV, LNCS 2404, pages 526--538. Springer, 2002.

Digital Library

[22]

G. Holzmann and M. Smith. Software model checking - extracting verification models from source code. In Formal Methods for Protocol Engineering and Distributed Systems, pages 481--497, 1999.

Digital Library

[23]

F. Logozzo. Automatic inference of class invariants. In Proc. of VMCAI, LNCS 2937, pages 211--222, 2004.

[24]

J. Nimmer and M. Ernst. Automatic generation of program specification. In Proc. of ISSTA, pages 229--239, 2002.

Digital Library

[25]

G. Ramalingam, A. Warshavsky, J. Field, D. Goyal and M. Sagiv. Deriving specialized program analyses for certifying component-client conformance. In ACM PLDI, pages 83--94, 2002.

Digital Library

[26]

J.H. Reif. Universal games of incomplete information. In Proc. of the 11th ACM symposium on Theory of computing, pages 288--308. ACM Press, 1979.

Digital Library

[27]

R. L. Rivest and R. E. Schapire. Inference of finite automata using homing sequences. Information and Computation, 103(2):299--347, 1993.

Digital Library

[28]

W. Thomas. Infinite games and verification. In Proc. 14th CAV, LNCS 2404, pages 58--64. Springer, 2002.

Digital Library

[29]

O. Tkachuk, M.B. Dwyer, and C.S. Pasareanu. Automated environment generation for software model checking. In Proc. 18th ASE, pages 116--127, 2003.

Digital Library

[30]

R. Vallée-Rai, L. Hendren, V. Sundaresan, E.G. Patrick Lam, and P. Co. Soot - a Java optimization framework. In Proc. CASCON, pages 125--135, 1999.

[31]

D. Walker. A type system for expressive security policies. In Proc. 27th ACM POPL, pages 254--267, 2000.

Digital Library

[32]

J. Whaley, M.C. Martin, and M.S. Lam. Automatic extraction of object-oriented component interfaces. In Proc. ISSTA, pages 218--228, 2002.

Digital Library

Cited By

Li XXiao GChen YTang ZJiang WLi K(2023)An Explicitly Weighted GCN Aggregator based on Temporal and Popularity Features for RecommendationACM Transactions on Recommender Systems10.1145/35872721:2(1-23)Online publication date: 24-Apr-2023
https://dl.acm.org/doi/10.1145/3587272
Dou QPan HTang HJiang PWang H(2023)Program synthesis algorithm based on context consistency heuristicInternational Journal of Machine Learning and Cybernetics10.1007/s13042-023-01925-315:2(559-571)Online publication date: 1-Aug-2023
https://doi.org/10.1007/s13042-023-01925-3
Kechagia MMechtaev SSarro FHarman M(2022)Evaluating Automatic Program Repair Capabilities to Repair API MisusesIEEE Transactions on Software Engineering10.1109/TSE.2021.306715648:7(2658-2679)Online publication date: 1-Jul-2022
https://doi.org/10.1109/TSE.2021.3067156
Show More Cited By

Index Terms

Synthesis of interface specifications for Java classes
1. Software and its engineering
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Synthesis of interface specifications for Java classes
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

While a typical software component has a clearly specified (static) interface in terms of the methods and the input/output types they support, information about the correct sequencing of method calls the client must invoke is usually undocumented. In ...
Tools to generate and check consistency of model classes for Java PathFinder

Java PathFinder (JPF) is a model checker for Java applications. Like any other model checker, JPF has to combat the notorious state space explosion problem. Since JPF is a JVM, it can only model check Java bytecode and needs to handle native calls ...
SAT-based counterexample-guided abstraction refinement

We describe new techniques for model checking in the counterexample-guided abstraction-refinement framework. The abstraction phase "hides" the logic of various variables, hence considering them as inputs. This type of abstraction may lead to "spurious" ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2005

402 pages

ISBN:158113830X

DOI:10.1145/1040305

General Chair:
Jens Palsberg
University of California, Los Angeles, CA
,
Program Chair:
Martín Abadi
University of California, Santa Cruz, CA

ACM SIGPLAN Notices Volume 40, Issue 1
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2005
391 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1047659
Issue’s Table of Contents

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: 12 January 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL05

Sponsor:

POPL05: The 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2005

January 12 - 14, 2005

California, Long Beach, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

311
Total Citations
View Citations
1,363
Total Downloads

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

Reflects downloads up to 23 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Li XXiao GChen YTang ZJiang WLi K(2023)An Explicitly Weighted GCN Aggregator based on Temporal and Popularity Features for RecommendationACM Transactions on Recommender Systems10.1145/35872721:2(1-23)Online publication date: 24-Apr-2023
https://dl.acm.org/doi/10.1145/3587272
Dou QPan HTang HJiang PWang H(2023)Program synthesis algorithm based on context consistency heuristicInternational Journal of Machine Learning and Cybernetics10.1007/s13042-023-01925-315:2(559-571)Online publication date: 1-Aug-2023
https://doi.org/10.1007/s13042-023-01925-3
Kechagia MMechtaev SSarro FHarman M(2022)Evaluating Automatic Program Repair Capabilities to Repair API MisusesIEEE Transactions on Software Engineering10.1109/TSE.2021.306715648:7(2658-2679)Online publication date: 1-Jul-2022
https://doi.org/10.1109/TSE.2021.3067156
Astorga ASaha SDinkins AWang FMadhusudan PXie T(2021)Synthesizing contracts correct modulo a test generatorProceedings of the ACM on Programming Languages10.1145/34854815:OOPSLA(1-27)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485481
Prabhu SFedyukovich GMadhukar KD'Souza DFreund SYahav E(2021)Specification synthesis with constrained Horn clausesProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454104(1203-1217)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454104
Li YChen YZhang LLiu D(2021)A novel learning algorithm for Büchi automata based on family of DFAs and classification treesInformation and Computation10.1016/j.ic.2020.104678281:COnline publication date: 1-Dec-2021
https://dl.acm.org/doi/10.1016/j.ic.2020.104678
Pick LFedyukovich GGupta A(2021)Unbounded Procedure Summaries from Bounded EnvironmentsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-67067-2_14(291-324)Online publication date: 12-Jan-2021
https://doi.org/10.1007/978-3-030-67067-2_14
Kellogg MRan MSridharan MSchäf MErnst MRothermel GBae D(2020)Verifying object constructionProceedings of the ACM/IEEE 42nd International Conference on Software Engineering10.1145/3377811.3380341(1447-1458)Online publication date: 27-Jun-2020
https://dl.acm.org/doi/10.1145/3377811.3380341
Yuniasri DRochimah SRaharjo A(2020)A Correlation Analysis Between ISO 25010 based Modularity and CK Metrics in Object-Oriented Software2020 International Conference on Advanced Science and Engineering (ICOASE)10.1109/ICOASE51841.2020.9436617(1-6)Online publication date: 23-Dec-2020
https://doi.org/10.1109/ICOASE51841.2020.9436617
Barros AOuyang CWei F(2020)Static Analysis for Improved Modularity of Procedural Web Application Programming InterfacesIEEE Access10.1109/ACCESS.2020.30089048(128182-128199)Online publication date: 2020
https://doi.org/10.1109/ACCESS.2020.3008904
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