Syntax-directed semantics-supported editing of algebraic specifications

This paper describes the functions performed by a program written to support syntax-directed editing of Emily algebraic specifications in the GNU EMACS text editor. The Emily algebraic specification language is a strongly-typed functional language which can be used to define abstract data types. The Emily language uses term rewriting rules to perform computations and is based on the algebraic specification language in [ANT089].

The program uses the binary choice method and recursive reduction, which guarantee that the resultant specifications satisfy the properties of completeness, parsimony, and termination ([ANT089]). The program is written in EMACS LISP under the UNIX operating system, with subprocesses written in C. An Emily translator, written in C, is called to parse the specifications and check for certain types of errors [SHAW89].