System support for modular order-sorted Horn clause specifications

The authors present an overview of CEC, a rewrite rule laboratory for order-sorted specifications with conditional equations. CEC differs from related systems, such as OBJ-3, in that it can check or achieve by completion the semantic prerequisites for correct operational execution of specifications by conditional term rewriting. CEC supports the modular structure of specifications in two ways. Its speculation browser allows accessing, editing, and administrating the modules of a specification through a highly interactive user interface. The completion procedure, apart from transforming a specification into executable rewrite code, will find the inconsistencies, if any, between the formal and actual parameters of generic specifications. CEC can handle a large class of conditional equations with extra variables in the condition without having to resort to inefficient goal solving methods at rewrite time