research-article

What good are strong specifications?

Authors:

Nadia Polikarpova,

Carlo A. Furia,

Bertrand MeyerAuthors Info & Claims

ICSE '13: Proceedings of the 2013 International Conference on Software Engineering

Pages 262 - 271

Published: 18 May 2013 Publication History

Abstract

Experience with lightweight formal methods suggests that programmers are willing to write specification if it brings tangible benefits to their usual development activities. This paper considers stronger specifications and studies whether they can be deployed as an incremental practice that brings additional benefits without being unacceptably expensive. We introduce a methodology that extends Design by Contract to write strong specifications of functional properties in the form of preconditions, postconditions, and invariants. The methodology aims at being palatable to developers who are not fluent in formal techniques but are comfortable with writing simple specifications. We evaluate the cost and the benefits of using strong specifications by applying the methodology to testing data structure implementations written in Eiffel and C#. In our extensive experiments, testing against strong specifications detects twice as many bugs as standard contracts, with a reasonable overhead in terms of annotation burden and run-time performance while testing. In the wide spectrum of formal techniques for software quality, testing against strong specifications lies in a "sweet spot" with a favorable benefit to effort ratio.

References

[1]

D. L. Parnas, “Precise documentation: The key to better software,” in The Future of Software Engineering. Springer, 2011, pp. 125–148.

[2]

B. Meyer, Object Oriented Software Construction. Prentice Hall, 1997.

Digital Library

[3]

P. Chalin, “Are practitioners writing contracts?” in The RODIN Book, ser. LNCS, vol. 4157, 2006, p. 100.

Digital Library

[4]

K. Beck, Test-Driven Development. Addison-Wesley, 2002.

Digital Library

[5]

N. Polikarpova, C. A. Furia, and B. Meyer, “Specifying reusable components,” in VSTTE, ser. LNCS, vol. 6217, 2010, pp. 127–141.

Digital Library

[6]

B. Meyer, A. Fiva, I. Ciupa, A. Leitner, Y. Wei, and E. Stapf, “Programs that test themselves,” IEEE Computer, vol. 42, no. 9, pp. 46–55, 2009.

Digital Library

[7]

http://dsa.codeplex.com/.

[8]

N. Tillmann and J. de Halleux, “Pex–white box test generation for .NET,” in TAP, 2008, pp. 134–153.

Digital Library

[9]

N. Polikarpova, I. Ciupa, and B. Meyer, “A comparative study of programmer-written and automatically inferred contracts,” in ISSTA, 2009, pp. 93–104.

Digital Library

[10]

M. Barnett, K. R. M. Leino, and W. Schulte, “The Spec# programming system: an overview,” in CASSIS. Berlin, Heidelberg: Springer-Verlag, 2005, pp. 49–69.

Digital Library

[11]

http://se.inf.ethz.ch/people/polikarpova/mbctesting.

[12]

A. Arcuri and L. Briand, “A practical guide for using statistical tests to assess randomized algorithms in software engineering,” in ICSE. ACM, 2011, pp. 1–10.

Digital Library

[13]

http://research.microsoft.com/en-us/projects/contracts/.

[14]

N. Polikarpova, C. A. Furia, Y. Wei, Y. Pei, and B. Meyer, “What good are strong specifications?” Extended version available at http://arxiv.org/abs/1208.3337.

Digital Library

[15]

N. Nagappan, E. M. Maximilien, T. Bhat, and L. Williams, “Realizing quality improvement through test driven development: results and experiences of four industrial teams,” ESE, vol. 13, pp. 289–302, 2008.

Digital Library

[16]

E. M. Maximilien and L. Williams, “Assessing test-driven development at IBM,” in ICSE, 2003, pp. 564–569.

Digital Library

[17]

V. Klebanov et al., “The 1st verified software competition,” in FM, ser. LNCS, vol. 6664, 2011, extended version at www.vscomp.org.

Digital Library

[18]

F. Dupressoir, A. D. Gordon, J. Jürjens, and D. A. Naumann, “Guiding a general-purpose C verifier to prove cryptographic protocols,” in IEEE Computer Security Foundations Symposium, 2011.

Digital Library

[19]

J.-C. Filliˆatre, “Verifying two lines of C with Why3: an exercise in program verification,” in VSTTE, ser. LNCS, 2012, pp. 83–97.

[20]

