發(fā)布時(shí)間：2021-07-28 06:01

　　面向?qū)ο蟪绦蛟O(shè)計(jì)（OOP）是以程序中的對(duì)象為核心,而泛型程序設(shè)計(jì)（GP）是以類型需求為核心的程序設(shè)計(jì)范式。泛型程序設(shè)計(jì)（GP）與面向?qū)ο蟪绦蛟O(shè)計(jì)（OOP）兩者都是在程序設(shè)計(jì)時(shí)除去不穩(wěn)定的部分,用更加通用的并且效率更高的部分來(lái)構(gòu)造程序。盡管通用性和效率這兩個(gè)特性被認(rèn)為是相互對(duì)立的,但是仍然期望能在程序開(kāi)發(fā)的大多數(shù)情況下實(shí)現(xiàn)兩者之間的平衡,從而在確保類型安全的前提下加快程序開(kāi)發(fā)的速度�？偨Y(jié)了不同設(shè)計(jì)風(fēng)格的主流程序設(shè)計(jì)語(yǔ)言有關(guān)泛型設(shè)施的異同。對(duì)于面向?qū)ο蟪绦蛟O(shè)計(jì)語(yǔ)言,以Java為例,Java的參數(shù)化類型和泛型約束之間緊耦合,描述的泛型需求過(guò)于狹窄,只能稱之為窄義的約束;對(duì)于動(dòng)態(tài)類型程序設(shè)計(jì)語(yǔ)言,以Python為例,動(dòng)態(tài)類型語(yǔ)言天然地支持泛型,沒(méi)有嚴(yán)格的類型定義格式,可以隨時(shí)改變參數(shù)類型,泛型約束機(jī)制近乎沒(méi)有;對(duì)于函數(shù)式程序設(shè)計(jì)語(yǔ)言,以Scala為例,Scala的Implicits機(jī)制基于面向?qū)ο蟪绦蛟O(shè)計(jì)風(fēng)格,支持關(guān)聯(lián)類型,對(duì)泛型概念特性有著良好的支持,但依舊具有隱式參數(shù)。研究了現(xiàn)今主流程序設(shè)計(jì)語(yǔ)言中的泛型約束方法及其安全機(jī)制,因?yàn)橹髁髡Z(yǔ)言其他設(shè)施的影響,語(yǔ)言抽象程度不高,難以描述復(fù)雜的語(yǔ)義需... 

【文章來(lái)源】：江西師范大學(xué)江西省

【文章頁(yè)數(shù)】：71 頁(yè)

【學(xué)位級(jí)別】：碩士

【部分圖文】：

Java泛型約束實(shí)例代碼運(yùn)行結(jié)果

泛型約束方法及其安全機(jī)制27圖3-1PAR方法及平臺(tái)的簡(jiǎn)單框架Apla是抽象程序設(shè)計(jì)語(yǔ)言，是PAR方法及PAR平臺(tái)重要組成部分之一。Apla的提出和使用是為了推進(jìn)程序設(shè)計(jì)的形式化推導(dǎo)及證明，經(jīng)過(guò)十余年的發(fā)展已經(jīng)具備了很多完善且實(shí)用的設(shè)施。泛型約束是Apla眾多設(shè)施的一部分，《Apla中泛型約束機(jī)制研究》[36]中提出泛型約束的重要部分就是約束匹配，約束匹配分為兩部分：約束匹配檢測(cè)和約束匹配驗(yàn)證，該文獻(xiàn)主要對(duì)泛型約束驗(yàn)證進(jìn)行介紹。其中：約束匹配檢測(cè)可判定形式參數(shù)和實(shí)例化參數(shù)是否滿足約束的靜態(tài)語(yǔ)法需求，此過(guò)程是基于PAR平臺(tái)完全自動(dòng)完成；而約束匹配驗(yàn)證則是判定實(shí)例化參數(shù)是否滿足約束的動(dòng)態(tài)語(yǔ)義需求，此過(guò)程為部分自動(dòng)化，需要手工推演出可驗(yàn)證的謂詞邏輯公式，并驗(yàn)證其正確，部分邏輯公式借助Isabelle定理證明器進(jìn)行自動(dòng)驗(yàn)證。相比之前的工作，本文的主要工作是設(shè)計(jì)并實(shí)現(xiàn)了可判定形式參數(shù)和實(shí)例化參數(shù)是否滿足約束的約束匹配檢測(cè)功能。該功能立足于靜態(tài)語(yǔ)法層，而約束匹配驗(yàn)證立足于動(dòng)態(tài)語(yǔ)義層。約束匹配檢測(cè)是約束匹配驗(yàn)證的前期工作，為約束匹配驗(yàn)證提供靜態(tài)語(yǔ)法的安全基矗同時(shí)，本文在設(shè)計(jì)約束匹配檢測(cè)之前，提出了嚴(yán)格規(guī)范的泛型約束描述語(yǔ)言，提供了設(shè)計(jì)泛型約束的基本框架，可以基于該描述語(yǔ)言寫出嚴(yán)格規(guī)范的泛型約束。本文設(shè)計(jì)的約束匹配檢測(cè)可以基于PAR平臺(tái)自動(dòng)完成。本文選擇以高度抽象的程序設(shè)計(jì)語(yǔ)言Apla為主要宿主語(yǔ)言，原因在于其

