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