Tempura(ID:1281/tem009)Language based on temporal logic. Related languages
References: Tempura is a programming language based on discrete-time Interval Temporal Logic (ITL), originally proposed by B. C. Moszkowski [1985,1986]. The roots of Tempura are in the functional programming, imperative programming, and logic programming paradigms. As a descendant of imperative programming languages, it has a "destructive" assignment statement. The programs of Tempura are a conjunction of executable ITL formulas, which are composed by the Tempura's operators. Moszkowski [1986] described an interpreter for Tempura with the details of the way in which the temporal constructs are implemented. The execution of a Tempura program is a transformation (or reduction) process. The program is repeatedly reduced according to the operations on time intervals until no interval can be divided, that is, the current subinterval contains a single state. In the above papers, some applications of Tempura including algorithm description and hardware specification are also given. This thesis extends the original Interval Temporal Logic (ITL) to include infinite models, past operators, and a new projection operator for dealing with concurrent computation, synchronous communication, and framing in the context of temporal logic programming. The thesis generalizes the original ITL to include past operators such as previous and past chop, and extends the model to include infinite intervals. A considerable collection of logic lows regarding both propositional and first order logics is formalized and proved within model theory. After that, a subset of the extended ITL is formalized as a programming language, called extended Tempura. These extensions, as in their logic basis, include infinite models, the previous operator, projection and framing constructs. A normal form for programs within the extended Tempura is demonstrated. Next, a new projection operator is introduced. In the new construct, the sub-processes are autonomous; each process has the right to specify its own interval over which it is executed. The thesis presents a framing technique for temporal logic programming, which includes the definitions of new assignments, the assignment flag and the framing operator, the formalization of algebraic properties of the framing operator, the minimal model semantics of framed programs, as well as an executable framed interpreter. The synchronous communication operator await is based directly on the proposed framing technique. It enables us to deal with concurrent computation. Based on EITL and await operator, a framed concurrent temporal logic programming language, FTLL, is formally defined within EITL. Finally, the thesis describes a framed interpreter for the extended Tempura which has been developed in SICSTUS prolog. In the new interpreter, the implementation of new assignments, the frame operator, the await operator, and the new projection operator are all included. External link: Online copy in Journal of Symbolic Computation 22(5-6) Nov./Dec. 1996 Special issue: executable temporal logics view details |