Sep 28, 2015
Gary Leavens: Behavioral Subtyping, Specification Inheritance, and Modular Reasoning
This talk aims to characterize modular reasoning for object-oriented (OO) programs that use subtyping and dynamic dispatch. It gives a semantic characterization of supertype abstraction using two different semantics for a Java-like OO language. The first semantics is an accurate semantics of the language’s behavior. The second semantics mimics supertype abstraction, using static type information and method specifications to determine what a program should do. The validity of supertype abstraction is defined as having this second semantics accurately predict the behavior of programs with the dynamic semantics.
This talk is based on joint work with David A. Naumann of Stevens Institute of Technology, and is based on our paper “Behavioral Subtyping, Specification Inheritance, and Modular Reasoning” published in ACM TOPLAS, 37(4):13:1-13:88, Aug. 2015. (See http://doi.acm.org/10.1145/2766446.) The work of Gary Leavens was supported by NSF grants CNS-0808913, CCF-0916350, CCF-0916715, CCF-1017262, and CNS-1228695 David Naumann’s work was supported in part by NSF grants CCF-0915611 and CNS-1228930.