Behavioral subtyping, specification inheritance, and modular reasoning

Gary T. Leavens, David A. Naumann

Research output: Contribution to journalArticlepeer-review

17 Scopus citations

Abstract

Verification of a dynamically dispatched method call, E.m(), seems to depend on E's dynamic type. To avoid case analysis and allow incremental development, object-oriented program verification uses supertype abstraction. In other words, one reasons about E.m() using m's specification for E's static type. Supertype abstraction is valid when each subtype in the program is a behavioral subtype. This article semantically formalizes supertype abstraction and behavioral subtyping for a Java-like sequential language with mutation and proves that behavioral subtyping is both necessary and sufficient for the validity of supertype abstraction. Specification inheritance, as in JML, is also formalized and proved to entail behavioral subtyping.

Original languageEnglish
Article number13
JournalACM Transactions on Programming Languages and Systems
Volume37
Issue number4
DOIs
StatePublished - 1 Aug 2015

Keywords

  • Behavioral subtyping
  • Dynamic dispatch
  • Eiffel language
  • JML language
  • Modularity
  • Predicate transformer
  • Refinement
  • Specification
  • Specification inheritance
  • State transformer
  • Supertype abstraction
  • Verification

Fingerprint

Dive into the research topics of 'Behavioral subtyping, specification inheritance, and modular reasoning'. Together they form a unique fingerprint.

Cite this