形式語義是對軟件系統(tǒng)進行形式化驗證和分析的重要理論基礎。程序語言的語義可以幫助人們更好的理解、執(zhí)行、分析軟件系統(tǒng)。操作語義有助于語言的實現(xiàn),公理語義有利于程序的驗證,指稱語義在強大的數(shù)學理論支持下為程序的含義提供了精確的數(shù)學描述。 時序邏輯程序設計是一種新型的程序設計范式,程序的具體執(zhí)行和性質的描述可以在同一邏輯框架內表示,適用于并發(fā)系統(tǒng)的建模、模擬和驗證。盡管研究人員開發(fā)了相關的解釋器來執(zhí)行各類時序邏輯程序語言,時序邏輯及其可執(zhí)行子集被廣泛地應用于系統(tǒng)的規(guī)范和驗證中,但是到目前為止,至少在區(qū)間時序邏輯程序語言中,還沒有一套系統(tǒng)而完整的形式語義。本文以區(qū)間時序邏輯程序語言MSVL為研究對象,分別從模型語義、操作語義、公理語義三條主線來研究區(qū)間時序邏輯程序的形式語義,并對三種語義之間的一致性、互補性進行分析和證明。 本文研究了MSVL語言的極小模型語義。由于MSVL語言中的框架技術破壞了邏輯的單調性,傳統(tǒng)的規(guī)范模型已不再適用于捕獲該語言的模型語義。因此,我們提出了極小模型理論并證明了極小模型的存在性定理。 為了正確理解程序語言的執(zhí)行過程,本文研究了MSVL語言的結構化操作語義。首先定義了...

【文章頁數(shù)】：139 頁

【文章目錄】：
Abstract(chinese)
Abstract
List of Figures
List of Tables
Chapter 1 Introduction
    1.1 Formal Semantics Methodologies
        1.1.1 Operational Semantics
        1.1.2 Denotational Semantics
        1.1.3 Axiomatic Semantics
    1.2 Temporal Logic and Temporal Logic Programming
        1.2.1 Temporal Logic
        1.2.2 Temporal Logic Programming
        1.2.3 Existing Problems
    1.3 Contributions
    1.4 Thesis Organization
Chapter 2 Projection Temporal Logic
    2.1 Propositional Projection Temporal Logic
    2.2 First Order Projection Temporal Logic
        2.2.1 Syntax and Semantics
        2.2.2 Satisfaction and Validity
        2.2.3 Derived Formulas and Logic Laws
        2.2.4 Replacement of Variables
    2.3 Conclusion
Chapter 3 Programming Language MSVL
    3.1 The History of MSVL
    3.2 Framing
    3.3 MSVL Programs
        3.3.1 Expressions and Statements
        3.3.2 Derived Constructs
        3.3.3 Data Structures
    3.4 Conclusion
Chapter 4 Minimal Model Semantics of MSVL
    4.1 The Minimal Satisfaction Relation
    4.2 Normal Form of Framed Programs
    4.3 Existence Theorem of Minimal Models
        4.3.1 Least Fixed Point Theorem
        4.3.2 Existence Theorem
    4.4 Examples
    4.5 Conclusion
Chapter 5 Operational Semantics of MSVL
    5.1 Notation
    5.2 Evaluation of Expressions
    5.3 State Reduction
        5.3.1 Semantic Equivalence Rules
        5.3.2 Transition Rules within One State
        5.3.3 Properties for State Reduction
    5.4 Interval Reduction
    5.5 Consistency between Minimal Model and Operational Semantics
        5.5.1 Consistency for Finite Models
        5.5.2 Consistency for Infinite Models
        5.5.3 Nondeterministic Framed Programs
    5.6 An Interpreter for MSVL
    5.7 Conclusion
Chapter 6 Axiomatic Semantics of MSVL
    6.1 The Assertion Language
    6.2 State Axioms and State Inference Rules
    6.3 Axioms and Inference Rules over Intervals
    6.4 Soundness and Completeness
        6.4.1 Soundness
        6.4.2 Completeness
    6.5 Verification of Mutual Exclusion
    6.6 Conclusion
Chapter 7 Conclusions and Future Works
    7.1 Conclusions
    7.2 Future Works
Acknowledgements
References
Finished Papers



本文編號：3917247