Skip to Main content Skip to Navigation
Conference papers

Specifying and Checking Protocols of Multithreaded Classes

Clément Hurlin 1 
1 EVEREST - Environments for Verification and Security of Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : In the Design By Contract (DBC) approach, programmers specify methods with pre and postconditions (also called contracts). Earlier work added protocols to the DBC approach to describe allowed method call sequences for classes. We extend this work to deal with a variant of generic classes and multithreaded classes. We present the semantical foundations of our extension. We describe a new technique to check that method contracts are correct w.r.t. to protocols. We show how to generate programs that must be proven to show that method contracts are correct w.r.t. to protocols. Because little support currently exists to help writing method contracts, our technique helps programmers to check their contracts early in the development process.
Document type :
Conference papers
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Clément Hurlin Connect in order to contact the contributor
Submitted on : Tuesday, May 19, 2009 - 12:26:44 PM
Last modification on : Friday, February 4, 2022 - 3:23:04 AM
Long-term archiving on: : Saturday, November 26, 2016 - 9:41:58 AM


Files produced by the author(s)




Clément Hurlin. Specifying and Checking Protocols of Multithreaded Classes. ACM Symposium on Applied Computing (SAC'09), ACM, Mar 2009, Honolulu, United States. pp.587--592, ⟨10.1145/1529282.1529407⟩. ⟨inria-00334527v3⟩



Record views


Files downloads