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

【文章來源】：江西師范大學江西省

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

【學位級別】：碩士

【部分圖文】：

Java泛型約束實例代碼運行結(jié)果

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

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

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

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



本文編號：3307370