research-article

Synthesizing iterators from abstraction functions

Authors:

Vajihollah Montaghami,

Francesca Leung,

Daniel JacksonAuthors Info & Claims

GPCE '12: Proceedings of the 11th International Conference on Generative Programming and Component Engineering

Pages 31 - 40

https://doi.org/10.1145/2371401.2371407

Published: 26 September 2012 Publication History

Abstract

A technique for synthesizing iterators from declarative abstraction functions written in a relational logic specification language is described. The logic includes a transitive closure operator that makes it convenient for expressing reachability queries on linked data structures. Some optimizations, including tuple elimination, iterator flattening, and traversal state reduction, are used to improve performance of the generated iterators.

A case study demonstrates that most of the iterators in the widely used JDK Collections classes can be replaced with code synthesized from declarative abstraction functions. These synthesized iterators perform competitively with the hand-written originals.

In a user study the synthesized iterators always passed more test cases than the hand-written ones, were almost always as efficient, usually took less programmer effort, and were the qualitative preference of all participants who provided free-form comments.

References

[1]

J. Bloch. Effective Java. Addison-Wesley, Reading, Mass., 2001.

[2]

L. Burdy, Y. Cheon, D. Cok, M. D. Ernst, J. R. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of JML tools and applications. Software Tools for Technology Transfer, 7(3): 212--232, June 2005.

Digital Library

[3]

Y. Cheon. A Runtime Assertion Checker for the Java Modeling Language. PhD thesis, Department of Computer Science, Iowa State University, Apr. 2003.

[4]

T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein. Introduction to Algorithms. The MIT Press and McGraw-Hill, 2nd edition, 2001.

Digital Library

[5]

B. Demsky, C. Cadar, D. Roy, and M. C. Rinard. Efficient specification-assisted error localization. In WODA, 2004.

[6]

G. Dennis. A Relational Framework for Bounded Program Verification. PhD thesis, MIT, 2009.

[7]

A. Gesar, H. Hussmann, and A. Muck. A compiler for a class of conditional term rewriting systems. In Kaplan and Jouannaud {19}.

[8]

ECOOP, volume 1628 of LNCS, 1999. Springer-Verlag.

[9]

P. Hawkins, A. Aiken, K. Fisher, M. Rinard, and M. Sagiv. Data representation synthesis. In PLDI, June 2011.

Digital Library

[10]

J. Henkel and A. Diwan. Discovering algebraic specifications from Java classes. In ECOOP. July 2003. ISBN 3-540-40531-3.

[11]

T. Heuillard. Compiling conditional rewriting systems. In Kaplan and Jouannaud {19}.

[12]

C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4): 271--281, Dec. 1972.

Digital Library

[13]

S. S. Huan, D. Zook, and Y. Smaragdakis. Domain-specific languages and program generation with Meta-AspectJ. TOSEM, 18(2), Oct. 2008.

Digital Library

[14]

D. Jackson. Software Abstractions: Logic, Language, and Analysis. The MIT Press, revised edition, Jan. 2012.

Digital Library

[15]

B. Jacobs, E. Meijer, F. Piessens, and W. Schulte. Iterators revisited: proof rules and implementation. In Formal Techniques for Java-like Programs (FTfJP), 2005.

[16]

L. Jadoul, L. Duponcheel, and W. Van Puymbroeck. An algebraic data type specification language and its rapid prototyping environment. In ICSE, May 1989.

Digital Library

[17]

P. Jalote. Synthesizing implementations of abstract data types from axiomatic specifications. Software---Practice & Experience, 17(11), Nov. 1987.

Digital Library

[18]

K. D. Jones. A Semantics for a Larch/Modula-3 Interface Language. In Workshop on Larch. July 1992.

Digital Library

[19]

Proceedings of the 1st International Workshop on Term Rewriting Systems, volume 308 of LNCS, 1988. Springer-Verlag.

[20]

T. Kühne. Internal iteration externalized. In Guerraoui {8}.

[21]

V. Kuncak. Modular Data Structure Verification. PhD thesis, MIT, 2007.

Digital Library

[22]

R. Laemmel and S. P. Jones. Scrap your boilerplate: a practical approach to generic programming. In TLDI, 2003.

Digital Library

[23]

G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06u, Iowa State University, Apr. 2003. URL http://www.jmlspecs.org.

[24]

K. R. M. Leino. Data groups: specifying the modification of extended state. In OOPSLA, Oct. 1998.

Digital Library

[25]

K. R. M. Leino and A. Milicevic. Program extrapolation with Jennisys. Technical Report KRML219, Microsoft Research, 2012. URL http://research.microsoft.com/pubs/158573/krml219.pdf.

