Dynamic Dispatch for Method Contracts through Abstract Predicates

Wojciech Mostowski, Mattias Ulbrich

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    3 Citations (Scopus)
    29 Downloads (Pure)


    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. 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.
    Original languageUndefined
    Title of host publicationProceedings of the 14th International Conference on Modularity (MODULARITY 2015)
    Place of PublicationNew York
    PublisherAssociation for Computing Machinery (ACM)
    Number of pages8
    ISBN (Print)978-1-4503-3249-1
    Publication statusPublished - 16 Mar 2015
    Event14th International Conference on Modularity (MODULARITY 2015), Fort Collins, CO, USA: Proceedings of the 14th International Conference on Modularity (MODULARITY 2015) - New York
    Duration: 16 Mar 2015 → …

    Publication series

    NameMODULARITY 2015


    Conference14th International Conference on Modularity (MODULARITY 2015), Fort Collins, CO, USA
    CityNew York
    Period16/03/15 → …


    • EWI-26141
    • JML
    • Abstract predicates
    • IR-96984
    • Design By Contract
    • Dynamic dispatch
    • METIS-312669
    • Modular specification

    Cite this