Reus, Bernhard, Wirsing, Martin and Hennicker, Rolf (2001) A Hoare calculus for verifying Java realizations of OCL-constrained design models. In: Hussmann, Heinrich (ed.) Proceedings in Fundamental Approaches to Software Engineering: 4th International Conference, FASE 2001, Genova, Italy. Lecture Notes in Computer Science, 2029 . Springer Berlin / Heidelberg, pp. 300-317. ISBN 9783540418634

PDF Restricted to SRO admin only Download (249kB)

Abstract

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.

Item Type:	Book Section
Schools and Departments:	School of Engineering and Informatics > Informatics
Subjects:	Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Depositing User:	Chris Keene
Date Deposited:	26 Feb 2008
Last Modified:	08 Nov 2013 14:32
URI:	http://sro.sussex.ac.uk/id/eprint/1423
Google Scholar:	46 Citations

View download statistics for this item

📧 Request an update