Digital Library

[26]

R. Lencevicius, U. Hölzle, and A. K. Singh. Query-based debugging of object-oriented programs. In OOPSLA, Oct. 1997.

Digital Library

[27]

R. Lencevicius, U. Hölzle, and A. K. Singh. Dynamic query-based debugging. In Guerraoui {8}, pages 135--160.

Digital Library

[28]

K. J. Lieberherr. Adaptive Object-Oriented Software: The Demeter Method with Propagation Patterns. PWS, 1996.

Digital Library

[29]

J. Liu and A. C. Myers. JMatch: Iterable Abstract Pattern Matching for Java. In PADL, 2003.

Digital Library

[30]

J. Liu, A. Kimball, and A. C. Myers. Interruptible iterators. In POPL, Jan. 2006.

Digital Library

[31]

A. Milicevic, D. Rayside, K. Yessenov, and D. Jackson. Unifying execution of imperative and declarative code. In ICSE, 2011.

Digital Library

[32]

C. Morgan. Programming from Specifications. Prentice-Hall, Inc., 2nd edition, 1998. First edition 1990.

Digital Library

[33]

S. Murer, S. Omohundro, D. Stoutamire, and C. Szypersky. Iteration abstraction in Sather. TOPLAS, 18(1), 1996.

Digital Library

[34]

M. Odersky, L. Spoon, and B. Venners. Programming in Scala. Artima, Nov. 2008.

[35]

C. Pacheco, S. K. Lahiri, M. D. Ernst, and T. Ball. Feedback-directed random test generation. In ICSE, 2007.

Digital Library

[36]

A. Potanin, J. Noble, and R. Biddle. Checking ownership and confinement. Concurrency and Computation: Practice and Experience, 16(7): 671--687, 2004.

Digital Library

[37]

V. K. Proulx and W. Jossey. Unit test support for Java via reflection and annotations. In Principles and Practice of Programming in Java, 2009.

Digital Library

[38]

D. Rayside, Z. Benjamin, R. Singh, J. P. Near, A. Milicevic, and D. Jackson. Equality and hashing for (almost) free: Generating implementations from abstraction functions. In ICSE, 2009.

Digital Library

[39]

D. Rayside, A. Milicevic, K. Yessenov, G. Dennis, and D. Jackson. Agile specifications. In Proceedings of Onward'09, Oct. 2009.

Digital Library

[40]

C. Reichenbach, N. Immerman, Y. Smaragdakis, E. E. Aftandilian, and S. Z. Guyer. What can the GC compute efficiently? A language for heap assertions at GC time. In OOPSLA, Oct. 2010.

Digital Library

[41]

H. Samimi, E. D. Aung, and T. Millstein. Falling back on executable specifications. In ECOOP. June 2010.

Digital Library

[42]

Y. Smaragdakis and D. Batory. DiSTiL: a Transformation Library for Data Structures. In DSL, 1997.

Digital Library

[43]

M. K. Srivas. Automatic synthesis of implementations for abstract data types from algebraic specifications. PhD thesis, MIT, 1982.

[44]

E. Torlak and D. Jackson. Kodkod: A relational model finder. In TACAS. Mar. 2007.

Digital Library

[45]

M. T. Vandevoorde and J. V. Guttag. Using specialized procedures and specification-based analysis to reduce the runtime costs of modularity. In FSE, Dec. 1994.

Digital Library

[46]

M. Vaziri, F. Tip, S. Fink, and J. Dolby. Declarative object identity using relation types. In ECOOP. July 2007.

Digital Library

[47]

P. Wadler. Deforestation: transforming programs to eliminate trees. TCS, 73: 231--248, 1990.

Digital Library

[48]

D. Willis, D. J. Pearce, and J. Noble. Efficient object querying for Java. In ECOOP. July 2006.

Digital Library

[49]

K. Yessenov. A light-weight specification language for bounded program verification. Master's thesis, MIT, May 2009.

[50]

K. Zee, V. Kuncak, and M. Rinard. Full functional verification of linked data structures. In PLDI, June 2008.

Digital Library

Cited By

Nie PParovic MZang ZKhurshid SMilicevic AGligoric M(2020)Unifying execution of imperative generators and declarative specificationsProceedings of the ACM on Programming Languages10.1145/34282854:OOPSLA(1-26)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428285
Sullivan AMarinov DKhurshid S(2019)Solution Enumeration Abstraction: A Modeling Idiom to Enhance a Lightweight Formal MethodFormal Methods and Software Engineering10.1007/978-3-030-32409-4_21(336-352)Online publication date: 28-Oct-2019
https://doi.org/10.1007/978-3-030-32409-4_21
Milicevic ANear JKang EJackson D(2017)Alloy*: a general-purpose higher-order relational constraint solverFormal Methods in System Design10.1007/s10703-016-0267-2Online publication date: 27-Jan-2017
https://doi.org/10.1007/s10703-016-0267-2
Show More Cited By

