Department of Computer Science and Technology

Technical reports

Programming in temporal logic

Roger William Stephen Hale

July 1989, 182 pages

This technical report is based on a dissertation submitted October 1988 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Trinity College.

DOI: 10.48456/tr-173

Abstract

The idea of writing computer programs in logic is an attractive one, for such programs may be designed, verified, and implemented using a single formal language. This brings a number of practical benefits:

1. There is no room for ambiguity in the relationship between specification and implementation, and no need to learn a different language for each.

2. It is easy to test out specifications from the earliest stages of development, which avoids attempting to implement or verify an inapproptiate design.

3. Computerised tools can be applied directly to transform and verify programs, using the established machinery of mathematical logic.

4. Logic supports hierarchical design, so a large project can be divided into smaller tasks which may be designed and verified independently.

Similar benefits may be bestowed by any formal programming language, but the idea only works if the language suits the intended application. All too often the application is forced to fit the language.

In this dissertation I describe an approach that suits the development of parallel and real-time systems. The approach is based on Tempura, a deterministic programming language developed by Moszkowski from his work on hardware specification using Interval Temporal Logic (ITL). I present the formal semantics of ITL in higher-order logic, and show how programs can be transformed and verified using the HOL theorem prover. Then I show how to represent a number of familiar programming concepts in ITL. First, I show that the language of while-programs can be embedded in temporal logic; and that includes the destructive assignment statement with the usual inertial assumption. An interesting corollary is that a simple sequential program, written in Pascal, say, becomes a logic program in Tempura. More advanced concepts include parallel processes and message passing, as well as real-time phenomena such as timeouts, interrupts and traps. Each idea is experimentally tested on a suitable example, using an interpreter for Tempura. The examples range from matrix multiplication and parallel sorting, to a pipelined parser and a real-time lift-controller.

Full text

Only available on paper (could be scanned on request).

BibTeX record

@TechReport{UCAM-CL-TR-173,
  author =	 {Hale, Roger William Stephen},
  title = 	 {{Programming in temporal logic}},
  year = 	 1989,
  month = 	 jul,
  institution =  {University of Cambridge, Computer Laboratory},
  address =	 {15 JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom,
          	  phone +44 1223 763500},
  doi = 	 {10.48456/tr-173},
  number = 	 {UCAM-CL-TR-173}
}