Specifying and Checking Protocols of Multithreaded Classes

C. Hurlin

doi:10.1145/1529282.1529407

Specifying and Checking Protocols of Multithreaded Classes

C. Hurlin

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

9 Citations (Scopus)

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.

Original language	Undefined
Title of host publication	Proceedings of the 24th Annual ACM Symposium on Applied Computing
Place of Publication	New York
Publisher	Association for Computing Machinery
Pages	587-592
Number of pages	6
ISBN (Print)	978-1-60558-166-8
DOIs	https://doi.org/10.1145/1529282.1529407
Publication status	Published - 9 Mar 2009
Event	24th Annual ACM Symposium on Applied Computing, SAC 2009 - Honolulu, United States Duration: 8 Mar 2009 → 12 Mar 2009 Conference number: 24 https://www.sigapp.org/sac/sac2009/

Publication series

Name
Publisher	ACM

Conference

Conference	24th Annual ACM Symposium on Applied Computing, SAC 2009
Abbreviated title	SAC
Country/Territory	United States
City	Honolulu
Period	8/03/09 → 12/03/09
Other	8-12 March 2009
Internet address	https://www.sigapp.org/sac/sac2009/

Keywords

Protocols
Object Orientation
EWI-15320
METIS-263831
Design By Contract
Multithreading
IR-65479

Access to Document

10.1145/1529282.1529407

Cite this

@inproceedings{2344841bddb549d299baf9bdfbb57b54,

title = "Specifying and Checking Protocols of Multithreaded Classes",

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.",

keywords = "Protocols, Object Orientation, EWI-15320, METIS-263831, Design By Contract, Multithreading, IR-65479",

author = "C. Hurlin",

note = "10.1145/1529282.1529407 ; 24th Annual ACM Symposium on Applied Computing, SAC 2009 ; Conference date: 08-03-2009 Through 12-03-2009",

year = "2009",

month = mar,

day = "9",

doi = "10.1145/1529282.1529407",

language = "Undefined",

isbn = "978-1-60558-166-8",

publisher = "Association for Computing Machinery",

pages = "587--592",

booktitle = "Proceedings of the 24th Annual ACM Symposium on Applied Computing",

url = "https://www.sigapp.org/sac/sac2009/",

}

Hurlin, C 2009, Specifying and Checking Protocols of Multithreaded Classes. in Proceedings of the 24th Annual ACM Symposium on Applied Computing., 10.1145/1529282.1529407, Association for Computing Machinery, New York, pp. 587-592, 24th Annual ACM Symposium on Applied Computing, SAC 2009, Honolulu, Hawaii, United States, 8/03/09. https://doi.org/10.1145/1529282.1529407

TY - GEN

T1 - Specifying and Checking Protocols of Multithreaded Classes

AU - Hurlin, C.

N1 - Conference code: 24

PY - 2009/3/9

Y1 - 2009/3/9

N2 - 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.

AB - 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.

KW - Protocols

KW - Object Orientation

KW - EWI-15320

KW - METIS-263831

KW - Design By Contract

KW - Multithreading

KW - IR-65479

U2 - 10.1145/1529282.1529407

DO - 10.1145/1529282.1529407

M3 - Conference contribution

SN - 978-1-60558-166-8

SP - 587

EP - 592

BT - Proceedings of the 24th Annual ACM Symposium on Applied Computing

PB - Association for Computing Machinery

CY - New York

T2 - 24th Annual ACM Symposium on Applied Computing, SAC 2009

Y2 - 8 March 2009 through 12 March 2009

ER -