Executing Temporal Logic Programs

Ben C. Moszkowski9780521310994, 0521310997

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.

---

Table of contents :
Abstract……Page 2
Table of Contents……Page 4
0 Note about this version……Page 12
1 Introduction……Page 13
1.1 Organization of Presentation……Page 14
2.1 Background……Page 15
2.2 Syntax of the Logic……Page 16
2.2.2 Syntax of formulas……Page 17
2.3 Models……Page 18
2.4 Interpretation of Expressions and Formulas……Page 19
2.5 Satisfiability and Validity……Page 20
3.1 Boolean Operators……Page 22
3.2 The Operator……Page 23
3.4 The Operators gets and stable……Page 24
3.5 The Operator halt……Page 25
3.7 The Operator……Page 26
4 Programming in Temporal Logic……Page 28
4.1 Syntax of Tempura……Page 29
4.1.2 Expressions……Page 30
4.2 Some Other Statements……Page 31
4.3 Determinism……Page 32
5.1 Static Variables……Page 33
5.2 Quantified Formulas……Page 34
5.3 Enlarging the Data Domain……Page 35
5.5 Bounded Quantification……Page 37
5.6 The Operator fin……Page 38
5.7 Temporal Assignment……Page 39
5.8.2 Expressions……Page 40
5.8.3 Statements……Page 41
6.1 Syntax and Semantics of chop……Page 42
6.2 Discussion of the Operator chop……Page 43
6.3 Simple For-Loops……Page 44
6.5 While-Loops and Related Constructs……Page 45
6.6 Deriving For-Loops and While-Loops……Page 46
6.7 The Construct skip……Page 47
6.8 Incorporating these Constructs into Tempura……Page 48
7.1 Tree Summation……Page 50
7.1.1 Serial solution……Page 51
7.1.2 Parallel solution……Page 52
7.1.3 Correctness and performance……Page 55
7.2 Partitioning a List……Page 56
7.2.1 Correctness of partition_list……Page 58
7.3 Quicksort……Page 59
7.3.1 Explanation of quick_partition……Page 61
7.3.3 Parallel quicksort……Page 63
7.4 A Multiplication Circuit……Page 64
7.5 Pulse Generation……Page 66
7.6 Testing a Latch……Page 68
7.7 Synchronized Communication……Page 72
8 An Interpreter for Tempura……Page 76
8.2 Basic Execution Algorithm……Page 78
8.3 Description of the Procedure execute_single_state……Page 79
8.4.1 Implementing the statements true and false……Page 81
8.4.3 Implementing empty and more……Page 82
8.4.7 Implementing implication……Page 83
8.6 Implementing Expressions……Page 84
8.7.3 Implementing list, fixed_list and stable_struct……Page 85
8.7.5 Implementing subscripts……Page 86
8.7.7 Implementing existential quantification……Page 87
8.7.10 Implementing predicate and function definitions……Page 88
8.7.11 Implementing predicate and function invocations……Page 89
8.8.2 Implementing iterative operators……Page 90
8.9 Alternative Interpreters……Page 91
8.9.3 Single-pass processing……Page 92
8.9.6 Redundant assignments……Page 93
8.9.9 Call-by-name……Page 94
9.1 Temporal Projection……Page 96
9.1.1 Incorporating proj in Tempura……Page 98
9.2 Lambda Expressions and Pointers……Page 100
9.2.2 Pointers……Page 101
9.4 The prefix Construct……Page 102
9.4.1 Incorporating prefix in Tempura……Page 103
9.5 Implementing these Constructs……Page 105
9.5.2 Implementing lambda expressions and pointers……Page 106
9.5.4 Implementing the prefix construct……Page 107
10.1 Experience and Further Work……Page 108
10.2.2 CCS and CSP……Page 109
10.2.3 Predicative programming……Page 110
10.2.5 The programming language Prolog……Page 111
10.2.6 Functional programming……Page 113
10.3 Other Work on Temporal Logic……Page 114
10.3.2 Generalized next operator……Page 115
10.3.4 Semantics based on transition graphs……Page 116
10.3.5 Compositional proof rules……Page 117
10.3.6 Synthesis from temporal logic……Page 118
10.3.7 Automatic verification of circuits……Page 119
10.4 Conclusions……Page 120
Bibliography……Page 121