Paper Info
Title
Dynamic dispatch for method contracts through abstract predicates
Abstract
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.
Year
DOI
Venue
2015
10.1145/2724525.2724574
MODULARITY
Keywords
Field
DocType
design by contract,modular specification,abstract predicates,jml,software/program verification,dynamic dispatch,requirements/specifications
Programming language,Expression (mathematics),Computer science,Design by contract,Dynamic dispatch,Formal specification,First-order logic,Dynamic logic (digital electronics),Modular design,Semantics
Conference
Volume
Citations 
PageRank 
1
2
0.36
References 
Authors
33
2
Name
Order
Citations
PageRank
Wojciech Mostowski121.38
Mattias Ulbrich223.07