An Illustrated Guide To The Model Theory Of Supertype Abstraction And Behavioral Subtyping

Keywords

Behavioral subtyping; Hoare-style verification; JML specification language; Object-oriented programming; Specification inheritance; Supertype abstraction

Abstract

Object-oriented (OO) programs, which use subtyping and dynamic dispatch, make specification and verification difficult because the code executed by a method call may dynamically be dispatched to an overriding method in any subtype, even ones that did not exist at the time the program was specified. Modular reasoning for such programs means allowing one to add new subtypes to a program without re-specifying and re-verifying it. In a 2015 ACM TOPLAS paper we presented a model-theoretic characterization of a Hoare-style modular verification technique for sequential OO programs called “supertype abstraction,” defined behavioral subtyping, and proved that behavioral subtyping is both necessary and sufficient for the validity of supertype abstraction. The present paper is aimed at graduate students and other researchers interested in formal methods and gives a comprehensive overview of our prior work, along with the motivation and intuition for that work, with examples.

Publication Date

1-1-2018

Publication Title

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Volume

11174 LNCS

Number of Pages

39-88

Document Type

Article; Proceedings Paper

Personal Identifier

scopus

DOI Link

https://doi.org/10.1007/978-3-030-02928-9_2

Socpus ID

85056813569 (Scopus)

Source API URL

https://api.elsevier.com/content/abstract/scopus_id/85056813569

This document is currently not available here.

Share

COinS