学位论文详细信息
An Automaton-Theoretic View of Algebraic Specifications
Computer Science;automaton;automata;algebraic specifications;varieties
Lahav, Elad
University of Waterloo
关键词: Computer Science;    automaton;    automata;    algebraic specifications;    varieties;   
Others  :  https://uwspace.uwaterloo.ca/bitstream/10012/1070/1/elahav2005.pdf
瑞士|英语
来源: UWSPACE Waterloo Institutional Repository
PDF
【 摘 要 】
We compare two methods for software specification: algebraic specifications 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 trace assertions, 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.
【 预 览 】
附件列表
Files Size Format View
An Automaton-Theoretic View of Algebraic Specifications 427KB PDF download
  文献评价指标  
  下载次数:7次 浏览次数:21次