框架时序逻辑程序语言MSVL的形式语义

发布时间：2024-03-02 18:56

　　形式语义是对软件系统进行形式化验证和分析的重要理论基础。程序语言的语义可以帮助人们更好的理解、执行、分析软件系统。操作语义有助于语言的实现,公理语义有利于程序的验证,指称语义在强大的数学理论支持下为程序的含义提供了精确的数学描述。 时序逻辑程序设计是一种新型的程序设计范式,程序的具体执行和性质的描述可以在同一逻辑框架内表示,适用于并发系统的建模、模拟和验证。尽管研究人员开发了相关的解释器来执行各类时序逻辑程序语言,时序逻辑及其可执行子集被广泛地应用于系统的规范和验证中,但是到目前为止,至少在区间时序逻辑程序语言中,还没有一套系统而完整的形式语义。本文以区间时序逻辑程序语言MSVL为研究对象,分别从模型语义、操作语义、公理语义三条主线来研究区间时序逻辑程序的形式语义,并对三种语义之间的一致性、互补性进行分析和证明。 本文研究了MSVL语言的极小模型语义。由于MSVL语言中的框架技术破坏了逻辑的单调性,传统的规范模型已不再适用于捕获该语言的模型语义。因此,我们提出了极小模型理论并证明了极小模型的存在性定理。 为了正确理解程序语言的执行过程,本文研究了MSVL语言的结构化操作语义。首先定义了...

【文章页数】：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