泛型约束方法及其安全机制
发布时间：2021-07-28 06:01
面向对象程序设计（OOP）是以程序中的对象为核心,而泛型程序设计（GP）是以类型需求为核心的程序设计范式。泛型程序设计（GP）与面向对象程序设计（OOP）两者都是在程序设计时除去不稳定的部分,用更加通用的并且效率更高的部分来构造程序。尽管通用性和效率这两个特性被认为是相互对立的,但是仍然期望能在程序开发的大多数情况下实现两者之间的平衡,从而在确保类型安全的前提下加快程序开发的速度。总结了不同设计风格的主流程序设计语言有关泛型设施的异同。对于面向对象程序设计语言,以Java为例,Java的参数化类型和泛型约束之间紧耦合,描述的泛型需求过于狭窄,只能称之为窄义的约束;对于动态类型程序设计语言,以Python为例,动态类型语言天然地支持泛型,没有严格的类型定义格式,可以随时改变参数类型,泛型约束机制近乎没有;对于函数式程序设计语言,以Scala为例,Scala的Implicits机制基于面向对象程序设计风格,支持关联类型,对泛型概念特性有着良好的支持,但依旧具有隐式参数。研究了现今主流程序设计语言中的泛型约束方法及其安全机制,因为主流语言其他设施的影响,语言抽象程度不高,难以描述复杂的语义需...
【文章来源】：江西师范大学江西省
【文章页数】：71 页
【学位级别】：硕士
【部分图文】：
Java泛型约束实例代码运行结果
泛型约束方法及其安全机制27图3-1PAR方法及平台的简单框架Apla是抽象程序设计语言，是PAR方法及PAR平台重要组成部分之一。Apla的提出和使用是为了推进程序设计的形式化推导及证明，经过十余年的发展已经具备了很多完善且实用的设施。泛型约束是Apla众多设施的一部分，《Apla中泛型约束机制研究》[36]中提出泛型约束的重要部分就是约束匹配，约束匹配分为两部分：约束匹配检测和约束匹配验证，该文献主要对泛型约束验证进行介绍。其中：约束匹配检测可判定形式参数和实例化参数是否满足约束的静态语法需求，此过程是基于PAR平台完全自动完成；而约束匹配验证则是判定实例化参数是否满足约束的动态语义需求，此过程为部分自动化，需要手工推演出可验证的谓词逻辑公式，并验证其正确，部分逻辑公式借助Isabelle定理证明器进行自动验证。相比之前的工作，本文的主要工作是设计并实现了可判定形式参数和实例化参数是否满足约束的约束匹配检测功能。该功能立足于静态语法层，而约束匹配验证立足于动态语义层。约束匹配检测是约束匹配验证的前期工作，为约束匹配验证提供静态语法的安全基矗同时，本文在设计约束匹配检测之前，提出了严格规范的泛型约束描述语言，提供了设计泛型约束的基本框架，可以基于该描述语言写出严格规范的泛型约束。本文设计的约束匹配检测可以基于PAR平台自动完成。本文选择以高度抽象的程序设计语言Apla为主要宿主语言，原因在于其
泛型约束方法及其安全机制29图3-2约束库内约束精化关系图3.3Apla泛型及泛型约束Apla是本研究团队在形式化方法背景下开发出的一种新型语言，是为实现算法程序设计形式化开发的PAR方法而定义的一种高度抽象的程序设计语言(AbstractProgrammingLanguage)，其目标是尽可能完整地实现以类型需求为核心的泛型程序设计（GP）思想。3.3.1Apla泛型泛型程序设计（GP）与面向对象程序设计（OOP）两者都是在程序设计时除去系统中不稳定的部分，用更加通用的并且稳定性更高的部分来建造系统。GP提供了一种更为抽象的方法，即它是以类型需求作为核心进行编程[42]。以薛锦云教授为首的本研究团队一直关注国内外泛型程序的发展与研究，结合自身特性给出了新的定义，如下所示[34]：定义3（泛型程序设计）*泛型程序设计是一个参数化程序设计，其中参数是指数据、数据类型、子程序（函数和过程）、构件、服务和子系统等，并以此为基础，编制出具有通用性的程序。定义4（泛型约束）*泛型约束是在泛型程序设计中对每类泛型参数构成域的精确描述。如果泛型参数是函数，其泛型约束就是对函数的高度概括；同样如果泛型参数是操作，其泛型约束就是对操作的高度概括。泛型约束是泛型类型安全的重要保障。3.3.2Apla泛型约束描述语言结合泛型程序设计及泛型约束新定义和其他主流程序设计语言的特点，Apla将泛型约束分为三大部分：约束定义、约束调用和约束实例化。以下是Apla基于类型需求的泛型约束描述语言：
【参考文献】：
期刊论文
[1]Apla与程序设计语言泛型特性比较研究[J]. 左正康,刘志豪,黄箐,游珍,王昌晶,石海鹤,胡启敏,陶小明. 江西师范大学学报(自然科学版). 2019(05)
[2]形式化方法概貌[J]. 王戟,詹乃军,冯新宇,刘志明. 软件学报. 2019(01)
[3]泛型编程在面向对象语言中的对比研究[J]. 周卫星,左正康,王昌晶,石海鹤,游珍,谢武平,陶小明. 江西师范大学学报(自然科学版). 2018(03)
[4]Apla→Java程序生成系统中泛型机制实现方法研究[J]. 徐华珍,薛锦云,朱小征. 江西师范大学学报(自然科学版). 2017(01)
[5]一种抽象泛型机制的新型Java实现[J]. 田方,石海鹤,左正康,王昌晶,薛锦云. 江西师范大学学报(自然科学版). 2016(01)
[6]Apla中泛型约束机制研究[J]. 左正康,薛锦云. 软件学报. 2015(06)
[7]基于源代码静态分析的C++0x泛型概念抽取[J]. 陈林,徐宝文. 计算机学报. 2009(09)
[8]泛型编程扩展及其JAVA实现[J]. 徐文胜,薛锦云. 计算机工程与科学. 2007(10)
[9]面向对象、泛型程序设计与类型约束检查[J]. 孙斌. 计算机学报. 2004(11)
硕士论文
[1]Apla泛型约束匹配检测系统的设计与实现[D]. 陶小明.江西师范大学 2018
本文编号：3307370
【文章来源】：江西师范大学江西省
【文章页数】：71 页
【学位级别】：硕士
【部分图文】：
Java泛型约束实例代码运行结果
泛型约束方法及其安全机制27图3-1PAR方法及平台的简单框架Apla是抽象程序设计语言，是PAR方法及PAR平台重要组成部分之一。Apla的提出和使用是为了推进程序设计的形式化推导及证明，经过十余年的发展已经具备了很多完善且实用的设施。泛型约束是Apla众多设施的一部分，《Apla中泛型约束机制研究》[36]中提出泛型约束的重要部分就是约束匹配，约束匹配分为两部分：约束匹配检测和约束匹配验证，该文献主要对泛型约束验证进行介绍。其中：约束匹配检测可判定形式参数和实例化参数是否满足约束的静态语法需求，此过程是基于PAR平台完全自动完成；而约束匹配验证则是判定实例化参数是否满足约束的动态语义需求，此过程为部分自动化，需要手工推演出可验证的谓词逻辑公式，并验证其正确，部分逻辑公式借助Isabelle定理证明器进行自动验证。相比之前的工作，本文的主要工作是设计并实现了可判定形式参数和实例化参数是否满足约束的约束匹配检测功能。该功能立足于静态语法层，而约束匹配验证立足于动态语义层。约束匹配检测是约束匹配验证的前期工作，为约束匹配验证提供静态语法的安全基矗同时，本文在设计约束匹配检测之前，提出了严格规范的泛型约束描述语言，提供了设计泛型约束的基本框架，可以基于该描述语言写出严格规范的泛型约束。本文设计的约束匹配检测可以基于PAR平台自动完成。本文选择以高度抽象的程序设计语言Apla为主要宿主语言，原因在于其
泛型约束方法及其安全机制29图3-2约束库内约束精化关系图3.3Apla泛型及泛型约束Apla是本研究团队在形式化方法背景下开发出的一种新型语言，是为实现算法程序设计形式化开发的PAR方法而定义的一种高度抽象的程序设计语言(AbstractProgrammingLanguage)，其目标是尽可能完整地实现以类型需求为核心的泛型程序设计（GP）思想。3.3.1Apla泛型泛型程序设计（GP）与面向对象程序设计（OOP）两者都是在程序设计时除去系统中不稳定的部分，用更加通用的并且稳定性更高的部分来建造系统。GP提供了一种更为抽象的方法，即它是以类型需求作为核心进行编程[42]。以薛锦云教授为首的本研究团队一直关注国内外泛型程序的发展与研究，结合自身特性给出了新的定义，如下所示[34]：定义3（泛型程序设计）*泛型程序设计是一个参数化程序设计，其中参数是指数据、数据类型、子程序（函数和过程）、构件、服务和子系统等，并以此为基础，编制出具有通用性的程序。定义4（泛型约束）*泛型约束是在泛型程序设计中对每类泛型参数构成域的精确描述。如果泛型参数是函数，其泛型约束就是对函数的高度概括；同样如果泛型参数是操作，其泛型约束就是对操作的高度概括。泛型约束是泛型类型安全的重要保障。3.3.2Apla泛型约束描述语言结合泛型程序设计及泛型约束新定义和其他主流程序设计语言的特点，Apla将泛型约束分为三大部分：约束定义、约束调用和约束实例化。以下是Apla基于类型需求的泛型约束描述语言：
【参考文献】：
期刊论文
[1]Apla与程序设计语言泛型特性比较研究[J]. 左正康,刘志豪,黄箐,游珍,王昌晶,石海鹤,胡启敏,陶小明. 江西师范大学学报(自然科学版). 2019(05)
[2]形式化方法概貌[J]. 王戟,詹乃军,冯新宇,刘志明. 软件学报. 2019(01)
[3]泛型编程在面向对象语言中的对比研究[J]. 周卫星,左正康,王昌晶,石海鹤,游珍,谢武平,陶小明. 江西师范大学学报(自然科学版). 2018(03)
[4]Apla→Java程序生成系统中泛型机制实现方法研究[J]. 徐华珍,薛锦云,朱小征. 江西师范大学学报(自然科学版). 2017(01)
[5]一种抽象泛型机制的新型Java实现[J]. 田方,石海鹤,左正康,王昌晶,薛锦云. 江西师范大学学报(自然科学版). 2016(01)
[6]Apla中泛型约束机制研究[J]. 左正康,薛锦云. 软件学报. 2015(06)
[7]基于源代码静态分析的C++0x泛型概念抽取[J]. 陈林,徐宝文. 计算机学报. 2009(09)
[8]泛型编程扩展及其JAVA实现[J]. 徐文胜,薛锦云. 计算机工程与科学. 2007(10)
[9]面向对象、泛型程序设计与类型约束检查[J]. 孙斌. 计算机学报. 2004(11)
硕士论文
[1]Apla泛型约束匹配检测系统的设计与实现[D]. 陶小明.江西师范大学 2018
本文编号：3307370
本文链接：https://www.wllwen.com/shoufeilunwen/xixikjs/3307370.html
