TY  - CHAP
AU  - Mostowski, Wojciech
AU  - Ulbrich, Mattias
AB  - 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.
DO  - 10.1007/978-3-319-46969-0 7
ID  - OAPEN ID: 644831
ID  - OAPEN ID: OCN: 1030820407
KW  - dispatch
KW  - encapsulation
KW  - ghost
KW  - dispatch
KW  - encapsulation
KW  - ghost
KW  - Boolean data type
KW  - Dynamic dispatch
KW  - First-order logic
KW  - Inheritance (object-oriented programming)
KW  - Java Modeling Language
KW  - KeY
KW  - Liskov substitution principle
KW  - Postcondition
KW  - Predicate (mathematical logic)
L1  - https://library.oapen.org/bitstream/id/04c7e542-c407-433c-a1fb-26536a89b9c3/644831.pdf
LA  - English
LK  - http://library.oapen.org/handle/20.500.12657/30616
PB  - Springer Nature
PY  - 2017
TI  - Chapter Dynamic Dispatch for Method Contracts Through Abstract Predicatesnull
ER  - 
