Executing Trace Specifications Using Prolog

摘要

Trace specifications have some desirable properties that most specifications lack: they are abstract, so they need not impose unnecessary constraints on the implementor; and they are formal, so they can be understood unambiguously and can be rigorously tested for consistency, totalness, and correctness of implementation. Nevertheless, understanding trace specifications and translating them to computer programs are significant tasks. This report documents experiments in translating trace specifications to Prolog so that they can be executed directly. The seclection of Prolog over other possible languages is discussed, and several example specifications and their translations are presented. Some generally useful Prolog predicates are gleaned from these examples, and difficulties encountered in performing the translations are described. On the way, an implementation-free semantics for a subset of Prolog is given. The report concludes with a discussion of possibilities for mechanically translating trace specifications to Prolog. Keywords: Logic programming. (Author)