zbMATH — the first resource for mathematics

A Hoare calculus for verifying Java realizations of OCL-constrained design models. (English) Zbl 0977.68858
Hussmann, Heinrich (ed.), Fundamental approaches to software engineering. 4th international conference, FASE 2001. Held as part of the joint European conferences on theory and practice of software, ETAPS 2001, Genova, Italy, April 2-6, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2029, 300-317 (2001).
Summary: The Object Constraint Language OCL offers a formal notation for constraining the modelling elements occurring in UML diagrams. In this paper we apply OCL for developing Java realizations of UML design models and introduce a new Hoare-Calculus for Java classes which uses OCL as assertion language. The Hoare rules are as usual for while programs, blocks and (possibly recursive) method calls. Update of instance variables is handled by an explicit substitution operator which also takes care of aliasing. For verifying a Java subsystem w.r.t. a design subsystem specified using OCL constraints we define an appropriate realization relation and illustrate our approach by an example.
For the entire collection see [Zbl 0977.68805].

68U99 Computing methodologies and applications
68T01 General topics in artificial intelligence
68T27 Logic in artificial intelligence
Full Text: Link