软件规格说明技术
第1章 绪论
软件工程是研究大规模程序设计的方法、工具和管理的工程科学。软件工程的要点是大规模程序设计。
20世纪60年代末出现的“软件危机”，其主要表现在于软件质量差，可靠性难以保证；软件成本增长难以控制，只有极少软件能在预订的成本预算内完成；软件开发进度难以控制，周期拖得很长；软件的维护很困难，维护人员和费用不断增加。
造成软件危机的主要原因在于软件开发过程本身的复杂性以及软件工程作为一个职业相对还不够成熟。
IEEE给出的软件工程的定义：
软件工程是：（1）将系统化的、严格约束的、可量化的方法应用于软件的开发、运行和维护，即将工程化应用于软件。（2）在（1）中所述方法的研究。
1.1 软件生命周期
Pressman给出了关于软件的一个较为综合的定义：软件是①当它被执行时提供希望功能和性能的指令；②使得程序能够适当地操作信息的数据；③描述程序的操作和使用文档。简而言之，软件=程序+数据+文档。
软件开发的过程包括把用户的需求（Requirements）转化为软件需求规格说明（Specification），把软件需求规格说明转化为设计，用代码来实现设计，对代码进行测试，文档编制并确认它可以投入使用的过程。
典型的软件生命周期，通常称之为瀑布模型。几乎其他的软件开发模型，如螺旋模型、演化模型、原型模型等都使用了瀑布模型作为基础。
典型的瀑布模型生命周期模型由下面5个阶段组成：需求分析和规格说明，设计，实现，测试以及交付与维护阶段。
有两种不通的方法可以进行程序测试：功能测试和结构测试。这两种测试方法是按照他们的目的以及产生测试用例的不同的方法区分的。功能测试，同样也被称为“黑盒测试”，目的是为了发现导致违反规格说明与程序之间一致性的故障，并且测试用例通常是基于功能规格说明（需求规格说明或者是设计规格说明或者两者）产生的。结构测试，则被称为“白盒测试”，这种方法按照程序内部的逻辑测试程序，检验程序中的每条路径是否都能按照规定的要求正确工作。白盒测试的测试用例是根据程序的结构产生的。对于程序测试而言，功能测试和结构测试都是必需的，因为两者在发现故障方面是互补的。从本质上而言，测试是一个交互的过程，因此测试是一个劳动密集型的过程。
1.2 存在的问题
Davis等人指出：高质量的软件需求规格说明能提高软件开发的质量并且节省软件的开发费用。主要有以下三个重要原因：需求错误通常比其他错误多花费10倍时间来修复；需求错误通常占软件项目总错误的40%以上；需求错误的稍微减少能显著地降低返工成本和日程延期。
1.3 形式方法
形式方法包含两种技术：形式规格说明技术和形式验证技术。
软件开发的形式方法是一种提供了描述软件产品，如规格说明、设计和源代码的形式语言，并支持对描述的产品的性质进行推理和验证的方法。
形式验证的主要技术包括定理和模型检查。定理证明技术是形式方法的核心，定理证明系统是由一个形式语言和推理机制构成的形式系统。模型检查是一种自动验证系统正确性的方法，它已经被成功地应用到许多实际问题中，包括硬件设计、协议分析、交互式系统分析等问题。
形式规格说明语言的分类：基于模型的方法，面向模型的形式方法有时也称基于状态的形式方法；代数方法，为目标软件系统的规格说明提供了一些特殊的机制，以允许对目标软件系统描述的结构化，并支持目标软件系统中公共元素的重用；进程代数方法。
形式方法的优点：形式规格说明是精确的；由误解引起的错误减少；形式规格说明利于系统实现；能够对形式规格说明进行正确性证明。
形式方法的缺点：形式规格说明难以阅读；形式方法并不能对客观世界的所有方面进行模型化；形式规格说明的正确性证明费时费力；尚未出现支持形式方法全过程的软件环境。
第2章 一阶逻辑与集合论
Z语言是基于一阶逻辑和集合论的形式规格说明语言。
2.1 命题逻辑
命题是具有确定真假意义的陈述句。
命题与连接词
若公式G在所有的解释I下，其真值都为T，则称该公式是永真式，又称重言式（tautology）；如果公式G在所有的解释I下，其真值都为F，则称该公式是永假式；如果公式G不是永假式，则称该公式是可满足的。
2.2 谓词逻辑
带有参数的命题称为谓词。如果一个谓词带有n个参数，则称该谓词是n元谓词。
“对任意x”在谓词逻辑中记作“$\forall x$”，其中”$\forall$“称为全称量词；”存在一个x“在谓词逻辑中记作”$\exists x$“，其中”$\exists$“称为存在量词。而x是一个变量，称为约束变量。
通常称变量x在谓词公式($\exists x$)A和($\forall x$)A中的出现为约束出现；并称A为($\exists x$)A和($\forall x$)A的作用域（或辖域）。如果变量x在公式A中的某次出现是在A的分子公式中的约束出现，则称x的该次出现是约束出现；若变量x在公式A的某次出现不是约束出现，就称该出现为自由出现。在公式A中自由出现的变量称为自由变量，在公式A中约束出现的变量称为约束变量。
2.3 一阶逻辑中的证明
一个形如$\Gamma \vdash A$的符号相继式（简称相继式），其中$\Gamma$是一阶逻辑中的公式集合，$\vdash$称为“推出”符号，A是公式，$\Gamma \vdash A$就可读作：“$\Gamma$推出A”或“A由$\Gamma$推出”。通常称集合$\Gamma$为前提，而A为结论。经过证明的这个相继式就称为定理。
点规则（One-point Rule）：即若已有一个含存在量词的命题公式，其中对量词变量给定了一个确定值，则可以消去量词，用已知值来替换所出现的量词变量。
$$
\exists n:N \bullet (n<10\landn=23)等价于23\in N\land23<10
$$
式子的第一部分确保这一项是自然数集的一个元素，第二部分即对谓词进行替换，得$23<10$。
2.4 集合论
“$==$”是定义符号，可读作“定义为”。例如，$A=={x|x是能被3整除的自然数}$、$B=={y|y^3+y^2-y=80}$等。
集合谓词：属于$\in$、包含$\subset \supset$、真包含$\subsetq \supsetq$。
集合运算：并$\cup$、交$\cap$、差$\setminus$、广义并$\bigcup$、广义交$\bigcap$。
设A、B是任意两个集合，若序偶的第一元素是A的一个元素，第二个元素是B的一个元素，则所有这样的序偶集合，称为“集合A、B的笛卡尔积”，记作“$A\times B$”。即$A\times B=={(x, y)|x\in A，且y\in B}$。
设任由任意n个集合$A_1$、$A_2$、$\dots$、$A_n$构成的新集合${(a_1, a_2, \dots, a_n)|a_i \in A_i, i=1, 2, \dots, n}$称为$A_1$、$A_2$、$\dots$、$A_n$的笛卡儿积，记作“$A_1\times A_2 \times \dots \times A_n$”。
第3章 Z的类型与构造单元
3.1 Z的类型系统
基本类型是Z的类型系统中的重要组成部分，对基本类型重复使用类型构造符，可构造出其他的类型。现介绍两个复合类型：幂集类型和笛卡儿积类型。另外还有两个符合类型：序列和包（第6章）。
3.2 扩充表示法
表示“集合中元素的个数”的操作符，在Z中，使用操作符“#”可得到集合中的元素个数。
用声明加限制的组合表示集合，其一般形式为：
$${Decls|Pred}$$
有时并不希望集合的元素是由声明Decls的表所确定的元组，而想自由地选择某些元素。Z扩充了集合表达式原有的表示，增加了一个指明集合元素形式的部分。扩充后的集合表达式定义形如：
$${Decls|Pred\bullet ExPr}$$
它表示了所有这样的值的集合，这些值是由Decls中满足限制Pred的变量以ExPr项的形式确定的。竖线“|”将声明和限制分割开来，称为“限制条”（ConstraintBar），黑原点将限制与表达式项分隔开来。整个表示以一对花括号括起。
若想定义a到b之间（包括a和b）的所有整数的集合，就可以直接使用a..b的表示。“..”称做数域。
3.3 Z规格说明的构造单元
公理定义（Axiomatic Definition），引入了一个或多个全程变量和关于它们的谓词，这些谓词给出了进一步的信息。这些变量不能是前面已经定义的变量。它们的作用域为它们的声明出现处至整个规格说明的结束处。而谓词也具有全程的性质。
图3-1声明部分和谓词部分都可以不出现。
Z的模式的两个主要用途：①说明软件系统的状态；②说明状态的转化。
通用式定义（Generic Definition），又叫通用式常量。
第4章 关系和函数
4.1 关系
X到Y的所有关系的类型被写成$X\leftrightarrow Y$，事实上它就是$ℙ(X\times Y)$。这样定义X到Y的所有关系类型的标准写法为：
$$X\leftrightarrow Y==ℙ(X\times Y)$$
即集合X到集合Y的任一关系是$ℙ(X\times Y)$的一个元素。这里X和Y可以是相同的集合，$X\leftrightarrow Y$是$ℙ(X\times Y)$的简写形式。可用这种表达形式来声明关系。在Z中，$(x,y)$经常被写成$x\mapsto y$，读作“x映射到y”。
如果R是一个类型为$X\leftrightarrow Y$的关系，通常可以dom R来表示R的定义域，以ran R来表示R的值域。对于任何关系R、dom R和ran R可以用集合表达式形式地表示为：
$$dom R == {x:X | \exists y: Y \bullet x \mapsto y \in R} \ ran R == {y: Y | \exists x:X \bullet x \mapsto y \in R}$$
4.2 关系的运算
恒等关系的一般定义：设X是任意的集合类型。$id X=={x:X\bullet x \mapsto x}$
整数集Z上的“等于”是恒等关系中的一个典型例子。
关系逆的一般定义为：对任何类型为$X\leftrightarrow Y$的关系R，它的逆关系为：$R^~=={x:X; y:Y | x\mapsto y \in R \bullet y\mapsto x}$。
对任何类型为$X\leftrightarrow Y$的关系R，设S是定义域类型X的一个集合，则
$$S\triangleleft R =={x:X; y:Y | x\in S \landx\mapsto y \in R \bullet x\mapsto y}$$
可简写为：$S\triangleleft R =={x:X; y:Y | x\in S \land x\mapsto y \in R}$
对任何类型为$X\leftrightarrow Y$的关系R，设T是定义域类型Y的一个集合，则
$$R\triangleright T =={x:X; y:Y | y\in T \landx\mapsto y \in R}$$
与限定运算相类似，定义域限定减和值域限定减的运算可以被一般地描述为：
$$S⩤R =={x:X; y:Y | x\notin S \land x\mapsto y \in R} \ R⩥T =={x:X; y:Y | y\notin T \landx\mapsto y \in R}$$
4.3 函数
函数的性质可以形式地描述为：设R是一个类型为$X\leftrightarrow Y$的关系，则
$$(x\mapstp y)\in R \land (x\mapsto z)\in R \Rightarrow y=z$$。它说的是，如果x既关联y又关联z，那么y和z是同一个元素。
部分函数的一般定义：
$$
X⇸Y=={R:X\leftrightarrow Y | (\forall x:X; y; z:Y \bullet (x\mapsto y)\in R \land (x\mapsto z)\in R \Rightarrow y=z}
$$
全函数是一个函数，且其定义域是整个源集。
$$
X\rightarrow Y == {f:X⇸Y|dom f = X}
$$
函数叠加的形式定义可叙述为：设f和g都是类型为X⇸Y的函数，这里X是源集，Y是目标集，则$f\oplus g==((dom g)⩤f)\cup g$。其含义表明，对一个dom f或dom g中的元素x: X，如果$x\in dom g$，则$(f\oplus g)x=g x$；如果$x\notin dom g$但$x\in dom f, (f\oplus g) x = f x$。“$f\oplus g$”可读作“g叠加到f”。
𝜆-表达式采用的是人们较熟悉的形式，由声明加上谓词在跟上一个项的结构组成。其一般形式为：$\lamda decls | pred \bullet term$，该表达式以decls | pred为自变量，将它们映射到由term所定义的值。因此，𝜆-表达式$\lamda x_1: X_1; \dots; x_n: X_n |P\bullet t$就等价于由集合表达式描述的函数${x_1: X_1; \dots; x_n: X_n | P\bullet (x_1, \dots, x_n)\mapsto t}$，谓词部分是任选的。