掃一掃
關(guān)注中圖網(wǎng)
官方微博
本類五星書更多>
-
>
全國計算機等級考試最新真考題庫模擬考場及詳解·二級MSOffice高級應(yīng)用
-
>
決戰(zhàn)行測5000題(言語理解與表達)
-
>
軟件性能測試.分析與調(diào)優(yōu)實踐之路
-
>
第一行代碼Android
-
>
JAVA持續(xù)交付
-
>
EXCEL最強教科書(完全版)(全彩印刷)
-
>
深度學(xué)習(xí)
分劃遞推法中泛型約束機制 版權(quán)信息
- ISBN：9787030710727
- 條形碼：9787030710727 ; 978-7-03-071072-7
- 裝幀：一般膠版紙
- 冊數(shù)：暫無
- 重量：暫無
- 所屬分類：>
分劃遞推法中泛型約束機制 內(nèi)容簡介
本書是作者在泛型程序設(shè)計領(lǐng)域多年研究的結(jié)晶，通過研究分劃遞推法中泛型約束機制的設(shè)計與實現(xiàn)，向讀者展現(xiàn)泛型約束機制可解決一系列復(fù)雜泛型約束問題。讀者閱讀本書之后，既可對泛型程序設(shè)計有更深入的了解，也可參考本書提供的方法解決實際程序設(shè)計中可能會遇到的一些難題。 本書適合程序設(shè)計語言原理及軟件形式化方向的高年級本科生、研究生和相關(guān)教師閱讀，對從事可信軟件行業(yè)的相關(guān)人員也有一定的借鑒和參考意義，對一般程序員深入了解程序設(shè)計語言原理有一定幫助。
分劃遞推法中泛型約束機制 目錄
目錄
前言
第1章 緒論 1
1.1 研究背景 1
1.2 研究內(nèi)容 2
1.3 本書的組織結(jié)構(gòu) 3
第2章 泛型約束相關(guān)研究 4
2.1 泛型程序設(shè)計 4
2.2 泛型程序設(shè)計及其約束的新定義 4
2.3 函數(shù)式語言泛型約束 5
2.3.1 System F 5
2.3.2 Haskell 98 6
2.3.3 ML 7
2.4 面向?qū)ο笳Z言泛型約束 8
2.4.1 C++模板約束 8
2.4.2 Concepts概念約束 12
2.4.3 Java泛型約束 14
2.4.4 C#泛型約束 17
2.4.5 小結(jié) 19
2.5 泛型程序設(shè)計與面向?qū)ο蟪绦蛟O(shè)計的比較 19
第3章 Apla中的泛型機制 21
3.1 類型參數(shù)化 21
3.2 操作參數(shù)化 22
3.3 泛型Apla程序結(jié)構(gòu) 22
3.3.1 單類型參數(shù)化 22
3.3.2 多類型參數(shù)化 23
3.4 Apla泛型過程結(jié)構(gòu) 23
3.5 Apla泛型函數(shù)結(jié)構(gòu) 24
3.6 泛型算法示例 25
第4章 泛型約束機制在Apla中的設(shè)計 29
4.1 操作約束定義 29
4.2 類型約束定義 31
4.2.1 傳統(tǒng)數(shù)據(jù)類型約束 31
4.2.2 標(biāo)準(zhǔn)數(shù)據(jù)類型約束 34
4.2.3 代數(shù)結(jié)構(gòu)泛型約束庫 35
4.3 約束調(diào)用及例化 45
4.3.1 約束調(diào)用 45
4.3.2 約束例化 48
4.4 完整實例 51
4.4.1 泛型Kleene算法 51
4.4.2 泛型二分搜索算法 56
4.4.3 泛型Bellman-Ford算法 58
4.4.4 泛型極值類算法 59
4.4.5 泛型中綴表達式求值算法 60
第5章 約束匹配檢測及驗證 63
5.1 約束匹配檢測 63
5.2 約束匹配驗證 64
5.2.1 實例操作參數(shù)語義驗證 64
5.2.2 實例類型參數(shù)語義驗證 67
5.2.3 約束匹配驗證實例 70
第6章 泛型約束機制在PAR平臺C++生成系統(tǒng)中的實現(xiàn) 88
6.1 PAR平臺C++生成系統(tǒng) 88
6.1.1 系統(tǒng)主要功能 88
6.1.2 主要功能模塊 90
6.1.3 系統(tǒng)界面 92
6.1.4 規(guī)則庫 94
6.2 泛型約束機制在PAR平臺上的實現(xiàn) 95
6.2.1 形式類型參數(shù)檢測 95
6.2.2 實例參數(shù)語法檢測 95
6.2.3 實現(xiàn)實例 96
第7章 總結(jié) 99
參考文獻 101
前言
第1章 緒論 1
1.1 研究背景 1
1.2 研究內(nèi)容 2
1.3 本書的組織結(jié)構(gòu) 3
第2章 泛型約束相關(guān)研究 4
2.1 泛型程序設(shè)計 4
2.2 泛型程序設(shè)計及其約束的新定義 4
2.3 函數(shù)式語言泛型約束 5
2.3.1 System F 5
2.3.2 Haskell 98 6
2.3.3 ML 7
2.4 面向?qū)ο笳Z言泛型約束 8
2.4.1 C++模板約束 8
2.4.2 Concepts概念約束 12
2.4.3 Java泛型約束 14
2.4.4 C#泛型約束 17
2.4.5 小結(jié) 19
2.5 泛型程序設(shè)計與面向?qū)ο蟪绦蛟O(shè)計的比較 19
第3章 Apla中的泛型機制 21
3.1 類型參數(shù)化 21
3.2 操作參數(shù)化 22
3.3 泛型Apla程序結(jié)構(gòu) 22
3.3.1 單類型參數(shù)化 22
3.3.2 多類型參數(shù)化 23
3.4 Apla泛型過程結(jié)構(gòu) 23
3.5 Apla泛型函數(shù)結(jié)構(gòu) 24
3.6 泛型算法示例 25
第4章 泛型約束機制在Apla中的設(shè)計 29
4.1 操作約束定義 29
4.2 類型約束定義 31
4.2.1 傳統(tǒng)數(shù)據(jù)類型約束 31
4.2.2 標(biāo)準(zhǔn)數(shù)據(jù)類型約束 34
4.2.3 代數(shù)結(jié)構(gòu)泛型約束庫 35
4.3 約束調(diào)用及例化 45
4.3.1 約束調(diào)用 45
4.3.2 約束例化 48
4.4 完整實例 51
4.4.1 泛型Kleene算法 51
4.4.2 泛型二分搜索算法 56
4.4.3 泛型Bellman-Ford算法 58
4.4.4 泛型極值類算法 59
4.4.5 泛型中綴表達式求值算法 60
第5章 約束匹配檢測及驗證 63
5.1 約束匹配檢測 63
5.2 約束匹配驗證 64
5.2.1 實例操作參數(shù)語義驗證 64
5.2.2 實例類型參數(shù)語義驗證 67
5.2.3 約束匹配驗證實例 70
第6章 泛型約束機制在PAR平臺C++生成系統(tǒng)中的實現(xiàn) 88
6.1 PAR平臺C++生成系統(tǒng) 88
6.1.1 系統(tǒng)主要功能 88
6.1.2 主要功能模塊 90
6.1.3 系統(tǒng)界面 92
6.1.4 規(guī)則庫 94
6.2 泛型約束機制在PAR平臺上的實現(xiàn) 95
6.2.1 形式類型參數(shù)檢測 95
6.2.2 實例參數(shù)語法檢測 95
6.2.3 實現(xiàn)實例 96
第7章 總結(jié) 99
參考文獻 101
展開全部
分劃遞推法中泛型約束機制 節(jié)選
第1章 緒論 1.1 研究背景 泛型程序設(shè)計是指設(shè)計程序不僅可以使用數(shù)據(jù)作參數(shù)，還可以使用數(shù)據(jù)類型、操作、構(gòu)件、服務(wù)和子系統(tǒng)等作參數(shù)。1968年，McIlroy等[1]提出可重用軟件部件的概念，即像組裝硬件部件生產(chǎn)計算機一樣組裝軟件部件生產(chǎn)軟件。本書首次提出可重用軟件部件要力求泛型(generality)，以應(yīng)對軟件部件規(guī)模龐大和正確性驗證等問題。20世紀60年代，函數(shù)式編程語言LISP采用的高階函數(shù)和參數(shù)化多態(tài)的編程風(fēng)格，是泛型程序設(shè)計的早期雛形。70年代至今，多態(tài)類型系統(tǒng)得以完整實現(xiàn)，其中包括Siek和Milner等[2-4]的工作。80～90年代，Musser等正式提出了泛型程序設(shè)計基本方法和原則[5-8]。使用泛型程序設(shè)計技術(shù)可以大幅度提高程序的可重用性、可靠性和開發(fā)效率，使建設(shè)軟件構(gòu)件工廠的理想得以實現(xiàn)。C++標(biāo)準(zhǔn)模板庫(standard template library，STL)就是典型的成功實例[9]。泛型程序設(shè)計被認為是比面向?qū)ο蟪绦蛟O(shè)計(object oriented programming，OOP)更具影響力的程序設(shè)計范型[10，11]，因此引起國際計算機界的廣泛重視。 然而，泛型程序設(shè)計在提出之后，并沒有包含安全語言泛型機制。例如，Ada語言[8]和C++語言[12]均可實現(xiàn)類型和操作參數(shù)化，但對于其中的類型參數(shù)和操作參數(shù)沒有實行安全約束機制，這導(dǎo)致在泛型參數(shù)實例化過程中無法判斷哪些實例類型可以實例化數(shù)據(jù)類型參數(shù)，哪些實例操作可以實例化操作參數(shù)。一些本應(yīng)該在編譯階段發(fā)現(xiàn)的語法錯誤轉(zhuǎn)變成程序運行時才能被系統(tǒng)發(fā)現(xiàn)的語義錯誤，這帶來了嚴重的安全性問題。近年來，泛型約束逐漸成為國際上的研究熱點。Java語言在其SE1.5版本之后添加了泛型及其約束機制[13]，對類型參數(shù)的約束通過Extends和Implements子句來實現(xiàn)，子句分別說明了類型參數(shù)所屬的類和實現(xiàn)的接口列表，值類型以打包/解包方式實例化并能得到約束。C#采用了修改虛擬機以支持類型參數(shù)化的方案，加入C#2.0及以后版本中[14-16]，C#對類型參數(shù)的約束通過Where子句來實現(xiàn)，子句中可以說明類型參數(shù)所屬的類和實現(xiàn)的接口列表。元語言(meta language，ML)使用了signature[17，18]，Haskell帶有type class機制[19，20]，Musser將Concept概念擴展到C++語言，提出基于公理語義的泛型約束機制，并稱這種語言為ConceptC++或C++0X[20]。北京大學(xué)計算語言學(xué)研究所孫斌提出了命名類型約束機制[11]等，均在其各自設(shè)計的語言中支持泛型及其約束，但是這些語言的新的泛型約束機制均僅限于類型參數(shù)約束，且存在抽象程度不高、不易于形式化驗證等不足，嚴重限制了泛型程序設(shè)計方法的應(yīng)用范圍。 1.2 研究內(nèi)容 分劃遞推法由PAR方法和PAR平臺組成，是江西省高性能計算技術(shù)重點實驗室軟件形式化和自動化學(xué)術(shù)團隊提出并研制成功的一個程序設(shè)計環(huán)境[21，22]。它由泛型規(guī)約和算法描述語言Radl、泛型抽象程序設(shè)計語言(abstract programming language，Apla)、形式規(guī)約變換規(guī)則、系列算法和程序自動轉(zhuǎn)換工具，以及系統(tǒng)的程序設(shè)計方法學(xué)構(gòu)成。PAR方法和PAR平臺包含循環(huán)不變式的新定義和新的開發(fā)策略、統(tǒng)一的算法程序設(shè)計方法、自動生成SQL查詢程序等關(guān)鍵技術(shù)，并支持算法程序的形式化開發(fā)。文獻[23]～[25]證明，用PAR方法提供的語言、變換規(guī)則和系列轉(zhuǎn)換工具開發(fā)的算法程序具有原理簡單、使用方便、通用性強、可靠性高等特點，可以大幅度提高復(fù)雜算法程序的生產(chǎn)效率。 Isabelle是一種通用的交互式定理證明器[26]，由英國劍橋大學(xué)Lawrence C. Paulson和德國慕尼黑技術(shù)大學(xué)Tobias Nipkow于1986年聯(lián)合開發(fā)，用函數(shù)式編程語言ML來編寫，使用自然演繹規(guī)則進行定理證明。它既支持數(shù)學(xué)公式的形式化描述，又為公式的邏輯演算提供了證明工具。Isabelle主要應(yīng)用在數(shù)學(xué)定理證明和形式化驗證領(lǐng)域，尤其是計算機軟、硬件的正確性驗證以及程序設(shè)計語言和協(xié)議的驗證等方面。 江西省高性能計算技術(shù)重點實驗室軟件形式化和自動化學(xué)術(shù)團隊在2005年獲準(zhǔn)的國家自然科學(xué)基金面上項目“基于PAR方法和PAR平臺的泛型程序設(shè)計關(guān)鍵技術(shù)研究”(60573080)中，對泛型程序的正確性理論和新的泛型機制進行了深入研究，在提出的泛型算法設(shè)計語言Radl和抽象程序設(shè)計語言Apla中成功地實現(xiàn)了類型和操作參數(shù)的泛型機制，但在這些機制中沒有包含安全語言泛型機制，限制了泛型程序設(shè)計技術(shù)的安全使用。2010年，薛錦云領(lǐng)銜申請獲準(zhǔn)的國家自然科學(xué)基金重大國際(地區(qū))合作交流項目“若干軟件新技術(shù)及其在PAR平臺中的實驗研究”(61020106009)將在PAR中實現(xiàn)泛型約束機制作為該項目四大研究目標(biāo)之一。本書將針對這一研究目標(biāo)深入開展研究： (1)在PAR中設(shè)計抽象約束機制，其*終表現(xiàn)形式為謂詞邏輯公式，同時支持語法和語義層約束，拓展現(xiàn)有的支持泛型約束機制的程序設(shè)計語言泛型約束的應(yīng)用范圍。 (2)在設(shè)計過程中，給出類型參數(shù)和操作參數(shù)兩類泛型參數(shù)構(gòu)成域的精確描述。 (3)提出PAR平臺泛型約束匹配檢測及驗證模型及其相關(guān)算法，支持完善的模塊化約束匹配自動檢測，借助Isabelle定理證明器驗證實例類型和實例操作與類型約束和操作約束的語義匹配關(guān)系。 (4)進一步設(shè)計泛型約束機制在PAR平臺的實現(xiàn)方案及其系統(tǒng)原型，可將檢驗合法的泛型Apla程序自動生成可執(zhí)行的C++程序，提高C++程序的泛型安全性。 1.3 本書的組織結(jié)構(gòu) 本書共7章，各章的組織結(jié)構(gòu)如下： 第1章為緒論部分，對撰寫背景和研究內(nèi)容進行概述。 第2章為綜述部分，對國內(nèi)外泛型程序設(shè)計和泛型約束的研究狀況進行分析總結(jié)。 第3章概要介紹PAR方法和PAR平臺，并重點闡述本書提出的泛型約束機制的宿主語言，即抽象程序設(shè)計語言Apla及其原有的泛型機制。 第4章提出泛型約束機制在Apla中的設(shè)計方案，包含數(shù)據(jù)類型約束和操作約束兩類約束定義及其調(diào)用和例化方案。 第5章設(shè)計PAR平臺泛型約束匹配檢測及驗證模型及其相關(guān)算法，支持完善的模塊化約束匹配自動檢測，借助Isabelle定理證明器驗證實例類型和實例操作與類型約束和操作約束的語義匹配關(guān)系。 第6章設(shè)計泛型約束機制在PAR平臺的實現(xiàn)方案及其系統(tǒng)原型，并將其成功應(yīng)用于多個泛型實例，通過一個典型的基于閉半環(huán)代數(shù)結(jié)構(gòu)約束的Kleene泛型算法展示該泛型約束機制的設(shè)計與實現(xiàn)過程。 第7章在對全書進行總結(jié)的基礎(chǔ)上，討論本書工作可能的后續(xù)擴展。 第2章 泛型約束相關(guān)研究 2.1 泛型程序設(shè)計 迄今為止，泛型程序設(shè)計的定義仍未統(tǒng)一[27]。Jarvi等認為泛型程序設(shè)計是設(shè)計和實現(xiàn)軟件可重用部件庫的一種范式，抽取算法相近實現(xiàn)的共性，并以盡可能參數(shù)化的方式覆蓋這些實現(xiàn)，在力求抽象性的同時保持高效運行，*終得到抽象的泛型算法[28，29]。Hinze等認為泛型程序設(shè)計是函數(shù)式編程的一種范式，其中函數(shù)將類型作為參數(shù)，函數(shù)的行為取決于類型的結(jié)構(gòu)[19，30]，這類函數(shù)稱為泛型函數(shù)，編寫一次泛型函數(shù)，可通過實例化不同的具體類型使用多次。Reis等認為泛型程序設(shè)計是軟件設(shè)計的一種系統(tǒng)性方法，致力于抽取算法的*通用(或抽象)表示形式，并保持高效的運行方式[31-33]。Russo等給出了更廣義的泛型程序設(shè)計的定義[34，35]：泛型程序設(shè)計是計算機科學(xué)的一個分支，主要是抽取算法、數(shù)據(jù)結(jié)構(gòu)和其他軟件概念的抽象表示，并將它們進行系統(tǒng)的組織。 根據(jù)現(xiàn)有的泛型程序設(shè)計的定義，本書認為典型的泛型程序設(shè)計是一個參數(shù)化程序設(shè)計(parameterized programming)，其中參數(shù)是指數(shù)據(jù)、數(shù)據(jù)類型、操作(函數(shù)和過程)、構(gòu)件、服務(wù)和子系統(tǒng)等，并以此為基礎(chǔ)，編制出具有通用性的程序。泛型程序設(shè)計的作用在于能編寫清晰、易理解、可重用的程序，能反映程序中算法的實質(zhì)，是編寫抽象算法程序的有力工具。用泛型程序設(shè)計方法設(shè)計的程序稱為泛型程序，泛型程序中的形參稱為泛型參數(shù)，形參對應(yīng)的實參稱為實例參數(shù)。泛型程序設(shè)計以高效率和高抽象的特點已在產(chǎn)業(yè)界和學(xué)術(shù)界得到廣泛關(guān)注和認可。 2.2 泛型程序設(shè)計及其約束的新定義 1997年起，Xue[21，22]一直致力于研究泛型程序設(shè)計，經(jīng)過深入的研究，本書給出了更為確切的泛型程序設(shè)計及其約束的定義。 定義2-1(泛型程序設(shè)計)泛型程序設(shè)計是一個參數(shù)化程序設(shè)計，其中參數(shù)是指數(shù)據(jù)、數(shù)據(jù)類型、子程序(函數(shù)和過程)、構(gòu)件、服務(wù)和子系統(tǒng)等，并以參數(shù)化程序設(shè)計為基礎(chǔ)，編制出具有通用性的程序。 定義2-2(泛型約束)泛型約束是在泛型程序設(shè)計中對每類泛型參數(shù)構(gòu)成域的精確描述。 例如，若泛型參數(shù)為數(shù)據(jù)，則其泛型約束即對數(shù)據(jù)域的精確描述，即類型，這是*低級的泛型約束；若泛型參數(shù)為數(shù)據(jù)類型，則其泛型約束即對數(shù)據(jù)類型的精確描述，依據(jù)任何一個標(biāo)準(zhǔn)數(shù)據(jù)類型都是一個代數(shù)系統(tǒng)的結(jié)論[36]，本書提出用代數(shù)結(jié)構(gòu)來描述標(biāo)準(zhǔn)數(shù)據(jù)類型約束；若泛型參數(shù)為操作，則其泛型約束即對操作的精確描述，本書提出用Hoare公理語義來描述操作約束。泛型約束是保證泛型程序設(shè)計安全性的重要機制，也是構(gòu)造可信軟件的關(guān)鍵技術(shù)[37]。 從以上定義可以看出，完整的泛型約束應(yīng)包含對數(shù)據(jù)、數(shù)據(jù)類型、操作(函數(shù)和過程)、構(gòu)件、服務(wù)和子系統(tǒng)等每類泛型參數(shù)構(gòu)成域的精確描述。然而，目前大多數(shù)語言只支持數(shù)據(jù)及數(shù)據(jù)類型的構(gòu)成域的描述，并且對于數(shù)據(jù)類型約束也只涵蓋了語法層的約束需求，對語義層約束也未涉及。 2.3 函數(shù)式語言泛型約束 將泛型程序設(shè)計引入現(xiàn)代函數(shù)式語言(如Haskell?98、ML等)中是當(dāng)前研究的一大熱點，其基本思想是在類型結(jié)構(gòu)上歸納定義函數(shù)。 2.3.1 System F 泛型程序設(shè)計的思想源于20世紀60年代的函數(shù)式編程語言LISP，LISP提出高階函數(shù)、參數(shù)化多態(tài)的編程方式；類型系統(tǒng)*終實現(xiàn)是在20世紀70年代，主要有兩類： (1)Girard和Reynolds提出的System F； (2)Hindley-Milner類型系統(tǒng)。 System F[3，4]是由邏輯學(xué)家Jean-Yves Girard和計算機科學(xué)家John C. Reynolds分別獨立設(shè)計的。System F提出了一種多態(tài)性的λ演算，構(gòu)成了Haskell、ML等程序語言參數(shù)化多態(tài)的理論基礎(chǔ)。System F的定義非常簡明，其語法只支持兩類特性，即函數(shù)和泛型，并且只支持一個參數(shù)。 System F的巴克斯-諾爾范式(Backus-Naur form，BNF)文法如下： System F的類型規(guī)則如下： 其中，代表e被定義為類型，且在范圍內(nèi)。在中是抽象，其形參變量是x，類型為，體部分是e，類型為。代表的輸入?yún)?shù)類型為，輸出參數(shù)類型為。在中，是泛型需求，代表任何符合泛型需求的類型。 2.3.2 Haskell 98 Haskell 98由低到高定義了三類層次結(jié)構(gòu)[38]，即值(value)、類型(type)和類屬(kind)，將結(jié)構(gòu)強加于較低層次后可獲得較高層次。定義參數(shù)化類型需要類屬這一層次結(jié)構(gòu)。 例2-1 用Haskell 98描述比較數(shù)據(jù)相等性的泛型模式舉例。 記相等函數(shù)為EqT，其中下標(biāo)T指定了函數(shù)EqT能夠操作(運算)的數(shù)據(jù)類型，[T]為以T類型為基類型的序列類型。 此處的A為類屬，所有可比較的具體類型(如int、char等)均可作為A的模型。 例2-2 用Haskell 98
書友推薦
- >
煙與鏡
- >
回憶愛瑪儂
- >
李白與唐代文化
- >
名家?guī)阕x魯迅:朝花夕拾
- >
羅曼·羅蘭讀書隨筆-精裝
- >
羅庸西南聯(lián)大授課錄
- >
莉莉和章魚
- >
史學(xué)評論
本類暢銷
