An Automaton-Theoretic View of Algebraic Specifications

Abstract

We compare two methods for software specification: <em>algebraic specifications</em> and automata. While algebraic specifications have been around since the 1970s and have been studied extensively, specification by automata is relatively new. Its origins are in another veteran method called <em>trace assertions</em>, which considers a software module as a set of traces, that is, a sequences of function executions. A module is specified by a set of canonical traces and an equivalence relation matching one of the canonical traces to each non-canonical trace. It has been recently shown that trace assertions is an equivalent method to specification by automata. In continuation of this work on trace assertions and automata, we study how automata compare with algebraic specifications. We prove that every specification using an automaton can be converted into an algebraic specification describing the same abstract data type. This conversion utilises a set of canonical words, representing states in the automaton. We next consider varieties of monoids as a heuristic for obtaining more concise algebraic specifications from automata. Finally, we discuss the opposite conversion of algebraic specifications into automata. We show that, while an automaton always exists for every abstract data type described by an algebraic specification, this automaton may not be finitely describable and therefore may not be considered as a viable method for software specification.