Sciweavers

Share
FASE
2001
Springer

A Hoare Calculus for Verifying Java Realizations of OCL-Constrained Design Models

9 years 1 months ago
A Hoare Calculus for Verifying Java Realizations of OCL-Constrained Design Models
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.
Bernhard Reus, Martin Wirsing, Rolf Hennicker
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Where FASE
Authors Bernhard Reus, Martin Wirsing, Rolf Hennicker
Comments (0)
books