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

<cite>[..] 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 | rewrite) with 
case analysis for conditional equations over behavioral theories, as 
well as behavioral _(rewriting | rewrite) 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 | rewrite) 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. [..]</cite>

<ul class="links">
  <li>_("Home page"|http://www-cse.ucsd.edu/groups/tatami/bobj/) at UCSD.</li>
  <li>see also _("The Tatami Project"
       | http://www-cse.ucsd.edu/groups/tatami/) (using BOBJ):
    <blockquote>The Tatami system supports distributed cooperative 
    design, specification and validation of (software and/or hardware) 
    systems, especially distributed concurrent systems. The Tatami 
    system integrates formal with informal methods, has an online 
    tutorial capability, runs over the web, and is intended to be useful 
    to ordinary software engineers. The underlying formal logic is first 
    order logic with atoms from hidden (order sorted) algebra.
    _(User interface) design has been guided by algebraic semiotics and 
    narratology, which are respectively theories of signs and of 
    stories. [..]</blockquote>
  </li>
</ul>
