×

zbMATH — the first resource for mathematics

Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited. (English) Zbl 1064.68543
Eriksson, Lars-Henrik (ed.) et al., FME 2002: Formal methods - getting IT right. International symposium of formal methods Europe, Copenhagen, Denmark, July 22–24, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43928-5). Lect. Notes Comput. Sci. 2391, 89-105 (2002).
Summary: We define NanoJava, a kernel of Java tailored to the investigation of Hoare logics. We then introduce a Hoare logic for this language featuring an elegant approach for expressing auxiliary variables: by universal quantification on the outer logical level. Furthermore, we give simple means of handling side-effecting expressions and dynamic binding within method calls. The logic is proved sound and (relatively) complete using Isabelle/HOL.
For the entire collection see [Zbl 0997.68675].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N15 Theory of programming languages
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
Isabelle/HOL; JML
PDF BibTeX XML Cite
Full Text: Link