LePUS3 and Class-Z Home Page

Visual representations of evidence should be governed by principles of reasoning: Clear and precise seeing becomes as one with clear and precise thinking.
-- Edward R. Tufte

Codecharts: Roadmaps and Blueprints for Object-Oriented Programs (Wiley/Blackwell, 2011)

LePUS3 is a visual object-oriented design description language: a notation for for modelling and visualizing object-oriented programs at any level of abstraction. LePUS3 is tailored to allow tool support in software modelling, fully automated design verification, and software visualization. A diagram in LePUS3 is called a 'Codechart'. Class-Z is the symbolic counterpart to LePUS3: each LePUS3 Codechart has an equivalent Class-Z schema.

About LePUS3 and Class-Z
Tutorial: Object-Oriented Modelling with LePUS3 and Class-Z [.pdf][.ppt]
Legend: Key to LePUS3 and Class-Z Symbols
Reference Manual for LePUS3 & Class-Z

Modelling design patterns:

Modelling design patterns, Chapter 11 of Codecharts: Roadmaps and Blueprints of Object-Oriented Programs
The 'Gang of Four' Companion: Formal specification of design patterns in LePUS3 and Class-Z
Composite pattern: Implementation in Java's Abstract Windowing Toolkit--AWT

Modelling programs and class libraries:

Java 3D 1.5.2 API
java.awt (Java SDK 1.4)
JDom
JGraph
Widget Factories: implementation of the Abstract Factory pattern)
Collections and Iterators in java.util: implementation of the Iterator pattern (Java SDK 1.4)

Modelling application frameworks

Java Remote Method Invocation (toy example)
Enterprise JavaBeans
JUnit

Verification: Sample models and Abstract Semantics for Java 1.4 [.pdf]

Part I: Abstract Semantics for Java 1.4 Programs
Part II: Sample Models
Case study: The Iterator pattern

Links:

The Two-Tier Programming Project: Tool support in software specification, verification, and visualization