Method for Automatically Translating Trace Specifications into Prolog

摘要

The trace method of software specification provides unambiguous, nonprocedural program specifications that are subject to rigorous proof techniques. The nonprocedural property makes it easier for a programmer to develop an implementation without being overly influenced by the form the specification takes. However, this same nonprocedural property often makes it difficult for programmers to interpret trace specifications or for users to predict the results of the specifications they design. This disadvantage can be overcome by a rapid prototyping system that enables programmers and specification writers to immediately check the requirements of a given specification. Such a prototyping system should be able to take a given trace specification and automatically translate it into executable code that satisfies the requirements of the specification. In this report we present an algorithm for translating specifications into Prolog and a method for formulating specifications so that the algorithm always produces complete programs. Therefore a program thus produced will eventually yield an answer to any query concerning the value; or legality of any given trace or the equivalence of any two given traces. We also provide a proof that property holds. Keywords; Computer languages; Programming; Automatic implementation; Formal specification; Rapid prototyping; Prolog computer language; Logic programming. (kt)