Report Number: CS-TR-81-865
Institution: Stanford University, Department of Computer Science
Title: Toward a unified logical basis for programming languages
Author: Tang, Chih-sung
Date: June 1981
Abstract: In recent years, more and more computer scientists have been
paying attention to temporal logic, since there are many
properties of programs that can be described only by bringing
the time parameter into consideration. But existing temporal
logic languages, such as Lucid, in spite of their
mathematical elegance, are still far from practical. I
believe that a practical temporal-logic language, once it
came into being, would have a wide spectrum of applications.
XYZ /E is a temporal-logic language. Like other logic
languages, it is a logic system as well as a programming
language. But unlike them, it can express all conventional
data structures and control structures, nondeterminate or
concurrent programs, even programs with branching-time order.
We find that the difficulties met in other logic languages
often stem from the fact that they try to deal with these
structures in a higher level. XYZ /E adopts another approach.
We divide the language into two forms: the internal form and
the external form. The former is lower level, while the
latter is higher. Just as any logic system contains rules of
abbreviation, so also in XYZ /E there are rules of
abbreviation to transform the internal form into the external
form, and vice versa. These two forms can be considered to be
different representations of the same thing. We find that
this approach can ameliorate many problems of formalization.