The Object Oriented Language: Semantics, Specification And Verification

Object Orientation (OO) greatly changes the development of software indus-try. It is and will be, for a longtime, one of the mainstream techniques in softwaredevelopment. Recently, due to the even higher demands on the reliability and cor-rectness of software systems (and in general, computer-based systems), developingpowerful and useful frameworks for specifying and verifying OO programs becomesmore urgent. For developing such frameworks, two mutually dependent issues mustbe considered: (1) a formal semantics for OO programs as the basis for verifica-tion, which should be powerful enough thus can capture the desired behaviors ofvarious useful programs, and abstract enough so researchers do not su?er from theimplementation details; (2) useful specification and verification techniques, whichcan support modular verification, thus o?er scalability to program verification.In this paper, we investigate above two problems with a model languageμJava,and focus on developing practical specification and verification system for OO pro-grams.μJava is a su?cient large subset of sequential Java covering most importantOO features, including reference types, subtypes, inheritance, dynamic binding, andsharing based parameters for methods, etc, thus is a good model for our study. This paper presents a generic OO storage model, and defines an object-orientedSeparation Logic (OOSL) to describe OO programs'states. Based on this logic,we develop a Weakest Precondition (WP) semantics forμJava, show it has manygood properties, and we prove it is both sound and complete respect toμJava'soperational semantics. Then we use the WP semantics as a theoretical tool toformalize and study some important issues in OO program verification, such asmethod specification, object invariant and behavioral subtyping and so on.Based on above work, we try to develop a practical verification framework.We expandμJavaby adding specification languages , so we can specify behaviors ofprogram. And we develop a framework to verify whether aμJava program satisfiesits specification. Our framework supports modular specification and verification,and avoid re-verifying inherited methods. We use some typical examples to showthat how to specify and verify OO programs with our framework. We also providea detailed comparison with other researchers'work.This paper touches many hot topics nowadays, including Separation Logic,abstract specification, modular verification and so on. In these topics, we keep instep with academic frontiers, and propose our own points. On the other hand,we also show our new knowledge and ideas in some longtime concerned issues,for example, OO storage model, object invariants. We argue that theories andtechniques presented in this paper catch essential OO features, and they are easyto understand, and close to practice. These theories and techniques maybe a goodguide for practical verification tools for OO programs.