MARC details
| 000 -LEADER |
|---|
| fixed length control field |
03602naaaa2200493uu 4500 |
| 001 - CONTROL NUMBER |
|---|
| control field |
https://directory.doabooks.org/handle/20.500.12854/30241 |
| 005 - DATE AND TIME OF LATEST TRANSACTION |
|---|
| control field |
20220714162809.0 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
978-3-319-46969-0 7 |
| 024 7# - OTHER STANDARD IDENTIFIER |
|---|
| Standard number or code |
10.1007/978-3-319-46969-0 7 |
| Terms of availability |
doi |
| 041 0# - LANGUAGE CODE |
|---|
| Language code of text/sound track or separate title |
English |
| 042 ## - AUTHENTICATION CODE |
|---|
| Authentication code |
dc |
| 072 #7 - SUBJECT CATEGORY CODE |
|---|
| Subject category code |
U |
| Source |
bicssc |
| 100 1# - MAIN ENTRY--PERSONAL NAME |
|---|
| Personal name |
Mostowski, Wojciech |
| Relator code |
auth |
| 9 (RLIN) |
1575056 |
| 245 10 - TITLE STATEMENT |
|---|
| Title |
Chapter Dynamic Dispatch for Method Contracts Through Abstract Predicates |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) |
|---|
| Name of publisher, distributor, etc |
Springer Nature |
| Date of publication, distribution, etc |
2017 |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Extent |
1 electronic resource (30 p.) |
| 506 0# - RESTRICTIONS ON ACCESS NOTE |
|---|
| Terms governing access |
Open Access |
| Source of term |
star |
| Standardized terminology for access restriction |
Unrestricted online access |
| 520 ## - SUMMARY, ETC. |
|---|
| Summary, etc |
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. |
| 536 ## - FUNDING INFORMATION NOTE |
|---|
| Text of note |
FP7 Ideas: European Research Council |
| 540 ## - TERMS GOVERNING USE AND REPRODUCTION NOTE |
|---|
| Terms governing use and reproduction |
Creative Commons |
| -- |
https://creativecommons.org/licenses/by/4.0/ |
| -- |
cc |
| -- |
https://creativecommons.org/licenses/by/4.0/ |
| 546 ## - LANGUAGE NOTE |
|---|
| Language note |
English |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Computing & information technology |
| Source of heading or term |
bicssc |
| 9 (RLIN) |
919507 |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
dispatch |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
encapsulation |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
ghost |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
dispatch |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
encapsulation |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
ghost |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
Boolean data type |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
Dynamic dispatch |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
First-order logic |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
Inheritance (object-oriented programming) |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
Java Modeling Language |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
KeY |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
Liskov substitution principle |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
Postcondition |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
Predicate (mathematical logic) |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Ulbrich, Mattias |
| Relator code |
auth |
| 9 (RLIN) |
1575057 |
| 773 10 - HOST ITEM ENTRY |
|---|
| Host Biblionumber |
OAPEN Library ID: 644831 |
| Title |
Transactions on Modularity and Composition I |
| Control subfield |
nnaa |
| 856 40 - ELECTRONIC LOCATION AND ACCESS |
|---|
| Host name |
www.oapen.org |
| Uniform Resource Identifier |
<a href="https://library.oapen.org/bitstream/20.500.12657/30616/1/644831.pdf">https://library.oapen.org/bitstream/20.500.12657/30616/1/644831.pdf</a> |
| -- |
0 |
| Public note |
DOAB: download the publication |
| 856 40 - ELECTRONIC LOCATION AND ACCESS |
|---|
| Host name |
www.oapen.org |
| Uniform Resource Identifier |
<a href="https://library.oapen.org/bitstream/20.500.12657/30616/1/644831.pdf">https://library.oapen.org/bitstream/20.500.12657/30616/1/644831.pdf</a> |
| -- |
0 |
| Public note |
DOAB: download the publication |
| 856 40 - ELECTRONIC LOCATION AND ACCESS |
|---|
| Host name |
www.oapen.org |
| Uniform Resource Identifier |
<a href="https://library.oapen.org/bitstream/20.500.12657/30616/1/644831.pdf">https://library.oapen.org/bitstream/20.500.12657/30616/1/644831.pdf</a> |
| -- |
0 |
| Public note |
DOAB: download the publication |
| 856 40 - ELECTRONIC LOCATION AND ACCESS |
|---|
| Host name |
www.oapen.org |
| Uniform Resource Identifier |
<a href="https://directory.doabooks.org/handle/20.500.12854/30241">https://directory.doabooks.org/handle/20.500.12854/30241</a> |
| -- |
0 |
| Public note |
DOAB: description of the publication |
