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.
Type de document :
Communication dans un congrès
ACM Symposium on Applied Computing (SAC'09), Mar 2009, Honolulu, United States. ACM Press, pp.587--592, 2009, 〈10.1145/1529282.1529407〉
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00334527
Contributeur : Clément Hurlin <>
Soumis le : mardi 19 mai 2009 - 12:26:44
Dernière modification le : samedi 27 janvier 2018 - 01:30:46
Document(s) archivé(s) le : samedi 26 novembre 2016 - 09:41:58

Fichier

sac09.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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

Partager

Métriques

Consultations de la notice

136

Téléchargements de fichiers

71