Higher Order Logic Theorem Proving and its Applications (eBook)

Front Cover 1
Higher Order Logic Theorem Proving and its Applications 4
Copyright Page 5
Table of Contents 10
Preface 6
Conference organization 8
Part 1. Mathematical Logic 16
Chapter 1. The HOL Logic Extended with Quantification overType Variables 18
Abstract 18
1 Introduction 18
2 Types and polymorphism in HOL 18
3 Motivation 19
4 Universal quantification over types 23
5 Existential quantification over types 29
6 Implementation 31
Acknowledgements 32
References 32
Chapter 2. A Lazy Approach to Fully-Expansive TheoremProving 34
Abstract 34
1 Introduction 34
2 A Simple Form of Lazy Theorem 35
3 Lazy Conversions 36
4 Lazy Theorems as an Abstract Type 41
5 Lazy Inference Rules 43
6 Three Modes of Operation 46
7 Results 46
8 A Complete Lazy System 49
9 Applications 49
10 Conclusions and Future Work 51
Acknowledgements 53
References 53
Chapter 3. Efficient Representation and Computation of Tableaux Proofs 54
Abstract 54
1 Introduction 54
2 The Tableau Graph Calculus CTG 56
3 Algorithmic aspects 63
4 Implement at ional details concerning extensions 67
5 Embedding CTG in HOL 70
6 Summary 71
References 71
Chapter 4. A Note on Interactive Theorem Proving with Theorem Continuation Functions 74
Abstract 74
1 An Example 74
2 The Technique 76
3 Another Example 79
Appendix: The Code 82
Acknowledgements 84
References 84
Chapter 5. A Sequent Formulation of a Logic of Predicates in HOL 86
Abstract 86
1 A Logic of Predicates 86
2 Applications of LP 88
3 Lifting Tactics and Theorem Tactics 91
4 Outline of Implementation 94
Acknowledgements 95
References 95
Chapter 6. A Classical Type Theory with Transfinite Types 96
Abstract 96
1 Introduction 96
2 The Metalanguage 98
3 Terms, Assertions, Environments, and Sequents 99
4 Set Theoretic Closure Conditions 100
5 Structures, Models, Denotation, Satisfaction, Validity, and Consequence 100
6 Abbreviations 102
7 Inferences, Rules of Inference, Derivations, and Derivability 103
8 The Monotonicity Rule 104
9 Closure Rules 104
10 Conversion Rules 104
11 Assignment Rules 105
12 Morphologies 105
13 Boolean Rules 106
14 Bases, Theoremhood, and Consistency 107
15 Concluding Remarks 108
References 108
Part 2: Induction 110
Chapter 7. Unification-Based Induction 112
Abstract 112
1 Introduction 112
2 The Proof System LAMBDA 114
3 Weil-Founded Induction in LAMBDA 116
4 Finding an Induction Approach 119
5 The Completion of Induction Proofs 124
6 Additional Problems 126
7 Conclusions 129
References 130
Chapter 8. Introducing well-founded function definitions in HOL 132
Abstract 132
1 Introduction 132
2 Concepts and definitions 133
3 The introduction scheme 134
4 Examples 136
5 Formalisation 137
6 Examples continued 142
7 Conclusions 145
References 146
Chapter 9. Boyer-Moore Automation for the HOL System 148
Abstract 148
1 Introduction 148
2 Comparison between the Boyer-Moore Prover and the HOL Implementation 149
3 System-Wide Features 150
4 The Heuristics 152
5 The Automatic Prover in Use 154
6 Results 156
7 Remarks 157
References 157
Part 3: General Modelling and Proofs 158
Chapter 10. Constructing the real numbers in HOL 160
Abstract 160
1 Constructing the real numbers 160
2 Building on the real number axioms 173
3 Applications 176
4 Conclusion and related work 177
5 Acknowledgements 178
References 179
Chapter 11. Modelling Generic Hardware Structures by Abstract Datatypes 180
Abstract 180
1 Introduction 180
2 The Abstract Datatype 181
3 Using the ADT 183
4 Summary and future work 189
References 190
Chapter 12. A Methodology for Reusable Hardware Proofs 192
Abstract 192
1 Introduction 192
2 Background 194
3 Hardware Verification with Dependent Types 195
4 Examples 198
Acknowledgements 210
References 210
Chapter 13. Abstract Theories in HOL 212
Abstract 212
1 Introduction 212
2 Abstract Theories 212
3 Using the Abstract Theory Package 214
4 Example: Group Theory 216
5 Conclusions 224
References 224
Chapter 14. Machine Abstraction in Microprocessor Specification 226
Abstract 226
1 Introduction 226
2 A Separation of Concerns 227
3 Machine Abstraction 228
4 An Example of Machine Abstraction 229
5 Advantages 235
6 Disadvantages 237
7 Application Areas 237
8 Conclusions 238
9 Acknowledgements 239
References 239
Part 4: Formalizing and Modelling ofAutomata 240
Chapter 15. A Formal Theory of Simulations Between Infinite Automata 242
Abstract 242
1 Introduction 242
2 The HOL logic 243
3 The Automaton Model 244
4 Simulations between Automata 248
5 Safety Properties 250
6 Automata and Safety Properties 251
7 Constructions on Automata 252
8 Extending the use of Simulation 255
9 Examples 257
10 Conclusion 260
References 261
Chapter 16. A Comparison between Statecharts and State Transition Assertions 262
Abstract 262
1 Introduction 262
2 Terminology 263
3 Statecharts 264
4 State Transition Assertions 268
5 An Example 269
6 Differences Between STAs and Statecharts 272
7 Issues for Connecting Real-time Specification and Verification Techniques 273
8 Future Work 274
9 Summary 275
10 Acknowledgements 276
References 276
Chapter 17. An Embedding of Timed Transition Systems in HOL 278
Abstract 278
1 Introduction 278
2 Example: A Traffic Light Controller 279
3 Real-Time Temporal Logic 282
4 Timed Transition Systems 284
5 Timed Transition Diagrams 286
6 Verification 289
References 293
Chapter 18. Formalizing a Modal Logic for CCS in the HOL Theorem Prover 294
Abstract 294
1 Introduction 294
2 CCS 295
3 Mechanization of CCS in HOL 297
4 Proving Modal Properties of CCS Processes in HOL 301
5 Related Work and Conclusions 306
Acknowledgements 307
References 307
Chapter 19. Modelling Non-Deterministic Systems in HOL 310
Abstract 310
1 Introduction 310
2 System Model 311
3 Non—Deterministic Ordering 313
4 Non—Deterministic Outputs 314
5 Conclusion 317
References 318
Part 5: Program Verification 320
Chapter 20. Mechanising some Advanced Refinement Concepts 322
Abstract 322
1 Introduction 322
2 The refinement calculus 323
3 The refinement calculus as a theory of HOL 327
4 Data refining loops in HOL 332
5 Backwards data refinement 335
6 Superposition refinement 337
7 Conclusion 340
References 340
Chapter 21. Deriving Correctness Properties of Compiled Code 342
Abstract 342
1. Introduction 342
2. Vista 344
3· The Relational Semantics of Vista 346
4. A Derived Programming Logic for Vista 348
5. A Verified Compiler 353
6. Deriving Correctness Theorems about Object Code 356
7. Related Work 357
8. Conclusions 358
Acknowledgements 359
References 359
Chapter 22. A HOL Mechanization of The Axiomatic Semantics of a Simple Distributed Programming Language¹ 362
1 Introduction 362
2 Motivation 363
3 Axiomatic Semantics Of Message Passing 364
4 Our Target Distributed Language 365
5 The HOL Mechanization of the Semantics 367
6 Discussion 369
References 371
Part 6: Hardware Description LanguageSemantics 372
Chapter 23. A Formalisation of the VHDL Simulation Cycle 374
Abstract 374
1 Introduction 374
2 Overview of VHDL 374
3 Related Work 375
4 Philosophy 376
5 Intuition behind the Semantics 376
6 The Femto-VHDL Subset 378
7 The Semantic Framework 380
8 The Semantics of Femto-VHDL 381
9 Femto-VHDL in HOL 384
10 Conclusions and Future Work 387
11 Acknowledgements 388
References 388
Chapter 24. The Formal Semantics Definition of a Multi-Rate DSPSpecification Language in HOL ¹ 390
Abstract 390
1 Introduction 390
2 An informal description of Silage 391
3 Previous work and extensions 394
4 HOL definitions and functions described in ML 396
5 Denotational semantics of expressions 401
6 Denotational Semantics of Definitions 401
7 The Denotational Semantics of Silage Functions 405
8 Reasoning about Silage Programs 405
9 Status of the work 407
10 Conclusions 408
11 Acknowledgements 408
References 408
Chapter 25. Design-Flow Graph Partitioning 410
Abstract 410
1 Introduction 410
2 Scheduling of Flow-Graphs 411
3 Graph Restructuring 412
4 Future Higher-Order Operations 417
5 Acknowledgements 418
References 418
Part 7: Hardware Verification Methodologies 420
Chapter 26. Implementation and Use of Annotations in HOL 422
Abstract 422
1 Introduction 422
2 Related work 425
3 Proposed approach 426
4 Basic structures 428
5 Uses of annotations 433
6 Conclusions and further work 437
Acknowledgements 441
References 441
Chapter 27. Towards a Formal Verification of a Floating Point Coprocessor and its Composition with a Central Processing Unit ¹ 442
Abstract 442
1 Introduction 443
2 Verifying the composition of verified systems 444
3 The floating-point coprocessor architecture 448
4 Verifying the FPC top-level from three communicatingunits 452
5 Verifying the concurrent top level 457
6 Verifying the sequential top level 459
7 Discussion 461
References 462
Chapter 28. Deriving a Correct Computer 464
Abstract 464
1 Introduction 464
2 Specification 465
3 Axioms 466
4 Derivation 466
5 Implementation 471
6 Conclusion and Further Work 471
References 473
Chapter 29. Formal Tools for Tri-State Design in Busses 474
Abstract 474
1 Introduction 474
2 The LAMBDA System 475
3 Industrial Example 478
4 Conclusions 487
5 Acknowledgements 488
References 488
Chapter 30. Specification and formal synthesis of digital circuits 490
Abstract 490
1. INTRODUCTION 490
2. POST DESIGN VALIDATION WITH OTTER 491
3. FORMALLY BASED SYNTHESIS WITH LAMBDA/DIALOG 493
4. INTRODUCTION OF FORMAL TOOLS INTO A DESIGN FLOW 496
5. CONCLUSIONS 498
6. REFERENCES 499
Part 8: Simulation in Higher Order Logic 500
Chapter 31. Operational Semantics Based Formal Symbolic Simulation 502
Abstract 502
1 Introduction 502
2 picoELLA 504
3 A picoELLA Semantics and Its Embedding in Higher Order Logic 505
4 Examples 509
5 Conclusions 520
References 521
Chapter 32. Simulating Microprocessors from Formal Specifications 522
Abstract 522
1 Introduction 522
2 The Generic Interpreter Theory 523
3 Generic Interpreter Theory Simulator 525
4 Tamarack—3 Example 529
5 Conclusion 536
References 536
Chapter 33. Executing HOL Specifications: Towards an Evaluation Semantics for Classical Higher Order Logic 542
Abstract 542
1 Introduction 543
2 Issues in Evaluating Specifications 543
3 Translation Overview 544
4 Example Translation: Step b y Step 545
5 Limitations 548
6 Towards Evaluation Semantics 548
7 Summary and Future Work 549
Acknowledgements 549
References 550
Appendix: Example Evaluation Sessions 551
Part 9: Extended uses of Higher Order Logic 552
Chapter 34. Linking Other Theorem Provers to HOL Using PM: Proof Manager¹ 554
Abstract 554
1.Introduction 554
2. Improvements to PM as a proof manager 555
3. Translation from HOL to other theorem provers 556
4. Using PM with multiple provers 559
5. An example of using multiple provers with PM 559
6. References 563
Chapter 35. Adding New Rules to an LCF-style Logic Implementation 564
Abstract 564
1 Introduction 564
2 The formalization of programs 566
3 First class environments 568
4 Program equivalence 569
5 Adding a new rule 569
6 Methodology, or Modelling the Growth of an Implementation 571
7 Related Work 572
8 Conclusions and Future Work 573
9 Acknowledgements 573
References 574
Chapter 36. Why We Can't have SML Style datatype Declarations in HOL 576
Abstract 576
1 Introduction 576
2 Differences Between SML Types and HOL Types 577
3 The HOL Proof that the Function Space Can't Be Embedded 578
4 Constraints on type constructors that don't work 580
5 What we can build 581
References 583