This has been a long-term project, studying the semantics of object-oriented OO programming languages and how to specify and verify them in a modular way. We found that the notion of behavioral subtyping is both necessary and sufficient for supertype abstraction: that is, reasoning about a program (with subtyping) using static type information and the specifications associated with the static type information. In a nutshell, subtypes must all obey the specifications of their supertypes to make reasoning using the supertypes’ specifications valid.
Principal Investigator
- Gary Leavens, Ph.D.
- Professor of Computer Science
- leavens@ucf.edu