內容簡介
《軟體工程卷1:抽象與建模》主要內容簡介：《軟體工程卷1～3》是馮諾依曼獎章獲得者、世界著名的計算機科學家DinesBjorner教授的最新著作。這套叢書為讀者理解軟體和軟體開發過程提供了一個“全新的視角”。這三卷書首次系統地論述了如何用形式方法來指導領域工程、需求工程和軟體設計，即軟體工程的三個相互關聯並重疊的組成部分，或稱之為軟體工程的“三部曲”。在軟體開發的各個階段，如果都能夠採用這種形式化的開發模式，將能夠在極大程度上保證軟體開發的正確性和有效性。
這套叢書可以被視為軟體工程史上里程碑式的著作。作者通過長達30年的程式設計方法論的研究與實踐，加上長達25年不斷完善的課程講義彙編成這一套前後連貫、內容一致以及相對完整的軟體工程著作。這套叢書的一個顯著特點就是在這三卷書中，所有的原理、技術和工具都是通過大量的案例分析來進行闡述，並覆蓋了所有主要的軟體開發時期、階段和步驟；同時，這些原理、技術和工具是能夠套用在大型工業和商業軟體的開發項目中去的。
這套叢書不但可以作為高校計算機專業學生、教師以及研究人員的教材和必備參考書，而且在工業和計算機產業界也具有極大的實用價值。
《軟體工程卷1：抽象與建模》介紹了抽象與建模的基本原理和技術。首先，本卷給出了離散數學的基本介紹，包括數、集合、笛卡爾、類型、函式、入-演算、代數和數理邏輯，然後講授基本的面向屬性與面向模型的規約的基本原理和技術。一些其他的規約語言，比如B、VDM-SL和Z都具有面向模型的概念，本卷則通過RAISE規約語言RSL來講解這個概念。本卷還介紹了有關套用式（函式式）、命令式和並髮式（並行式）規約程式設計的基本原則。最後，本卷給出了一個全面的軟體工程術語表以及大量的索引和參考文獻。
《軟體工程卷2：系統與語言規約》介紹了描述系統與語言的規約的基本原理和技術。首先，本卷講授一些高級的原理和技術：分層與組合、指稱與計算以及構型：環境與狀態的抽象與建模，然後講授符號學建模的基本原理和技術：語用、語義以及系統和語言的句法。其中重要的一部分介紹了對空間和簡單時態現象進行建模的基本原理和技術。本卷的主要章節用於介紹一些專門的主題，比如模組（包括UML的類圖）、Petri網、活動序列圖、狀態圖和時態邏輯（包括時段演算）。最後，本卷介紹了開發函式式，命令式以及並行程式設計語言的可靠和有效的解釋器和編譯器的基本原理和技術。本卷適合於作為高年級本科生和研究生，以及研究程式設計方法學的學者的教材或參考書。
《軟體工程卷3：領域、需求與軟體設計》介紹了整體軟體開發的基本原理和技巧：從領域描述，經過需求分析，直到軟體設計。本卷倡導一種全新的軟體工程開發模式：在需求被形式化之前，人們必須理解套用領域，因此本卷首先介紹領域描述的原理和技術，然後介紹從領域模型導出需求規則的原理和技術，最後介紹細化需求到軟體設計的原理和技術：體系結構和組件設計。
目錄
原著作者為中文版所作的序
譯者序
前言
叢書成因
叢書的不足
著手方法
軟體新觀
“輕量級”形式技術
“超級程式設計師
何為軟體工程
作者的願望
這幾卷在軟體工程教育課程中的作用
為什麼這么多材料
課程中如何使用這套叢書
本書的簡要介紹
本卷的簡要介紹
致謝
開篇
緒論
1.1 準備
1.2 軟體工程三部曲
1.2.1 軟體和系統開發
1.2.2 三部曲引出
1.2.3 領域工程
1.2.4 需求工程
1.2.5 軟體設計
1.2.6 討論
1.3 文檔
1.3.1 文檔種類
1.3.2 時期、階段和步驟文檔
1.3.3 信息文檔
1.3.4 描述文檔
1.3.5 分析文檔
1.4 形式技術和形式工具
1.4.1 關於形式技術和語言
1.4.2 軟體工程教材中的形式技術
1.4.3 一些程式設計語言
1.4.4 一些形式規約語言
1.4.5 目前形式語言的不足
1.4.6 其他的形式工具
1.4.7 為什麼要形式技術和形式工具
1.5 方法和方法學
1.5.1 方法
1.5.2 方法學
1.5.3 討論
1.5.4 元方法學
1.6 軟體基礎
1.6.1 教學法和範式
1.6.2 語用、語義和句法
1.6.3 規約和程式設計範式
1.6.4 描述、規定和規約
1.6.5 元語言
1.6.6 總結
1.7 目標和效果
1.7.1 目標
1.7.2 效果
1.7.3 討論
1.8 文獻評註
1.9 練習
離散數學
數
2.1 引言
2.2 數符和數
2.3 數的子集
2.3.1 自然數：Nat
2.3.2 整數：Int
2.3.3 實數：Real
2.3.4 無理數
2.3.5 代數數
2.3.6 超越數
2.3.7 複數和虛數
2.4 類型定義：數
2.5 總結
2.6 文獻評註
2.7 練習
集合
3.1 背景
3.2 數學的集合
3.3 特殊集合
3.3.1 外延公理
3.3.2 劃分
3.3.3 冪集
3.4 分類和類型定義：集合
3.4.1 集合抽象
3.4.2 集合類型表達式和類型定義
3.4.3 分類
3.5 RSL中的集合
3.6 文獻評註
3.7 練習
笛卡爾
4.1 要點
4.2 笛卡爾值表達式
4.3 笛卡爾類型
4.4 笛卡爾的目
4.5 笛卡爾的相等
4.6 一些構造的例子
4.7 分類和類型定義：笛卡爾
4.7.1 笛卡爾抽象
4.7.2 笛卡爾類型表達式和類型定義
4.8 RSI.中的笛卡爾
4.9 文獻評註
4.10 練習
類型
5.1 值和類型
5.2 現象和概念類型
5.2.1 現象和概念
5.2.2 實體：原子和複合
5.2.3 屬性和值
5.3 程式設計語言類型概念
5.4 分類或抽象類型
5.5 內建和具體類型
5.6 類型檢查
5.6.1.類型確定的變數和表達式
5.6.2 類型錯誤
5.6.3 類型錯誤檢測
5.7 類型作為集合，類型作為格
5.8 總結
5.9 練習
函式
6.1 概述
6.2 要點
6.2.1 背景
6.2.2 一些函式概念
6.3 數是如何產生的
6.4 關於求值概念的題外話
6.4.1 求值，解釋和細化
6.4.2 兩個求值的例子
6.4.3 函式調用
6.5 數代數
6.5.1 代數
6.5.2 數類型
6.5.3 高階函式類型
6.5.4 非確定性函式
6.5.5 常量函式
6.5.6 嚴格函式
6.5.7 嚴格函式和嚴格函式調用
6.5.8 數上的操作
……
簡單RSL
規約類型
規約程式設計
其他
附錄
參考文獻
