Temporal logic is gaining recognition as an attractive and versatile formalism for rigorously specifying and reasoning about computer programs, digital circuits and message-passing systems. This book introduces Tempura, a programming language based on temporal logic. Tempura provides a way of directly executing suitable temporal logic specifications of digital circuits, parallel programs and other dynamic systems. Since every Tempura statement is also a temporal formula, the entire temporal logic formalism can be used as the assertion language and semantics. One result is that Tempura has the two seemingly contradictory properties of being a logic programming language and having imperative constructs such as assignment statements.The presentation investigates Interval Temporal Logic, a formalism with conventional temporal operators such as  (next) and 2 (always) as well as lesser known ones such as chop. This provides the basis for Tempura. The design of an interpreter for Tempura is also included as are a variety of sample Tempura programs illustrating how to model both hardware and software.

Скачать книгу бесплатно (pdf, 491 Kb)

---

Читать «Executing Temporal Logic Programs»