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...

Ausführliche Beschreibung

Bibliographische Detailangaben

Hauptverfasser:	Mostowski, Wojciech, Ulbrich, Mattias
Format:	Online
Sprache:	Englisch
Veröffentlicht:	Springer Nature 2021
Schlagworte:	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)
Online-Zugang:	644831
Tags:	Tag hinzufügen Keine Tags, Fügen Sie das erste Tag hinzu!