R. M. Hierons et al., “Using formal specifications to support testing,” ACM Comput. Surv., vol. 41, no. 2, 2009.

Digital Library

[21]

J. D. Gannon, P. R. McMullin, and R. G. Hamlet, “Data-abstraction implementation, specification, and testing,” ACM Trans. Program. Lang. Syst., vol. 3, no. 3, pp. 211–223, 1981.

Digital Library

[22]

J. Chang and D. J. Richardson, “Structural specification-based testing: Automated support and experimental evaluation,” in ESEC/FSE, 1999, pp. 285–302.

Digital Library

[23]

P. Stocks and D. A. Carrington, “Test templates: A specification-based testing framework,” in ICSE, 1993, pp. 405–414.

Digital Library

[24]

A. J. Offutt and A. Abdurazik, “Generating tests from UML specifications,” in UML, 1999, pp. 416–429.

Digital Library

[25]

D. Marinov and S. Khurshid, “TestEra: A novel framework for automated testing of Java programs,” in ASE, 2001, p. 22.

Digital Library

[26]

Y. Cheon and G. T. Leavens, “A simple and practical approach to unit testing: The JML and JUnit way,” in ECOOP, 2002, pp. 231–255.

Digital Library

[27]

C. Boyapati, S. Khurshid, and D. Marinov, “Korat: automated testing based on Java predicates,” in ISSTA, 2002, pp. 123–133.

Digital Library

[28]

M. Staats, M. W. Whalen, and M. P. E. Heimdahl, “Programs, tests, and oracles,” in ICSE, 2011, pp. 391–400.

Digital Library

[29]

M. M. Müller, R. Typke, and O. Hagner, “Two controlled experiments concerning the usefulness of assertions as a means for programming,” in ICSM, 2002, pp. 84–92.

Digital Library

[30]

L. du Bousquet, Y. Ledru, O. Maury, C. Oriat, and J.-L. Lanet, “Reusing a JML specification dedicated to verification for testing, and vice-versa: Case studies,” J. Autom. Reasoning, vol. 45, no. 4, pp. 415–435, 2010.

Digital Library

[31]

C. A. R. Hoare, “How did software get so reliable without proof?” in FME, 1996, pp. 1–17.

Digital Library

[32]

C. Pacheco and M. D. Ernst, “Eclat: Automatic generation and classification of test inputs,” in ECOOP, 2005, pp. 504–527.

Digital Library

[33]

T. Xie and D. Notkin, “Tool-assisted unit-test generation and selection based on operational abstractions,” Autom. Softw. Eng., vol. 13, no. 3, pp. 345–371, 2006.

Digital Library

[34]

A. Zeller, “Mining specifications: A roadmap,” in The Future of Software Engineering. Springer, 2010, pp. 173–182.

[35]

Y. Wei, H. Roth, C. A. Furia, Y. Pei, A. Horton, M. Steindorfer, M. Nordio, and B. Meyer, “Stateful testing: Finding more errors in code and contracts,” in ASE, 2011, pp. 440–443.

Digital Library

[36]

M. d’Amorim, C. Pacheco, T. Xie, D. Marinov, and M. D. Ernst, “An empirical comparison of automated generation and classification techniques for object-oriented unit testing,” in ASE, 2006, pp. 59–68.

Digital Library

[37]

Y. Wei, C. A. Furia, N. Kazmin, and B. Meyer, “Inferring better contracts,” in ICSE, 2011, pp. 191–200.

Digital Library

[38]

G. T. Leavens, Y. Cheon, C. Clifton, C. Ruby, and D. R. Cok, “How the design of JML accommodates both runtime assertion checking and formal verification,” Sci. Com. Prg., vol. 55, no. 1-3, pp. 185–208, 2005.

Digital Library

Cited By

Molina FPonzio PAguirre NFrias M(2021)EvoSpexProceedings of the 43rd International Conference on Software Engineering10.1109/ICSE43902.2021.00112(1223-1235)Online publication date: 22-May-2021
https://dl.acm.org/doi/10.1109/ICSE43902.2021.00112
Hallett JPatnaik NShreeve BRashid A(2021)Do this! Do that!, And nothing will happenProceedings of the 43rd International Conference on Software Engineering10.1109/ICSE43902.2021.00053(486-498)Online publication date: 22-May-2021
https://dl.acm.org/doi/10.1109/ICSE43902.2021.00053
Astorga AMadhusudan PSaha SWang SXie TMcKinley KFisher K(2019)Learning stateful preconditions modulo a test generatorProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314641(775-787)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314641
Show More Cited By

