×

zbMATH — the first resource for mathematics

A syntax-directed Hoare logic for object-oriented programming concepts. (English) Zbl 1253.68087
Najm, Elie (ed.) et al., Formal methods for open object-based distributed systems. 6th IFIP WG 6.1 international conference, FMOODS 2003, Paris, France, November 19–21, 2003. Proceedings. Berlin: Springer (ISBN 3-540-20491-1/pbk). Lect. Notes Comput. Sci. 2884, 64-78 (2003).
Summary: This paper outlines a sound and complete Hoare logic for a sequential object-oriented language with inheritance and subtyping like Java. It describes a weakest precondition calculus for assignments and object-creation, as well as Hoare rules for reasoning about (mutually recursive) method invocations with dynamic binding. Our approach enables reasoning at an abstraction level that coincides with the general abstraction level of object-oriented languages.
For the entire collection see [Zbl 1029.00058].

MSC:
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
03B70 Logic in computer science
68N15 Theory of programming languages
Software:
JML
PDF BibTeX XML Cite
Full Text: DOI