Algebraic specification with provision for the automatic addition of error descriptions
Takeshi Hamaguchi, Masahiko Sakai, Shinichirou Yamamoto, Kiyoshi Agusa · Systems and Computers in Japan · 1997
We define a type of algebraic specification that has the capability for error handling, then give an algorithm for appending error descriptions automatically. Generally, error descriptions in algebraic specifications are so complicated that they are difficult to comprehend, and inconsistencies arise if they are written by hand. Automatic addition of error descriptions to algebraic specifications that lack such descriptions is effective and does not produce inconsistency. We introduce error constructors that represent error values as a framework for error handling. If there exists a term which is not equal to any constructor term, an equation that equalizes the term to an error constructor is appended. In order to avoid inconsistency in which the normal value and error value become equal, we distinguish three kinds of variables; variables which can be substituted only by normal terms, variables which can be substituted only by error terms, and variables which can be substituted by any term. We show the correctness of automatic error description addition; the congruence relation on normal terms is preserved after addition of the error description. © 1997 Scripta Technica, Inc. Syst Comp Jpn, 28 (1): 1–9, 1997