Index Terms

What good are strong specifications?
1. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Requirements analysis
      2. Software implementation planning
        Software design techniques
    2. Software development process management

Recommendations

Formalized structured analysis specifications
Protective Interface Specifications
Abstract.
The interface specification of a procedure describes the procedure's behaviour using pre- and postconditions. These pre- and postconditions are written using various functions. If some of these functions are partial, or underspecified, then the ...
Trace Specifications: Methodology and Models

The authors summarize the trace specification language and present the trace specification methodology: a set of heuristics designed to make the reading and writing of complex specifications manageable. Also described is a technique for constructing ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE '13: Proceedings of the 2013 International Conference on Software Engineering

May 2013

1561 pages

ISBN:9781467330763

General Chair:
David Notkin,
Program Chairs:
Betty H. C. Cheng,
Klaus Pohl

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

IEEE Press

Publication History

Published: 18 May 2013

Check for updates

Qualifiers

Research-article

Conference

ICSE '13

Sponsor:

SIGSOFT

ICSE '13: 35th International Conference on Software Engineering

May 18 - 26, 2013

CA, San Francisco, USA

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
350
Total Downloads

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

Reflects downloads up to 27 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Molina FPonzio PAguirre NFrias M(2021)EvoSpexProceedings of the 43rd International Conference on Software Engineering10.1109/ICSE43902.2021.00112(1223-1235)Online publication date: 22-May-2021
https://dl.acm.org/doi/10.1109/ICSE43902.2021.00112
Hallett JPatnaik NShreeve BRashid A(2021)Do this! Do that!, And nothing will happenProceedings of the 43rd International Conference on Software Engineering10.1109/ICSE43902.2021.00053(486-498)Online publication date: 22-May-2021
https://dl.acm.org/doi/10.1109/ICSE43902.2021.00053
Astorga AMadhusudan PSaha SWang SXie TMcKinley KFisher K(2019)Learning stateful preconditions modulo a test generatorProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314641(775-787)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314641
Uva MPonzio PRegis GAguirre NFrias M(2018)Automated workarounds from Java program specifications based on SAT solvingInternational Journal on Software Tools for Technology Transfer (STTT)10.5555/3288063.328808320:6(665-688)Online publication date: 1-Nov-2018
https://dl.acm.org/doi/10.5555/3288063.3288083
Milanez ALima BFerreira JMassoni TShin SShin DLencastre M(2017)Nonconformance between programs and contractsProceedings of the Symposium on Applied Computing10.1145/3019612.3019779(1219-1224)Online publication date: 3-Apr-2017
https://dl.acm.org/doi/10.1145/3019612.3019779
Pearce DLaToza TAnslow CSunshine J(2015)Some usability hypotheses for verificationProceedings of the 6th Workshop on Evaluation and Usability of Programming Languages and Tools10.1145/2846680.2846691(57-60)Online publication date: 26-Oct-2015
https://dl.acm.org/doi/10.1145/2846680.2846691
Kogtenkov AMeyer BVelder S(2015)Alias calculus, change calculus and frame inferenceScience of Computer Programming10.1016/j.scico.2013.11.00697:P1(163-172)Online publication date: 1-Jan-2015
https://dl.acm.org/doi/10.1016/j.scico.2013.11.006
Schiller TDonohue KCoward FErnst MJalote PBriand LHoek A(2014)Case studies and tools for contract specificationsProceedings of the 36th International Conference on Software Engineering10.1145/2568225.2568285(596-607)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2568225.2568285
Estler HFuria CNordio MPiccioni MMeyer B(2014)Contracts in PracticeProceedings of the 19th International Symposium on FM 2014: Formal Methods - Volume 844210.1007/978-3-319-06410-9_17(230-246)Online publication date: 12-May-2014
https://dl.acm.org/doi/10.1007/978-3-319-06410-9_17
Tschannen JFuria CNordio MMeyer B(2013)Program Checking with Less HassleRevised Selected Papers of the 5th International Conference on Verified Software: Theories, Tools, Experiments - Volume 816410.1007/978-3-642-54108-7_8(149-169)Online publication date: 17-May-2013
https://dl.acm.org/doi/10.1007/978-3-642-54108-7_8

View Options

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