Index Terms

Synthesizing iterators from abstraction functions
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Object oriented languages

Recommendations

Interruptible iterators
POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

This paper introduces interruptible iterators, a language feature that makes expressive iteration abstractions much easier to implement. Iteration abstractions are valuable for software design, as shown by their frequent use in well-designed data ...
Synthesizing iterators from abstraction functions
GPCE '12

A technique for synthesizing iterators from declarative abstraction functions written in a relational logic specification language is described. The logic includes a transitive closure operator that makes it convenient for expressing reachability ...
A new iteration mechanism for the C++ programming language

A new mechanism for writing iterators in the C++ programming language is proposed in this paper. It provides a handy notation for writing general iterators easily, and a simple semantics based-on semicoroutines. A set of useful programming idioms for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

GPCE '12: Proceedings of the 11th International Conference on Generative Programming and Component Engineering

September 2012

148 pages

ISBN:9781450311298

DOI:10.1145/2371401

General Chair:
Klaus Ostermann
University of Marburg, Germany
,
Program Chair:
Walter Binder
University of Lugano, Switzerland

ACM SIGPLAN Notices Volume 48, Issue 3
GPCE '12
March 2013
140 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2480361
Issue’s Table of Contents

Copyright © 2012 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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 September 2012

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

GPCE'12

Sponsor:

SIGPLAN

GPCE'12: Generative Programming and Component Engineering

September 26 - 27, 2012

Dresden, Germany

Acceptance Rates

Overall Acceptance Rate 56 of 180 submissions, 31%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

23
Total Citations
View Citations
216
Total Downloads

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

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nie PParovic MZang ZKhurshid SMilicevic AGligoric M(2020)Unifying execution of imperative generators and declarative specificationsProceedings of the ACM on Programming Languages10.1145/34282854:OOPSLA(1-26)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428285
Sullivan AMarinov DKhurshid S(2019)Solution Enumeration Abstraction: A Modeling Idiom to Enhance a Lightweight Formal MethodFormal Methods and Software Engineering10.1007/978-3-030-32409-4_21(336-352)Online publication date: 28-Oct-2019
https://doi.org/10.1007/978-3-030-32409-4_21
Milicevic ANear JKang EJackson D(2017)Alloy*: a general-purpose higher-order relational constraint solverFormal Methods in System Design10.1007/s10703-016-0267-2Online publication date: 27-Jan-2017
https://doi.org/10.1007/s10703-016-0267-2
Milicevic ANear JKang EJackson DBertolino ACanfora GElbaum S(2015)Alloy*Proceedings of the 37th International Conference on Software Engineering - Volume 110.5555/2818754.2818829(609-619)Online publication date: 16-May-2015
https://dl.acm.org/doi/10.5555/2818754.2818829
Milicevic ANear JKang EJackson D(2015)Alloy*: A General-Purpose Higher-Order Relational Constraint Solver2015 IEEE/ACM 37th IEEE International Conference on Software Engineering10.1109/ICSE.2015.77(609-619)Online publication date: May-2015
https://doi.org/10.1109/ICSE.2015.77
Anthes G(2014)Researchers simplify parallel programmingCommunications of the ACM10.1145/266710957:11(13-15)Online publication date: 27-Oct-2014
https://dl.acm.org/doi/10.1145/2667109
De Meo PFerrara EFiumara GProvetti A(2014)On Facebook, most ties are weakCommunications of the ACM10.1145/262943857:11(78-84)Online publication date: 27-Oct-2014
https://dl.acm.org/doi/10.1145/2629438
Huang JNie FHuang HDing C(2014)Robust Manifold Nonnegative Matrix FactorizationACM Transactions on Knowledge Discovery from Data10.1145/26014348:3(1-21)Online publication date: 1-Jun-2014
https://dl.acm.org/doi/10.1145/2601434
Zhang YYeung D(2014)A Regularization Approach to Learning Task Relationships in Multitask LearningACM Transactions on Knowledge Discovery from Data10.1145/25380288:3(1-31)Online publication date: 1-Jun-2014
https://dl.acm.org/doi/10.1145/2538028
Kurilova DRayside D(2013)On the simplicity of synthesizing linked data structure operationsACM SIGPLAN Notices10.1145/2637365.251722549:3(155-158)Online publication date: 27-Oct-2013
https://dl.acm.org/doi/10.1145/2637365.2517225
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