动态模糊逻辑程序设计语言的操作语义模型及验证

论文摘要

动态模糊逻辑(DFL)的研究已有十年的时间了,目前已取得了一系列研究成果,为了进一步拓展这些研究成果的应用,本文借鉴Dijkstra的监督命令程序结构,通过结构化操作语义描述方法从软件理论方面进行研究,提出了动态模糊逻辑程序设计语言(DFL Programming Language)的操作语义模型,以期形成解决动态模糊性问题的程序设计方法。主要内容包括:变形传统的λ演算,以更好地描述具有动态模糊性的问题;通过BNF描述了DFL程序设计语言的抽象语法;通过一个三元组<DFSC,DFO,DFSS>给出了DFL程序设计语言的操作语义模型;给出了DFL程序设计语言的基本框架结构;给出了该操作语义模型的一些应用实例;通过Hoare逻辑和基本指称语义对本文所定义的操作语义模型的正确性和可靠性进行了证明。由此可见,本文从全新的角度定义了一种可以处理动态模糊问题的程序设计语言。在描述、解决具有动态模糊性的问题时,本文所给出的DFL程序设计语言的操作语义模型与常见的高级程序设计语言相比表现出了很好的优越性。本文的特色体现在:(1)提出了可以描述动态模糊性问题的λ演算的变形方法;(2)提出了可以解决动态模糊性问题的DFL程序设计语言的操作语义模型,并对该模型的正确性和可靠性进行了证明;(3)提出了DFL程序设计语言的基本框架结构。

论文目录

• 中文摘要
• Abstract
• 第一章 引论
• 1.1 动态模糊逻辑（DFL）的研究综述
• 1.2 问题的提出
• 1.3 本文的内容安排
• 第二章 动态模糊逻辑程序设计语言的基础理论
• 2.1 动态模糊逻辑（DFL）简介
• 2.1.1 DFL 的命题演算
• 2.1.2 DFL 的谓词演算
• 2.1.3 动态模糊数据理论
• 2.2 操作语义
• 2.2.1 操作语义的研究历史
• 2.2.2 结构化操作语义
• 2.3 DFL 的λ演算描述
• 2.3.1 传统的λ演算
• 2.3.1.1 λ项
• 2.3.1.2 置换（Substitution）
• 2.3.1.3 α-变换（α-conversion）
• 2.3.1.4 β-归约（β-conversion）
• 2.3.1.5 丘奇-罗赛定理（Church-Rosser）
• 2.3.2 变形传统的λ演算
• 2.3.2.1 变形的λ演算的项
• 2.3.2.2 变形的λ演算的置换
• 2.3.2.3 变形的λ演算的α-变换
• 2.3.2.4 变形的λ演算的β-归约
• 2.3.2.5 变形的λ演算的丘奇－罗赛定理
• 2.3.3 动态模糊命题的λ演算描述
• 2.3.4 动态模糊谓词的λ演算描述
• 2.4 本章小结
• 第三章 动态模糊逻辑辑程序设计语言的语法
• 3.1 监督命令程序结构
• 3.2 动态模糊逻辑程序设计语言的抽象语法
• 3.3 本章小结
• 第四章 动态模糊逻辑程序设计语言的操作语义模型
• 4.1 动态模糊逻辑程序设计语言的操作语义模型结构
• 4.1.1 动态模糊语法范畴（DFSC）
• 4.1.2 动态模糊算子（DFO）
• 4.1.3 动态模糊语义（DFSS）
• 4.1.3.1 表达式
• 4.1.3.2 布尔表达式
• 4.1.3.3 语句
• 4.1.3.4 监督命令
• 4.2 动态模糊逻辑程序设计语言的数据类型的操作语义
• 4.2.1 动态模糊逻辑程序设计语言的基本数据类型的表示
• 4.2.2 动态模糊逻辑程序设计语言的基本数据类型的操作语义
• 4.2.2.1 动态模糊整型数据（DFInt）
• 4.2.2.2 动态模糊实型数据（DFReal）
• 4.2.2.3 动态模糊布尔型数据（DFBool）
• 4.2.2.4 动态模糊字符型数据（DFChr）
• 4.2.3 其它数据类型
• 4.3 本章小结
• 第五章 动态模糊逻辑程序设计语言的框架
• 5.1 处理对象的动态模糊化
• 5.1.1 动态模糊整数
• 5.1.2 动态模糊布尔值
• 5.1.3 动态模糊字符
• 5.2 类型的动态模糊化
• 5.3 语句的动态模糊化
• 5.4 本章小结
• 第六章 动态模糊逻辑程序设计语言的应用
• 6.1 应用实例
• 6.2 程序的执行过程
• 6.3 本章小结
• 第七章 验证
• 7.1 正确性验证
• 7.2 可靠性验证
• 7.2.1 动态模糊逻辑程序设计语言的指称语义
• 7.2.2 推理规则的可靠性证明
• 7.3 本章小结
• 第八章 结论与展望
• 参考文献
• 致谢
• 附录
• 中英文名词对照
• 中文详细摘要