Separating Obligations of Subjects and Handlers for More Flexible Event Type Verification

Abstract : Implicit invocation languages, like aspect-oriented languages, automate the Observer pattern, which decouples subjects (base code) from handlers (advice), and then compound them together in the final system. For such languages, event types have been proposed as a way of further decoupling subjects from handlers. In Ptolemy, subjects explicitly announce events at certain program points, and pass the announced piece of code to the handlers for its eventual execution. This implies a mutual dependency between subjects and handlers that should be considered in verification; i.e., verification of subject code should consider the handlers and vice versa.However, in Ptolemy the event type defines only one obligation that both the handlers and the announced piece of code must satisfy. This limits the flexibility and completeness of verification in Ptolemy. That is, some correct programs cannot be verified due to specification mismatches between the announced code and the handlers’ code. For example, when the announced code does not satisfy the specification of the entire event and handlers must make up the difference, or when the announced code has no effect, imposing a monotonic behavior on the handlers.In this paper we propose an extension to the specification features of Ptolemy that explicitly separates the specification of the handlers from the specification of the announced code. This makes verification in our new language PtolemyRely more flexible and more complete, while preserving modularity.
Type de document :
Communication dans un congrès
Walter Binder; Eric Bodden; Welf Löwe. 12th International Conference on Software Composition (SC), Jun 2013, Budapest, Hungary. Springer, Lecture Notes in Computer Science, LNCS-8088, pp.65-80, 2013, Software Composition. 〈10.1007/978-3-642-39614-4_5〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01492777
Contributeur : Hal Ifip <>
Soumis le : lundi 20 mars 2017 - 15:34:58
Dernière modification le : mardi 16 janvier 2018 - 15:43:54
Document(s) archivé(s) le : mercredi 21 juin 2017 - 13:11:35

Fichier

978-3-642-39614-4_5_Chapter.pd...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

José Sánchez, Gary Leavens. Separating Obligations of Subjects and Handlers for More Flexible Event Type Verification. Walter Binder; Eric Bodden; Welf Löwe. 12th International Conference on Software Composition (SC), Jun 2013, Budapest, Hungary. Springer, Lecture Notes in Computer Science, LNCS-8088, pp.65-80, 2013, Software Composition. 〈10.1007/978-3-642-39614-4_5〉. 〈hal-01492777〉

Partager

Métriques

Consultations de la notice

30

Téléchargements de fichiers

14