Claesen / Gordon Higher Order Logic Theorem Proving and its Applications

Proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications - HOL '92 Leuven, Belgium, 21-24 September 1992
1. Auflage 2014
ISBN: 978-1-4832-9840-5
Verlag: Elsevier Science & Techn.
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, Band Volume 20, 582 Seiten, Web PDF

Reihe: IFIP Transactions A: Computer Science and Technology

The HOL system is a higher order logic theorem proving system implemented at Edinburgh University, Cambridge University and INRIA. Its many applications, from the verification of hardware designs at all levels to the verification of programs and communication protocols are considered in depth in this volume. Other systems based on higher order logic, namely Nuprl and LAMBDA are also discussed. Features given particular consideration are: novel developments in higher order logic and its implementations in HOL; formal design and verification methodologies for hardware and software; public domain availability of the HOL system. Papers addressing these issues have been divided as follows: Mathematical Logic; Induction; General Modelling and Proofs; Formalizing and Modelling of Automata; Program Verification; Hardware Description Language Semantics; Hardware Verification Methodologies; Simulation in Higher Order Logic; Extended Uses of Higher Order Logic. Academic and industrial researchers involved in formal hardware and software design and verification methods should find the publication especially interesting and it is hoped it will also provide a useful reference tool for those working at software institutes and within the electronics industries.

Autoren/Hrsg.

Claesen, L. J. M.

Gordon, M. J. C.

Inhaltsverzeichnis

