An illustrated guide to the model theory of supertype abstraction and behavioral subtyping

Gary T. Leavens, David A. Naumann

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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.

Original languageEnglish
Title of host publicationEngineering Trustworthy Software Systems - Third International School, SETSS 2017, Tutorial Lectures
EditorsZhiming Liu, Zili Zhang, Jonathan P. Bowen
Pages39-88
Number of pages50
DOIs
StatePublished - 2018
Event3rd School on Engineering Trustworthy Software Systems, SETSS 2017 - Chongqing, China
Duration: 17 Apr 201722 Apr 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11174 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd School on Engineering Trustworthy Software Systems, SETSS 2017
Country/TerritoryChina
CityChongqing
Period17/04/1722/04/17

Keywords

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

Fingerprint

Dive into the research topics of 'An illustrated guide to the model theory of supertype abstraction and behavioral subtyping'. Together they form a unique fingerprint.

Cite this