University of Sussex
Browse

File(s) under permanent embargo

A Hoare calculus for verifying Java realizations of OCL-constrained design models

chapter
posted on 2023-06-07, 14:13 authored by Bernhard ReusBernhard Reus, Martin Wirsing, Rolf Hennicker
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.

History

Publication status

  • Published

Journal

FASE '01: Proceedings of the 4th International Conference on Fundamental Approaches to Software Engineering

Publisher

Springer Berlin / Heidelberg

Volume

2029

Page range

300-317

Pages

333.0

Book title

Proceedings in Fundamental Approaches to Software Engineering: 4th International Conference, FASE 2001, Genova, Italy

ISBN

9783540418634

Series

Lecture Notes in Computer Science

Department affiliated with

  • Informatics Publications

Full text available

  • No

Peer reviewed?

  • Yes

Editors

Heinrich Hussmann

Legacy Posted Date

2008-02-26

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC