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

LePUS3 and Class-Z are object-oriented Design Description Languages: formal specification and modelling languages for object-oriented design which were tailored to allow tool support in automated design verification and visualization. A diagram in the LePUS3 language is called a 'Codechart'.

LePUS3 vocabulary (Legend)

Site outline

• 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

Specifying design patterns:

• The 'Gang of Four' Companion: Formal specification of design patterns in LePUS3 and Class-Z

Specifying programs and class libraries:

• Java 3D 1.5.2 API
• java.awt: implementation of the Composite pattern (Java SDK 1.4)
• JDom
• JGraph
• Widget Factories: implementation of the Abstract Factory pattern (from [Gamma et al. 1995])
• Collections and Iterators in java.util: implementation of the Iterator pattern (Java SDK 1.4)

Specifying application frameworks

• Java Remote Method Invocation (toy example)
• Enterprise JavaBeans
• JUnit

Verification: Verification of LePUS3/Class-Z Specifications: Sample models and Abstract Semantics for Java 1.4 [.pdf]

• Part I: Abstract Semantics for Java 1.4 Programs
• Part II: Sample Models
• Complete verification case study: The Iterator pattern

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