zbMATH — the first resource for mathematics

How to cook a complete Hoare logic for your pet OO language. (English) Zbl 1104.68428
de Boer, Frank S. (ed.) et al., Formal methods for components and objects. Second international symposium, FMCO 2003, Leiden The Netherlands, November 4–7, 2003. Revised lectures. Berlin: Springer (ISBN 3-540-22942-6/pbk). Lecture Notes in Computer Science 3188, 111-133 (2004).
Summary: This paper introduces a general methodology for obtaining complete Hoare logics for object-oriented languages. The methodology is based on a new completeness result of a Hoare logic for a procedural language with dynamically allocated variables. This new result involves a generalization of Gorelick’s seminal completeness result of the standard Hoare logic for recursive procedures with simple variables. We show how this completeness result can be generalized to existing Hoare logics for typical object-oriented concepts like method calls, sub-typing and inheritance, and dynamic binding, by transforming an encoding of these concepts into this procedural language with dynamically allocated variables.
For the entire collection see [Zbl 1060.68006].

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
68N15 Theory of programming languages
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
Eiffel; ESC/Java
Full Text: DOI