Codecharts: Roadmaps and blueprints for object-oriented programs

Chapter 3

An Overview of Codecharts

The vices and virtues of existing modelling and specification languages examined in Chapter 1 motivate our choice of the underlying principles of LePUS3, the language of Codecharts, as follows:

1. Object-orientation
2. Visualization
3. Rigour
4. Automated verifiability
5. Scalability
6. Genericity
7. Minimality
8. Information neglect

Let us examine each one of these principles and illustrate how each manifests itself in Codecharts.

3.1 OBJECT-ORIENTATION

LePUS3 is an object-oriented design description language: It is a language of statements about the design of programs encoded in object-oriented programming languages called Codecharts. More specifically, we may divide the subjects of LePUS3 specifications into three broad categories:

1. Programs and Class Libraries. Codecharts can serve as roadmaps for existing implementations and blueprints for hypothetical ones encoded in various class-based programming languages. Verification proceeds by indicating the meaning of the terms in the symbols (e.g., what CollectionsHrc stands for).

   

   Codechart 2. Collections and their iterators in java.util (Chapter 7)

2. Design Motifs. Codecharts were tailored to articulate object-oriented design patterns, in particular the Gang of Four design patterns (Chapter 11). Verification normally proceeds by indicating which parts of the program are intended to serve as the implementation of the pattern ...