Algebraically modelling object-orientated programs.

We explore the process of building algebraic models of the behaviour of Java classes. A fundamental building block of object-oriented programs is the class that can typically contain multiple fields, constructors, and methods. In Java a programmer can control access to the various methods, fields and constructors of a class. We will be formally specifying and documenting a class' public behaviour algebraically. In practice even a simple Java class can have complex behaviour. A full algebraic specification (FAS) of a class can be complicated and hard to understand for someone who wishes to quickly ascertain the behaviour of a class. This complexity is largely as a result of machinery needed to define class behaviours that are implicit, that is behaviour that is considered part of Java's general language behaviour and defines the general structure of classes, methods, fields and constructors. However, it is unreasonable to expect a programmer to write such full specifications. Therefore we introduce the concept of an Algebraic Class Specification (ACS) that provides a much reduced version of the FAS of a class. The ACS is therefore more readable and is aimed at showing what we consider to be key information in the specification of a class that cannot be programmatically inferred from the language definition. Using the ACS we present a methodology for generating an FAS thus reducing the complexity of specification for the user. We will show that the ACS provides a reader with a clear formal understanding of a class' behaviour using a minimum of information. The ACS is designed to be human readable yet still machine readable. We will show that in order to aid users in creating specifications of classes we have mimicked the Java syntax closely in the specification syntax. We will, in addition, present a methodology for embedding the formal semantic description for a Java class within javadoc comments thus allowing Java API documentation to contain both a formal specification of the behaviour of a class and its components and an informal general textual description. These techniques have been developed by the analysis of case studies. We will demonstrate all of these techniques applied to a wide and varied range of both invented and existing examples of Java classes