Chapter Dynamic Dispatch for Method Contracts Through Abstract Predicates
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...
Zapisane w:
| Główni autorzy: | , |
|---|---|
| Format: | Online |
| Język: | angielski |
| Wydane: |
Springer Nature
2021
|
| Hasła przedmiotowe: | |
| Dostęp online: | 644831 |
| Etykiety: |
Nie ma etykietki, Dołącz pierwszą etykiete!
|
| _version_ | 1869522983260782592 |
|---|---|
| author | Mostowski, Wojciech Ulbrich, Mattias |
| author_browse | Mostowski, Wojciech Ulbrich, Mattias |
| author_facet | Mostowski, Wojciech Ulbrich, Mattias |
| author_sort | Mostowski, Wojciech |
| collection | Directory of Open Access Books |
| description | 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. |
| format | Online |
| id | doab-20.500.12854ir-30241 |
| institution | Directory of Open Access Books |
| language | eng |
| publishDate | 2021 |
| publishDateRange | 2021 |
| publishDateSort | 2021 |
| publisher | Springer Nature |
| publisherStr | Springer Nature |
| record_format | ojs |
| spelling | doab-20.500.12854ir-302412025-05-08T07:52:27Z Chapter Dynamic Dispatch for Method Contracts Through Abstract Predicates Mostowski, Wojciech Ulbrich, Mattias dispatch encapsulation ghost dispatch encapsulation ghost Boolean data type Dynamic dispatch First-order logic Inheritance (object-oriented programming) Java Modeling Language KeY Liskov substitution principle Postcondition Predicate (mathematical logic) 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. 2021-02-10T12:58:18Z 2020-03-18 13:36:15 2020-04-01T13:03:06Z 2018-03-03 23:55 2020-03-18 13:36:15 2020-04-01T13:03:06Z 2018-02-01 23:55:55 2020-03-18 13:36:15 2020-04-01T13:03:06Z 2017 chapter 644831 OCN: 1030820407 http://library.oapen.org/handle/20.500.12657/30616 https://directory.doabooks.org/handle/20.500.12854/30241 eng open access image/jpeg image/jpeg image/jpeg image/jpeg image/jpeg Attribution 4.0 International Attribution 4.0 International Attribution 4.0 International Attribution 4.0 International Attribution 4.0 International https://library.oapen.org/bitstream/20.500.12657/30616/1/644831.pdf https://library.oapen.org/bitstream/20.500.12657/30616/1/644831.pdf https://library.oapen.org/bitstream/20.500.12657/30616/1/644831.pdf https://library.oapen.org/bitstream/20.500.12657/30616/1/644831.pdf https://library.oapen.org/bitstream/20.500.12657/30616/1/644831.pdf Springer Nature 10.1007/978-3-319-46969-0 7 10.1007/978-3-319-46969-0 7 9fa3421d-f917-4153-b9ab-fc337c396b5a Transactions on Modularity and Composition I FP7 Ideas: European Research Council 7292b17b-f01a-4016-94d3-d7fb5ef9fb79 European Research Council (ERC) EU collection 30 258405 FP7 open access |
| spellingShingle | dispatch encapsulation ghost dispatch encapsulation ghost Boolean data type Dynamic dispatch First-order logic Inheritance (object-oriented programming) Java Modeling Language KeY Liskov substitution principle Postcondition Predicate (mathematical logic) Mostowski, Wojciech Ulbrich, Mattias Chapter Dynamic Dispatch for Method Contracts Through Abstract Predicates |
| title | Chapter Dynamic Dispatch for Method Contracts Through Abstract Predicates |
| title_full | Chapter Dynamic Dispatch for Method Contracts Through Abstract Predicates |
| title_fullStr | Chapter Dynamic Dispatch for Method Contracts Through Abstract Predicates |
| title_full_unstemmed | Chapter Dynamic Dispatch for Method Contracts Through Abstract Predicates |
| title_short | Chapter Dynamic Dispatch for Method Contracts Through Abstract Predicates |
| title_sort | chapter dynamic dispatch for method contracts through abstract predicates |
| topic | dispatch encapsulation ghost dispatch encapsulation ghost Boolean data type Dynamic dispatch First-order logic Inheritance (object-oriented programming) Java Modeling Language KeY Liskov substitution principle Postcondition Predicate (mathematical logic) |
| topic_facet | dispatch encapsulation ghost dispatch encapsulation ghost Boolean data type Dynamic dispatch First-order logic Inheritance (object-oriented programming) Java Modeling Language KeY Liskov substitution principle Postcondition Predicate (mathematical logic) |
| url | 644831 |
| work_keys_str_mv | AT mostowskiwojciech chapterdynamicdispatchformethodcontractsthroughabstractpredicates AT ulbrichmattias chapterdynamicdispatchformethodcontractsthroughabstractpredicates |