Modular specification and verification of object-oriented programs. (English) Zbl 0998.68034

Lecture Notes in Computer Science. 2262. Berlin: Springer. xiv, 292 p. (2002).
This book deals with the language Mojave, a language for object oriented software. The language Mojave is a variant of Java that is more suited for a modular approach and includes mechanisms for verification. In chapter 2 a the language Mojave is introduced, together with an extended type system. In chapter 3 the semantics of Mojave is defined. Chapter 4 suggests the use of pre- and post conditions to specify behavioural properties. In the subsequent chapter this is applied to the ‘frame problem’ that refers to variables that remain untouched by an invoked method. The last main chapter deals with type invariants, i.e. invariants required to show the type correctness of modular Mojave specifications. The book is a typical product of the ‘formal approach’ to software. It defines a rather complex basic framework and provides the ingredients that in principle allow to specify systems and check properties and types. However, the book does not address the issue of application to slightly more complex problems, and as such is not convincing regarding the applicability of the framework.


68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68-02 Research exposition (monographs, survey articles) pertaining to computer science


JML; LARCH; Virginity