TY - JOUR
T1 - Behavioral subtyping, specification inheritance, and modular reasoning
AU - Leavens, Gary T.
AU - Naumann, David A.
N1 - Publisher Copyright:
© 2015 ACM.
PY - 2015/8/1
Y1 - 2015/8/1
N2 - 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.
AB - 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.
KW - Behavioral subtyping
KW - Dynamic dispatch
KW - Eiffel language
KW - JML language
KW - Modularity
KW - Predicate transformer
KW - Refinement
KW - Specification
KW - Specification inheritance
KW - State transformer
KW - Supertype abstraction
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=84939839513&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84939839513&partnerID=8YFLogxK
U2 - 10.1145/2766446
DO - 10.1145/2766446
M3 - Article
AN - SCOPUS:84939839513
SN - 0164-0925
VL - 37
JO - ACM Transactions on Programming Languages and Systems
JF - ACM Transactions on Programming Languages and Systems
IS - 4
M1 - 13
ER -