hh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Dynamic Dispatch for Method Contracts Through Abstract Predicates
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). (MBT)
Karlsruhe Institute of Technology, Karlsruhe, Germany.
2016 (English)In: Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349, Vol. 9800, 238-267 p.Article in journal (Refereed) Published
Abstract [en]

Dynamic method dispatch is a core feature of object-oriented programming by which the executed implementation for a polymorphic method is only chosen at runtime. In this paper, we present a specification and verification methodology which extends the concept of dynamic dispatch to design-by-contract specifications.

The formal specification language JML has only rudimentary means for polymorphic abstraction in expressions. We promote these to fully flexible specification-only query methods called model methods that can, like ordinary methods, be overridden to give specifications a new semantics in subclasses in a transparent and modular fashion. Moreover, we allow them to refer to more than one program state which give us the possibility to fully abstract and encapsulate two-state specification contexts, i.e., history constraints and method postconditions. Finally, we provide an elegant and flexible mechanism to specify restrictions on specifications in subtypes. Thus behavioural subtyping can be enforced, yet it still allows for other specification paradigms.

We provide the semantics for model methods by giving a translation into a first order logic and according proof obligations. We fully implemented this framework in the KeY program verifier and successfully verified relevant examples. We have also implemented an extension to KeY to support permission-based verification of concurrent Java programs. In this context model methods provide a modular specification method to treat code synchronisation through API methods. © The Author(s) 2016.

Place, publisher, year, edition, pages
Cham: Springer, 2016. Vol. 9800, 238-267 p.
Keyword [en]
Modular specification, Design by Contract, Dynamic dispatch, abstract predicates, JML
National Category
Computer Science
Identifiers
URN: urn:nbn:se:hh:diva-32127DOI: 10.1007/978-3-319-46969-0_7Scopus ID: 2-s2.0-84992727403OAI: oai:DiVA.org:hh-32127DiVA: diva2:1010230
Conference
15th International Conference on Modularity (MODULARITY'15), Fort Collins, Colorado, USA, March 16-19, 2015
Projects
VerCorsAUTO-CAAS
Funder
Knowledge Foundation
Note

Funding: ERC grant 258405 for the VerCors project and by the Swedish Knowledge Foundation grant for the project AUTO-CAAS, DFG (German Research Foundation) under the Priority Programme SPP1593: Design For Future – Managed Software Evolution.

Available from: 2016-10-03 Created: 2016-10-03 Last updated: 2017-11-30Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Mostowski, Wojciech
By organisation
Centre for Research on Embedded Systems (CERES)
In the same journal
Lecture Notes in Computer Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 32 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf