Theory of Deterministic Trace-Assertion Specications ?
Janusz Brzozowski, J Helmut · 2004
A software module is an abstraction of a program: it has a well dened functionality, operations by which the environment ac- cesses the program, and outputs. Traces are sequences of operations. Trace assertions constitute a particular formalism for abstract specica- tion of software modules. Certain traces are identied as canonical, and all traces are grouped in equivalence classes, each of which is represented by a unique canonical trace. Trace equivalence captures the observational indistinguishability of traces. A rewriting system transforms any trace to its canonical equivalent. A module can often be conveniently described by a (nite or innite) automaton. In this paper we consider only deterministic connected au- tomata. We show that any such automaton can be specied by canonical traces and trace equivalence; conversely, any set of canonical traces to- gether with a trace equivalence uniquely denes an automaton. For each state of an automaton, we select an arbitrary trace leading to that state as its canonical trace. Constructing trace equivalence amounts to nding a set of generators for state-equivalence, where two traces are state-equivalent if they lead to the same state. We present a simple algo- rithm for nding such a set of generators. Directly from these generators, we derive a rewriting system which yields a deterministic algorithm for transforming any trace to its canonical representative. This system is always conuen t, and it is Noetherian (has only nite derivations) if and only if the set of canonical traces is prex-con tinuous (a set is prex- continuous if whenever a word w and a prex u of w are in the set, then all the prexes of w longer than u are also in the set). Each prex- continuous set corresponds to a spanning forest of the automaton and vice versa. We apply our algorithms to specify several commonly used modules.