泛型約束方法及其安全機(jī)制29圖3-2約束庫(kù)內(nèi)約束精化關(guān)系圖3.3Apla泛型及泛型約束Apla是本研究團(tuán)隊(duì)在形式化方法背景下開(kāi)發(fā)出的一種新型語(yǔ)言，是為實(shí)現(xiàn)算法程序設(shè)計(jì)形式化開(kāi)發(fā)的PAR方法而定義的一種高度抽象的程序設(shè)計(jì)語(yǔ)言(AbstractProgrammingLanguage)，其目標(biāo)是盡可能完整地實(shí)現(xiàn)以類型需求為核心的泛型程序設(shè)計(jì)（GP）思想。3.3.1Apla泛型泛型程序設(shè)計(jì)（GP）與面向?qū)ο蟪绦蛟O(shè)計(jì)（OOP）兩者都是在程序設(shè)計(jì)時(shí)除去系統(tǒng)中不穩(wěn)定的部分，用更加通用的并且穩(wěn)定性更高的部分來(lái)建造系統(tǒng)。GP提供了一種更為抽象的方法，即它是以類型需求作為核心進(jìn)行編程[42]。以薛錦云教授為首的本研究團(tuán)隊(duì)一直關(guān)注國(guó)內(nèi)外泛型程序的發(fā)展與研究，結(jié)合自身特性給出了新的定義，如下所示[34]：定義3（泛型程序設(shè)計(jì)）*泛型程序設(shè)計(jì)是一個(gè)參數(shù)化程序設(shè)計(jì)，其中參數(shù)是指數(shù)據(jù)、數(shù)據(jù)類型、子程序（函數(shù)和過(guò)程）、構(gòu)件、服務(wù)和子系統(tǒng)等，并以此為基礎(chǔ)，編制出具有通用性的程序。定義4（泛型約束）*泛型約束是在泛型程序設(shè)計(jì)中對(duì)每類泛型參數(shù)構(gòu)成域的精確描述。如果泛型參數(shù)是函數(shù)，其泛型約束就是對(duì)函數(shù)的高度概括；同樣如果泛型參數(shù)是操作，其泛型約束就是對(duì)操作的高度概括。泛型約束是泛型類型安全的重要保障。3.3.2Apla泛型約束描述語(yǔ)言結(jié)合泛型程序設(shè)計(jì)及泛型約束新定義和其他主流程序設(shè)計(jì)語(yǔ)言的特點(diǎn)，Apla將泛型約束分為三大部分：約束定義、約束調(diào)用和約束實(shí)例化。以下是Apla基于類型需求的泛型約束描述語(yǔ)言：

【參考文獻(xiàn)】：
期刊論文
[1]Apla與程序設(shè)計(jì)語(yǔ)言泛型特性比較研究[J]. 左正康,劉志豪,黃箐,游珍,王昌晶,石海鶴,胡啟敏,陶小明.  江西師范大學(xué)學(xué)報(bào)(自然科學(xué)版). 2019(05)
[2]形式化方法概貌[J]. 王戟,詹乃軍,馮新宇,劉志明.  軟件學(xué)報(bào). 2019(01)
[3]泛型編程在面向?qū)ο笳Z(yǔ)言中的對(duì)比研究[J]. 周衛(wèi)星,左正康,王昌晶,石海鶴,游珍,謝武平,陶小明.  江西師范大學(xué)學(xué)報(bào)(自然科學(xué)版). 2018(03)
[4]Apla→Java程序生成系統(tǒng)中泛型機(jī)制實(shí)現(xiàn)方法研究[J]. 徐華珍,薛錦云,朱小征.  江西師范大學(xué)學(xué)報(bào)(自然科學(xué)版). 2017(01)
[5]一種抽象泛型機(jī)制的新型Java實(shí)現(xiàn)[J]. 田方,石海鶴,左正康,王昌晶,薛錦云.  江西師范大學(xué)學(xué)報(bào)(自然科學(xué)版). 2016(01)
[6]Apla中泛型約束機(jī)制研究[J]. 左正康,薛錦云.  軟件學(xué)報(bào). 2015(06)
[7]基于源代碼靜態(tài)分析的C++0x泛型概念抽取[J]. 陳林,徐寶文.  計(jì)算機(jī)學(xué)報(bào). 2009(09)
[8]泛型編程擴(kuò)展及其JAVA實(shí)現(xiàn)[J]. 徐文勝,薛錦云.  計(jì)算機(jī)工程與科學(xué). 2007(10)
[9]面向?qū)ο�、泛型程序設(shè)計(jì)與類型約束檢查[J]. 孫斌.  計(jì)算機(jī)學(xué)報(bào). 2004(11)

碩士論文
[1]Apla泛型約束匹配檢測(cè)系統(tǒng)的設(shè)計(jì)與實(shí)現(xiàn)[D]. 陶小明.江西師范大學(xué) 2018



本文編號(hào)：3307370