An introduction to OBJ 3

Abstract

OBJ 3 is a new implementation of the OBJ language, with a new efficient operational semantics based on order-sorted term-rewriting. OBJ is a declarative language, with mathematical semantics given by order-sorted equational logic; its statements are equations that state properties the solution should have; i.e., they describe the problem to be solved. In addition, OBJ has a uniquely powerful generic module mechanism, including non-executable “theories” as well as executable “objects,” plus “module expressions” that describe and construct whole subsystems. OBJ also has user-definable abstract data types with user-definable mixfix syntax and a powerful and flexible type system that supports overloading and subtypes. OBJ is thus a wide-spectrum language that elegantly integrates coding, specification and design into a single framework.