1;Front Cover;1
2;Higher Order Logic Theorem Proving and its Applications;4
3;Copyright Page;5
4;Table of Contents;10
5;Preface;6
6;Conference organization;8
7;Part 1. Mathematical Logic;16
7.1;Chapter 1. The HOL Logic Extended with Quantification overType Variables;18
7.1.1;Abstract;18
7.1.2;1 Introduction;18
7.1.3;2 Types and polymorphism in HOL;18
7.1.4;3 Motivation;19
7.1.5;4 Universal quantification over types;23
7.1.6;5 Existential quantification over types;29
7.1.7;6 Implementation;31
7.1.8;Acknowledgements;32
7.1.9;References;32
7.2;Chapter 2. A Lazy Approach to Fully-Expansive TheoremProving;34
7.2.1;Abstract;34
7.2.2;1 Introduction;34
7.2.3;2 A Simple Form of Lazy Theorem;35
7.2.4;3 Lazy Conversions;36
7.2.5;4 Lazy Theorems as an Abstract Type;41
7.2.6;5 Lazy Inference Rules;43
7.2.7;6 Three Modes of Operation;46
7.2.8;7 Results;46
7.2.9;8 A Complete Lazy System;49
7.2.10;9 Applications;49
7.2.11;10 Conclusions and Future Work;51
7.2.12;Acknowledgements;53
7.2.13;References;53
7.3;Chapter 3. Efficient Representation and Computation of Tableaux Proofs;54
7.3.1;Abstract;54
7.3.2;1 Introduction;54
7.3.3;2 The Tableau Graph Calculus CTG;56
7.3.4;3 Algorithmic aspects;63
7.3.5;4 Implement at ional details concerning extensions;67
7.3.6;5 Embedding CTG in HOL;70
7.3.7;6 Summary;71
7.3.8;References;71
7.4;Chapter 4. A Note on Interactive Theorem Proving with Theorem Continuation Functions;74
7.4.1;Abstract;74
7.4.2;1 An Example;74
7.4.3;2 The Technique;76
7.4.4;3 Another Example;79
7.4.5;Appendix: The Code;82
7.4.6;Acknowledgements;84
7.4.7;References;84
7.5;Chapter 5. A Sequent Formulation of a Logic of Predicates in HOL;86
7.5.1;Abstract;86
7.5.2;1 A Logic of Predicates;86
7.5.3;2 Applications of LP;88
7.5.4;3 Lifting Tactics and Theorem Tactics;91
7.5.5;4 Outline of Implementation;94
7.5.6;Acknowledgements;95
7.5.7;References;95
7.6;Chapter 6. A Classical Type Theory with Transfinite Types;96
7.6.1;Abstract;96
7.6.2;1 Introduction;96
7.6.3;2 The Metalanguage;98
7.6.4;3 Terms, Assertions, Environments, and Sequents;99
7.6.5;4 Set Theoretic Closure Conditions;100
7.6.6;5 Structures, Models, Denotation, Satisfaction, Validity, and Consequence;100
7.6.7;6 Abbreviations;102
7.6.8;7 Inferences, Rules of Inference, Derivations, and Derivability;103
7.6.9;8 The Monotonicity Rule;104
7.6.10;9 Closure Rules;104
7.6.11;10 Conversion Rules;104
7.6.12;11 Assignment Rules;105
7.6.13;12 Morphologies;105
7.6.14;13 Boolean Rules;106
7.6.15;14 Bases, Theoremhood, and Consistency;107
7.6.16;15 Concluding Remarks;108
7.6.17;References;108
8;Part 2: Induction;110
8.1;Chapter 7. Unification-Based Induction;112
8.1.1;Abstract;112
8.1.2;1 Introduction;112
8.1.3;2 The Proof System LAMBDA;114
8.1.4;3 Weil-Founded Induction in LAMBDA;116
8.1.5;4 Finding an Induction Approach;119
8.1.6;5 The Completion of Induction Proofs;124
8.1.7;6 Additional Problems;126
8.1.8;7 Conclusions;129
8.1.9;References;130
8.2;Chapter 8. Introducing well-founded function definitions in HOL;132
8.2.1;Abstract;132
8.2.2;1 Introduction;132
8.2.3;2 Concepts and definitions;133
8.2.4;3 The introduction scheme;134
8.2.5;4 Examples;136
8.2.6;5 Formalisation;137
8.2.7;6 Examples continued;142
8.2.8;7 Conclusions;145
8.2.9;References;146
8.3;Chapter 9. Boyer-Moore Automation for the HOL System;148
8.3.1;Abstract;148
8.3.2;1 Introduction;148
8.3.3;2 Comparison between the Boyer-Moore Prover and the HOL Implementation;149
8.3.4;3 System-Wide Features;150
8.3.5;4 The Heuristics;152
8.3.6;5 The Automatic Prover in Use;154
8.3.7;6 Results;156
8.3.8;7 Remarks;157
8.3.9;References;157
9;Part 3: General Modelling and Proofs;158
9.1;Chapter 10. Constructing the real numbers in HOL;160
9.1.1;Abstract;160
9.1.2;1 Constructing the real numbers;160
9.1.3;2 Building on the real number axioms;173
9.1.4;3 Applications;176
9.1.5;4 Conclusion and related work;177
9.1.6;5 Acknowledgements;178
9.1.7;References;179
9.2;Chapter 11. Modelling Generic Hardware Structures by Abstract Datatypes;180
9.2.1;Abstract;180
9.2.2;1 Introduction;180
9.2.3;2 The Abstract Datatype;181
9.2.4;3 Using the ADT;183
9.2.5;4 Summary and future work;189
9.2.6;References;190
9.3;Chapter 12. A Methodology for Reusable Hardware Proofs;192
9.3.1;Abstract;192
9.3.2;1 Introduction;192
9.3.3;2 Background;194
9.3.4;3 Hardware Verification with Dependent Types;195
9.3.5;4 Examples;198
9.3.6;Acknowledgements;210
9.3.7;References;210
9.4;Chapter 13. Abstract Theories in HOL;212
9.4.1;Abstract;212
9.4.2;1 Introduction;212
9.4.3;2 Abstract Theories;212
9.4.4;3 Using the Abstract Theory Package;214
9.4.5;4 Example: Group Theory;216
9.4.6;5 Conclusions;224
9.4.7;References;224
9.5;Chapter 14. Machine Abstraction in Microprocessor Specification;226
9.5.1;Abstract;226
9.5.2;1 Introduction;226
9.5.3;2 A Separation of Concerns;227
9.5.4;3 Machine Abstraction;228
9.5.5;4 An Example of Machine Abstraction;229
9.5.6;5 Advantages;235
9.5.7;6 Disadvantages;237
9.5.8;7 Application Areas;237
9.5.9;8 Conclusions;238
9.5.10;9 Acknowledgements;239
9.5.11;References;239
10;Part 4: Formalizing and Modelling ofAutomata;240
10.1;Chapter 15. A Formal Theory of Simulations Between Infinite Automata;242
10.1.1;Abstract;242
10.1.2;1 Introduction;242
10.1.3;2 The HOL logic;243
10.1.4;3 The Automaton Model;244
10.1.5;4 Simulations between Automata;248
10.1.6;5 Safety Properties;250
10.1.7;6 Automata and Safety Properties;251
10.1.8;7 Constructions on Automata;252
10.1.9;8 Extending the use of Simulation;255
10.1.10;9 Examples;257
10.1.11;10 Conclusion;260
10.1.12;References;261
10.2;Chapter 16. A Comparison between Statecharts and State Transition Assertions;262
10.2.1;Abstract;262
10.2.2;1 Introduction;262
10.2.3;2 Terminology;263
10.2.4;3 Statecharts;264
10.2.5;4 State Transition Assertions;268
10.2.6;5 An Example;269
10.2.7;6 Differences Between STAs and Statecharts;272
10.2.8;7 Issues for Connecting Real-time Specification and Verification Techniques;273
10.2.9;8 Future Work;274
10.2.10;9 Summary;275
10.2.11;10 Acknowledgements;276
10.2.12;References;276
10.3;Chapter 17. An Embedding of Timed Transition Systems in HOL;278
10.3.1;Abstract;278
10.3.2;1 Introduction;278
10.3.3;2 Example: A Traffic Light Controller;279
10.3.4;3 Real-Time Temporal Logic;282
10.3.5;4 Timed Transition Systems;284
10.3.6;5 Timed Transition Diagrams;286
10.3.7;6 Verification;289
10.3.8;References;293
10.4;Chapter 18. Formalizing a Modal Logic for CCS in the HOL Theorem Prover;294
10.4.1;Abstract;294
10.4.2;1 Introduction;294
10.4.3;2 CCS;295
10.4.4;3 Mechanization of CCS in HOL;297
10.4.5;4 Proving Modal Properties of CCS Processes in HOL;301
10.4.6;5 Related Work and Conclusions;306
10.4.7;Acknowledgements;307
10.4.8;References;307
10.5;Chapter 19. Modelling Non-Deterministic Systems in HOL;310
10.5.1;Abstract;310
10.5.2;1 Introduction;310
10.5.3;2 System Model;311
10.5.4;3 Non—Deterministic Ordering;313
10.5.5;4 Non—Deterministic Outputs;314
10.5.6;5 Conclusion;317
10.5.7;References;318
11;Part 5: Program Verification;320
11.1;Chapter 20. Mechanising some Advanced Refinement Concepts;322
11.1.1;Abstract;322
11.1.2;1 Introduction;322
11.1.3;2 The refinement calculus;323
11.1.4;3 The refinement calculus as a theory of HOL;327
11.1.5;4 Data refining loops in HOL;332
11.1.6;5 Backwards data refinement;335
11.1.7;6 Superposition refinement;337
11.1.8;7 Conclusion;340
11.1.9;References;340
11.2;Chapter 21. Deriving Correctness Properties of Compiled Code;342
11.2.1;Abstract;342
11.2.2;1. Introduction;342
11.2.3;2. Vista;344
11.2.4;3· The Relational Semantics of Vista;346
11.2.5;4. A Derived Programming Logic for Vista;348
11.2.6;5. A Verified Compiler;353
11.2.7;6. Deriving Correctness Theorems about Object Code;356
11.2.8;7. Related Work;357
11.2.9;8. Conclusions;358
11.2.10;Acknowledgements;359
11.2.11;References;359
11.3;Chapter 22. A HOL Mechanization of The Axiomatic Semantics of a Simple Distributed Programming Language¹;362
11.3.1;1 Introduction;362
11.3.2;2 Motivation;363
11.3.3;3 Axiomatic Semantics Of Message Passing;364
11.3.4;4 Our Target Distributed Language;365
11.3.5;5 The HOL Mechanization of the Semantics;367
11.3.6;6 Discussion;369
11.3.7;References;371
12;Part 6: Hardware Description LanguageSemantics;372
12.1;Chapter 23. A Formalisation of the VHDL Simulation Cycle;374
12.1.1;Abstract;374
12.1.2;1 Introduction;374
12.1.3;2 Overview of VHDL;374
12.1.4;3 Related Work;375
12.1.5;4 Philosophy;376
12.1.6;5 Intuition behind the Semantics;376
12.1.7;6 The Femto-VHDL Subset;378
12.1.8;7 The Semantic Framework;380
12.1.9;8 The Semantics of Femto-VHDL;381
12.1.10;9 Femto-VHDL in HOL;384
12.1.11;10 Conclusions and Future Work;387
12.1.12;11 Acknowledgements;388
12.1.13;References;388
12.2;Chapter 24. The Formal Semantics Definition of a Multi-Rate DSPSpecification Language in HOL ¹;390
12.2.1;Abstract;390
12.2.2;1 Introduction;390
12.2.3;2 An informal description of Silage;391
12.2.4;3 Previous work and extensions;394
12.2.5;4 HOL definitions and functions described in ML;396
12.2.6;5 Denotational semantics of expressions;401
12.2.7;6 Denotational Semantics of Definitions;401
12.2.8;7 The Denotational Semantics of Silage Functions;405
12.2.9;8 Reasoning about Silage Programs;405
12.2.10;9 Status of the work;407
12.2.11;10 Conclusions;408
12.2.12;11 Acknowledgements;408
12.2.13;References;408
12.3;Chapter 25. Design-Flow Graph Partitioning;410
12.3.1;Abstract;410
12.3.2;1 Introduction;410
12.3.3;2 Scheduling of Flow-Graphs;411
12.3.4;3 Graph Restructuring;412
12.3.5;4 Future Higher-Order Operations;417
12.3.6;5 Acknowledgements;418
12.3.7;References;418
13;Part 7: Hardware Verification Methodologies;420
13.1;Chapter 26. Implementation and Use of Annotations in HOL;422
13.1.1;Abstract;422
13.1.2;1 Introduction;422
13.1.3;2 Related work;425
13.1.4;3 Proposed approach;426
13.1.5;4 Basic structures;428
13.1.6;5 Uses of annotations;433
13.1.7;6 Conclusions and further work;437
13.1.8;Acknowledgements;441
13.1.9;References;441
13.2;Chapter 27. Towards a Formal Verification of a Floating Point Coprocessor and its Composition with a Central Processing Unit ¹;442
13.2.1;Abstract;442
13.2.2;1 Introduction;443
13.2.3;2 Verifying the composition of verified systems;444
13.2.4;3 The floating-point coprocessor architecture;448
13.2.5;4 Verifying the FPC top-level from three communicatingunits;452
13.2.6;5 Verifying the concurrent top level;457
13.2.7;6 Verifying the sequential top level;459
13.2.8;7 Discussion;461
13.2.9;References;462
13.3;Chapter 28. Deriving a Correct Computer;464
13.3.1;Abstract;464
13.3.2;1 Introduction;464
13.3.3;2 Specification;465
13.3.4;3 Axioms;466
13.3.5;4 Derivation;466
13.3.6;5 Implementation;471
13.3.7;6 Conclusion and Further Work;471
13.3.8;References;473
13.4;Chapter 29. Formal Tools for Tri-State Design in Busses;474
13.4.1;Abstract;474
13.4.2;1 Introduction;474
13.4.3;2 The LAMBDA System;475
13.4.4;3 Industrial Example;478
13.4.5;4 Conclusions;487
13.4.6;5 Acknowledgements;488
13.4.7;References;488
13.5;Chapter 30. Specification and formal synthesis of digital circuits;490
13.5.1;Abstract;490
13.5.2;1. INTRODUCTION;490
13.5.3;2. POST DESIGN VALIDATION WITH OTTER;491
13.5.4;3. FORMALLY BASED SYNTHESIS WITH LAMBDA/DIALOG;493
13.5.5;4. INTRODUCTION OF FORMAL TOOLS INTO A DESIGN FLOW;496
13.5.6;5. CONCLUSIONS;498
13.5.7;6. REFERENCES;499
14;Part 8: Simulation in Higher Order Logic;500
14.1;Chapter 31. Operational Semantics Based Formal Symbolic Simulation;502
14.1.1;Abstract;502
14.1.2;1 Introduction;502
14.1.3;2 picoELLA;504
14.1.4;3 A picoELLA Semantics and Its Embedding in Higher Order Logic;505
14.1.5;4 Examples;509
14.1.6;5 Conclusions;520
14.1.7;References;521
14.2;Chapter 32. Simulating Microprocessors from Formal Specifications;522
14.2.1;Abstract;522
14.2.2;1 Introduction;522
14.2.3;2 The Generic Interpreter Theory;523
14.2.4;3 Generic Interpreter Theory Simulator;525
14.2.5;4 Tamarack—3 Example;529
14.2.6;5 Conclusion;536
14.2.7;References;536
14.3;Chapter 33. Executing HOL Specifications: Towards an Evaluation Semantics for Classical Higher Order Logic;542
14.3.1;Abstract;542
14.3.2;1 Introduction;543
14.3.3;2 Issues in Evaluating Specifications;543
14.3.4;3 Translation Overview;544
14.3.5;4 Example Translation: Step b y Step;545
14.3.6;5 Limitations;548
14.3.7;6 Towards Evaluation Semantics;548
14.3.8;7 Summary and Future Work;549
14.3.9;Acknowledgements;549
14.3.10;References;550
14.3.11;Appendix: Example Evaluation Sessions;551
15;Part 9: Extended uses of Higher Order Logic;552
15.1;Chapter 34. Linking Other Theorem Provers to HOL Using PM: Proof Manager¹;554
15.1.1;Abstract;554
15.1.2;1.Introduction;554
15.1.3;2. Improvements to PM as a proof manager;555
15.1.4;3. Translation from HOL to other theorem provers;556
15.1.5;4. Using PM with multiple provers;559
15.1.6;5. An example of using multiple provers with PM;559
15.1.7;6. References;563
15.2;Chapter 35. Adding New Rules to an LCF-style Logic Implementation;564
15.2.1;Abstract;564
15.2.2;1 Introduction;564
15.2.3;2 The formalization of programs;566
15.2.4;3 First class environments;568
15.2.5;4 Program equivalence;569
15.2.6;5 Adding a new rule;569
15.2.7;6 Methodology, or Modelling the Growth of an Implementation;571
15.2.8;7 Related Work;572
15.2.9;8 Conclusions and Future Work;573
15.2.10;9 Acknowledgements;573
15.2.11;References;574
15.3;Chapter 36. Why We Can't have SML Style datatype Declarations in HOL;576
15.3.1;Abstract;576
15.3.2;1 Introduction;576
15.3.3;2 Differences Between SML Types and HOL Types;577
15.3.4;3 The HOL Proof that the Function Space Can't Be Embedded;578
15.3.5;4 Constraints on type constructors that don't work;580
15.3.6;5 What we can build;581
15.3.7;References;583