BOBJ

[..] 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. [..]

• Home page at UCSD.
• see also The Tatami Project (using BOBJ):

  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. [..]

This page is linked from: OBJ Family   Sprint