OBJ3 is a specification language based on equational logic and algebra.
Informally, equational logic is the logic of substituting equals for equals
with algebras as models and term rewriting as operational semantics.
This operational semantics make OBJ3 specifications executable allowing
the software engineer to actually run specifications in order to validate
their behavior. The rigorous mathematical foundation of the language
allows the user to actually prove or verify properties of their specifications.
"OBJ3: A Quickstart for Software Engineers" is a brief, fairly informal introduction to the system. A more complete introduction to all OBJ features is the paper "Introducing OBJ" by Goguen et. al.
Professor Goguen, the originator of OBJ, maintains a website dealing with the history of OBJ as well as systems that were derived from OBJ.
OBJ3 is an opensource product available from Kindsoftware, LLC. You can download a precompiled version of OBJ3 for Linux from this website.
The examples appearing in the OBJ3 quickstart
document can be downloaded from this site.