Testing Library Specifications by Verifying Conformance Tests

Joseph Roland Kiniry, Daniel Zimmerman, Ralph Hyland

    Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review


    Formal specifications of standard libraries are necessary when statically verifying software that uses those libraries. Library specifications must be both correct, accurately reflecting library behavior, and useful, describing library behavior in sufficient detail to allow static verification of client programs. Specication and verification 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 refined 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 specifications 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 specifications through static verification. FCTD is beginning to see significant 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 specification 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.
    TitelTAP'12 Proceedings of the 6th international conference on Tests and Proofs
    ISBN (Trykt)978-3-642-30472-9
    StatusUdgivet - 2012
    Begivenhed6th International Conference on Tests & Proofs - Prague, Tjekkiet
    Varighed: 31 maj 20121 jun. 2012
    Konferencens nummer: 6


    Konference6th International Conference on Tests & Proofs
    AndetOrganised by Yuri Gurevich & Bertrand Meyer
    NavnLecture Notes in Computer Science


    Dyk ned i forskningsemnerne om 'Testing Library Specifications by Verifying Conformance Tests'. Sammen danner de et unikt fingeraftryk.