An algebraic specification and programming language member of the OBJ Family. From the homepage (see below):

[..] BOBJ is UCSD's implementation of next generation technology for algebraic specification and verification. It extends OBJ3 with support for behavioral specification and verification, and in particular, it provides circular coinductive rewriting with case analysis for conditional equations over behavioral theories, as well as behavioral rewriting over order sorted theories, modulo attributes that can be any combination of associative, commutative and identity. BOBJ also supports concurrent connection of behavioral theories, cobasis declaration, default cobasis generation, operations with multiple hidden arguments, non-congruent operations, higher order parameterized programming (with modules parameterized by modules, and instantiated with morphisms), sort constraints, and membership equational logic. In addition, BOBJ, like OBJ3, supports ordinary rewriting for order sorted equational logic (modulo attributes), as well as first order parameterized programming. These features are illustrated in examples below. BOBJ is written in pure Java and so should run on any machine. [..]

This page is linked from: OBJ Family   Sprint