Trace Rewriting Systems
Mr. Yabo Wang
Dr. David Lorge Parnas
Software Engineering Research Group
CRL, McMaster University,
Hamilton, Ontario, Canada L8S 4K1
Software modules, just as other engineering products, should have precise specifications, i.e., precise
descriptions of their externally observable behaviour. To abstractly specify the requirements on each
module's interface, we view modules as "black-boxes" and specify them by a finite state machine based
module interface specification method - the trace assertion method.
To support this method, we plan to develop a simulation tool, trace simulator, that symbolically
interprets trace assertions of trace specifications and simulates the externally observable behaviour of the
In this report, we first describe the trace assertion method. We then present a theoretical model for the
trace simulator - trace rewriting (a form of term rewriting), and study the properties of trace rewriting
systems. We show that a proper trace rewriting system is both terminating and confluent and offer some
comparisons between trace rewriting systems and general term rewriting systems.