There are many specification languages, and even several concurrent specification languages. Some are executable, but most offer no testing support. Some have formal semantics, but most offer no verification support. Some are based on computation models found in programming languages and thus allow a specification to be refined into a reasonably recognizable implementation, but most are mathematical notations. An OBJC specification is executable, verifiable, and implementable. Execution is by equational rewriting. Verification is by a combination of structural induction and monitor induction. Implementation is by message passing.
The most notable contribution of this dissertation is the definition, implementation, and demonstration of OBJC. OBJC embodies a new protocol for equational message passing, which is realized as a parameterized module that can be imported into an ordinary equational specification. An operational semantics based on an abstract message-passing rewrite-rule machine and an equational semantics based on a transformation to ordinary equational semantics is given. Several example specifications are also given, including a specification of SMTP, the Internet mail protocol. These examples utilize a new equational-specification model called the client/server model. Verification of OBJC specifications is also demonstrated, and several new techniques for using a rewrite-rule system as a verification tool are presented. These include message-induction, which is a combination of structural induction and monitor induction, and a kind of symbolic evaluation that is tailored for message passing.