Testing Library Specifications by Verifying Conformance Tests

Joseph Kiniry, Daniel M. Zimmerman, Ralph Hyland

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

97 Downloads (Pure)

Abstract

Formal specications of standard libraries are necessary when statically verifying software that uses those libraries. Library specications must be both correct, accurately reecting library behavior, and useful, describing library behavior in sucient detail to allow static verication of client programs. Specication and veriation researchers regularly face the question of whether the library specications we use are correct and useful, and we have collectively provided no good answers. Over the past few years we have created and rened a software engineering process, which we call the Formal CTD Process (FCTD), to address this problem. Although FCTD is primarily targeted toward those who write Java libraries (or specications for existing Java libraries) using the Java Modeling Language (JML), its techniques are broadly applicable. The key to FCTD is its novel usage of library conformance test suites. Rather than executing the conformance tests, FCTD uses them to measure the correctness and utility of specications through static verication. FCTD is beginning to see signicant use within the JML community
and is the cornerstone process of the JML Spec-a-thons, meetings that bring JML researchers and practitioners together for intensive specication writing sessions. This article describes the Formal CTD Process, its use in small case studies, and its broad application to the standard Java class library.
Original languageEnglish
Title of host publicationTests and Proofs : 6th International Conference, TAP 2012, Prague, Czech Republic, May 31 – June 1, 2012. Proceedings
PublisherSpringer
Publication date2012
Pages51-66
ISBN (Print)978-3-642-30472-9
DOIs
Publication statusPublished - 2012
Externally publishedYes
Event6th International Conference on Tests & Proofs (TAP 2012) - Prague, Czech Republic
Duration: 31 May 20121 Jun 2012

Conference

Conference6th International Conference on Tests & Proofs (TAP 2012)
CountryCzech Republic
CityPrague
Period31/05/201201/06/2012
SeriesLecture Notes in Computer Science
Volume7305
ISSN0302-9743

Cite this

Kiniry, J., Zimmerman, D. M., & Hyland, R. (2012). Testing Library Specifications by Verifying Conformance Tests. In Tests and Proofs: 6th International Conference, TAP 2012, Prague, Czech Republic, May 31 – June 1, 2012. Proceedings (pp. 51-66). Springer. Lecture Notes in Computer Science, Vol.. 7305 https://doi.org/10.1007/978-3-642-30473-6_6