This project extends the semantical foundations of object-oriented (OO) languages to cover methodologies for modular reasoning. Modular reasoning means verifying software components assuming the specification of each used component. Modularity is important for productivity and scalability, but is difficult to achieve for OO software. To support modular reasoning, researchers have proposed several methodologies that restrict programs and their specifications. The goal of this project is to provide a theoretical basis that supports practical techniques for justifying and using methodologies.
This project provides guidance for the designers of programming and specification languages, verification logics, and associated tools. The results will improve the utility and extensibility of verification tools --- a key goal of the Verified Software grand challenge. Software developers may benefit from the integration and harmonious interoperation of best-practice methodologies. This project is potentially transformative: it aims to enable combinations and customizations of methodologies by tool users, scalable to real applications.
Improved OO programming methodologies may greatly improve programming practice, especially in applications needing high assurance, reliability, and security. This will benefit society, which increasingly depends on computing systems built using OO components. Unification of methodologies and streamlining of tools also facilitates the education of software developers.
