Object-oriented Programming Laws for Annotated Java Programs

TL;DR

This paper introduces a set of programming laws tailored for Java programs annotated with JML, facilitating transformations and refactorings while considering object-oriented features and specifications.

Contribution

It presents novel programming laws specifically designed for Java with JML, addressing the integration of object-oriented features and specifications.

Findings

Laws enable systematic program transformations.

Laws support development of complex refactorings.

Address object-oriented features with specifications.

Abstract

Object-oriented programming laws have been proposed in the context of languages that are not combined with a behavioral interface specification language (BISL). The strong dependence between source-code and interface specifications may cause a number of difficulties when transforming programs. In this paper we introduce a set of programming laws for object-oriented languages like Java combined with the Java Modeling Language (JML). The set of laws deals with object-oriented features taking into account their specifications. Some laws deal only with features of the specification language. These laws constitute a set of small transformations for the development of more elaborate ones like refactorings.