Behavioral Subtyping, Specification Inheritance, And Modular Reasoning

Keywords

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

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.

Publication Date

8-1-2015

Publication Title

ACM Transactions on Programming Languages and Systems

Volume

37

Issue

4

Document Type

Article

Personal Identifier

scopus

DOI Link

https://doi.org/10.1145/2766446

Socpus ID

84939839513 (Scopus)

Source API URL

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

This document is currently not available here.

Share

COinS