Modular specification and verification of object-oriented programs (Q5960651)

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.