| Abstract(chinese) | 第1-6页 |
| Abstract | 第6-11页 |
| List of Figures | 第11-12页 |
| List of Tables | 第12-13页 |
| Chapter 1 Introduction | 第13-27页 |
| ·Formal Semantics Methodologies | 第13-18页 |
| ·Operational Semantics | 第14-16页 |
| ·Denotational Semantics | 第16页 |
| ·Axiomatic Semantics | 第16-18页 |
| ·Temporal Logic and Temporal Logic Programming | 第18-24页 |
| ·Temporal Logic | 第18-19页 |
| ·Temporal Logic Programming | 第19-21页 |
| ·Existing Problems | 第21-24页 |
| ·Contributions | 第24-25页 |
| ·Thesis Organization | 第25-27页 |
| Chapter 2 Projection Temporal Logic | 第27-39页 |
| ·Propositional Projection Temporal Logic | 第27-29页 |
| ·First Order Projection Temporal Logic | 第29-38页 |
| ·Syntax and Semantics | 第29-31页 |
| ·Satisfaction and Validity | 第31-32页 |
| ·Derived Formulas and Logic Laws | 第32-34页 |
| ·Replacement of Variables | 第34-38页 |
| ·Conclusion | 第38-39页 |
| Chapter 3 Programming Language MSVL | 第39-49页 |
| ·The History of MSVL | 第39页 |
| ·Framing | 第39-41页 |
| ·MSVL Programs | 第41-48页 |
| ·Expressions and Statements | 第41-46页 |
| ·Derived Constructs | 第46-48页 |
| ·Data Structures | 第48页 |
| ·Conclusion | 第48-49页 |
| Chapter 4 Minimal Model Semantics of MSVL | 第49-69页 |
| ·The Minimal Satisfaction Relation | 第49-51页 |
| ·Normal Form of Framed Programs | 第51-60页 |
| ·Existence Theorem of Minimal Models | 第60-64页 |
| ·Least Fixed Point Theorem | 第60-61页 |
| ·Existence Theorem | 第61-64页 |
| ·Examples | 第64-68页 |
| ·Conclusion | 第68-69页 |
| Chapter 5 Operational Semantics of MSVL | 第69-99页 |
| ·Notation | 第69-71页 |
| ·Evaluation of Expressions | 第71-72页 |
| ·State Reduction | 第72-83页 |
| ·Semantic Equivalence Rules | 第72-74页 |
| ·Transition Rules within One State | 第74-77页 |
| ·Properties for State Reduction | 第77-83页 |
| ·Interval Reduction | 第83-84页 |
| ·Consistency between Minimal Model and Operational Semantics | 第84-95页 |
| ·Consistency for Finite Models | 第84-87页 |
| ·Consistency for Infinite Models | 第87-90页 |
| ·Nondeterministic Framed Programs | 第90-95页 |
| ·An Interpreter for MSVL | 第95-98页 |
| ·Conclusion | 第98-99页 |
| Chapter 6 Axiomatic Semantics of MSVL | 第99-125页 |
| ·The Assertion Language | 第99-100页 |
| ·State Axioms and State Inference Rules | 第100-110页 |
| ·Axioms and Inference Rules over Intervals | 第110-114页 |
| ·Soundness and Completeness | 第114-120页 |
| ·Soundness | 第114-117页 |
| ·Completeness | 第117-120页 |
| ·Verification of Mutual Exclusion | 第120-124页 |
| ·Conclusion | 第124-125页 |
| Chapter 7 Conclusions and Future Works | 第125-127页 |
| ·Conclusions | 第125-126页 |
| ·Future Works | 第126-127页 |
| Acknowledgements | 第127-128页 |
| References | 第128-138页 |
| Finished Papers | 第138-139页 |
