TY - GEN
T1 - An illustrated guide to the model theory of supertype abstraction and behavioral subtyping
AU - Leavens, Gary T.
AU - Naumann, David A.
N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2018.
PY - 2018
Y1 - 2018
N2 - 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.
AB - 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.
KW - Behavioral subtyping
KW - Hoare-style verification
KW - JML specification language
KW - Object-oriented programming
KW - Specification inheritance
KW - Supertype abstraction
UR - http://www.scopus.com/inward/record.url?scp=85056813569&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85056813569&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-02928-9_2
DO - 10.1007/978-3-030-02928-9_2
M3 - Conference contribution
AN - SCOPUS:85056813569
SN - 9783030029272
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 39
EP - 88
BT - Engineering Trustworthy Software Systems - Third International School, SETSS 2017, Tutorial Lectures
A2 - Liu, Zhiming
A2 - Zhang, Zili
A2 - Bowen, Jonathan P.
T2 - 3rd School on Engineering Trustworthy Software Systems, SETSS 2017
Y2 - 17 April 2017 through 22 April 2017
ER -