出版時間:2009-1 出版社:國防工業(yè)出版社 作者:王宏生 頁數(shù):231
內(nèi)容概要
Z形式規(guī)約是一種世界上廣泛使用的軟件規(guī)格說明語言,在軟件開發(fā)的需求規(guī)格說明階段和軟件設(shè)計階段都可以使用,對于提高大型軟件質(zhì)量、驗證軟件設(shè)計正確性等方面具有非常重要的意義。 由于Z是以集合論和一階邏輯為基礎(chǔ),是設(shè)計用來給人看的而不能由機器執(zhí)行。將Z轉(zhuǎn)換成高級語言需要專業(yè)的數(shù)學知識,而且對于大型軟件,轉(zhuǎn)換過程極易出錯。Z的機器可執(zhí)行性已經(jīng)引起世界范圍的關(guān)注,但目前還不能直接從Z語言自動生成應用程序,Z到可執(zhí)行代碼的轉(zhuǎn)換主要由人工完成。本書指出了Z語言求精方法對于自動生成應用程序的不足,提出了對Z規(guī)格說明做一定限制后的Smart Z自動求精為C++和STL方法?! ”緯鴶⑹龊喢髑逦?,邏輯性強,可作為高等學校相關(guān)專業(yè)研究生和從事形式語言研究、大型軟件形式化開發(fā)與應用的專業(yè)人員參考。
書籍目錄
第1章 Z形式規(guī)約 1.1 軟 件開發(fā)的形式化方法 1.2 Z形式規(guī)約的類型 1.3 Z形式規(guī)約的構(gòu)造單元 1.4 Z形式規(guī)約的關(guān)系和函數(shù) 1.5 Z形式規(guī)約求精技術(shù)第2章 ++標準模板庫STL 2.1 STL簡介 2.2 STL基本結(jié)構(gòu) 2.3 容器 2.4 迭代器 2.5 算法 2.6 其他組件第3章 Z形式規(guī)約的精簡—Smart Z 3.1 概述 3.2 Z形式規(guī)約的類型約束 3.3 Z形式規(guī)約的謂詞約束 3.4 Z形式規(guī)約的精簡第4章 Smart Z的自動求精 4.1 Smart Z的詞法分析 4.2 Smart Z的語法分析 4.3 Smart Z的語義分析 4.4 Smart Z的自動求精轉(zhuǎn)換器第5章 一階邏輯算子的自動求精 5.1 一階邏輯 5.2 一階邏輯算子的自動求精步驟 5.3 表達式處理 5.4 Smart Z的量詞與連接詞的自動求精 5.5 一階邏輯算子的目標代碼生成 5.6 一個模式求精實例第6章 集合論算子的自動求精 6.1 集合類型的聲明 6.2 目標代碼中的集合操作 6.3 集合論算子到中間代碼的轉(zhuǎn)換 6.4 采用模板及重載技術(shù)設(shè)計Smart Z中集合論算子的求精 6.5 集合論算子自動求精實例第7章 冪集算子的自動求精 7.1 冪集類型 7.2 廣義表 7.3 單層冪集的自動求精 7.4 多層嵌套冪集的自動求精 7.5 冪集的自動求精實例第8章 笛卡兒積的自動求精 8.1 笛卡兒積的聲明 8.2 笛卡兒積的數(shù)據(jù)求精 8.3 笛卡兒積的過程求精48 8.4 笛卡兒積的自動求精實例第9章 關(guān)系和函數(shù)的自動求精 9.1 序偶與關(guān)系 9.2 關(guān)系操作與自動求精 9.3 函數(shù)操作與自動求精第10章 序列和包的自動求精 10.1 序列和包 10.2 序列操作的自動求精 10.3 包操作的自動求精 10.4 序列和包的自動求精實例附錄1 Z語法附錄2 Smart Z詞法附錄3 Smart Z的詞法附錄4 Smart Z語法附錄5 Smart Z語法的部分SI-NS圖附錄6 部分Smart Z算子的函數(shù)模板參考文獻
章節(jié)摘錄
第1章 z形式規(guī)約1.1 軟件開發(fā)的形式化方法1.1.1 形式化方法的意義軟件開發(fā)的過程是從對用戶的需求進行分析開始的,經(jīng)過設(shè)計和實現(xiàn),最后產(chǎn)生可以正確執(zhí)行的代碼以及有關(guān)使用和維護的各種文檔。完成這個過程的方法稱為軟件開發(fā)方法。傳統(tǒng)的軟件開發(fā)方法引入一些非形式的圖形和文字符號,提供一定的設(shè)計原則,協(xié)助開發(fā)人員按照一定的步驟,比較明確和簡練地書寫設(shè)計文檔,用人工方式開發(fā)出所要的軟件。從各軟件加工模型來看,用戶需求的規(guī)格說明在軟件開發(fā)過程中具有非常重要的地位。其使用者包括用戶、系統(tǒng)分析員、設(shè)計與編程人員、測試和驗收人員。許多軟件項目開發(fā)的經(jīng)驗表明,軟件開發(fā)費用的大部分是用于糾正在測試階段所發(fā)現(xiàn)的各種錯誤。而更詳細的調(diào)查告誡我們,這些錯誤中的很大一部分可追溯到項目開發(fā)的早期階段,即在實現(xiàn)和測試階段所花的高額費用是由于需求分析和設(shè)計階段虛假的“節(jié)省”所引起的。需求分析階段的錯誤通常就是規(guī)格說明的描述不精確。眾所周知,采用自然語言描述的非形式的規(guī)格說明具有易讀、易理解的優(yōu)點,但它通常具有模糊性和歧義性(二義性),經(jīng)常是不精確和不完整的。這往往引起規(guī)格說明的使用者對同一規(guī)格說明產(chǎn)生不同的理解,最終導致用戶對已完成的系統(tǒng)不滿意。
編輯推薦
《Z形式規(guī)約的自動求精研究》由國防工業(yè)出版社出版。
圖書封面
評論、評分、閱讀與下載