软件工程形式化方法.md

形式化方法

现实世界中的问题很难直接解决，需要先形式化抽象化问题到符号世界，就可以利用已有的逻辑、数学方法和计算工具来解决，得到一个形式化的解，再重新解释回现实世界

把实际的问题表达成形式化问题的工具就是Z notation

逻辑和集合论是所有数学学科的基础

由前提得到结论是由逻辑完成的

形式化概念

既有形式化的文法又有形式化的语义

通常，形式化意味着数学和逻辑的

例如：数理逻辑是典型的形式化表达方式

半形式化

有形式化语法但不一定有形式化语义

验证

一定要先表达成形式化内容，如果不是形式化的就无法验证

形式化方法验证的背景

发现错误的时间明显滞后于引入错误的时间，纠正错误的成本会越来越高

应当尽早发现错误，纠正错误

软件工程是用工程的方法

软件开发的发展

软件开发初始阶段

直接开始编码实现

软件开发传统方法

需求分析-定义-明确规格-设计-编码-实现

软件开发现代方法

需求分析、定义-形式化规格验证-设计-验证-编程-实现

使用形式化方法进行开发，直接导出代码

Specification

单词有两个意思，一个是规格结果，一个是规格化的过程

一个好的specification，没有二义性、完整的、可验证的、一致的

Formal specification是什么

为什么要用形式化方法/数学的目的

数学是稳定的、抽象的，可以应用到各个领域，可以作为一个相对正确性的基础。 将其他事物的正确性建立在数学的正确性之上

数学是严格的，没有二义的

数学是符号化的、简洁的

数学可以来做验证

验证是什么

检查正确性的过程

是否满足给定的条件

Verification and Validation 验证和验收

验证是用数学方法，验收一般不用数学方法

形式化验证

形式化前提之下，是否能得到目标

软件规格的作用

作用

• 相当于一个起跑线，基础。Specification的正确性是软件开发的基础
• 如果没有，软件复杂性无法控制

规格的描述

功能性

系统必须做的事情

非功能性

系统应该做的事情

规格的目标

完整……

规格的好处

可以控制系统开发过程等等

哪些内容需要明确

• 对象属性
• 正确性条件
• 可观察的行为

何时描述

多个阶段都可以，分阶段做

规格的验证

需要满足常识性的问题

可以用形式化方法，也可以用非形式化方法

一些非常普遍的性质

安全性、公平性等

第二课 集合论知识

最基本的思想：把一群类似的东西看作一个整体

互相之间能够区别的元素形成的集合，也就是不能有重复元素

空集

有穷集合

一定可以数出元素数量，叫做集合的尺寸

无穷集合

没有尺寸的概念

无穷大是实实在在存在的，不同的无穷大会有“大小”

比如自然数集合N和自然数平方$N^2$，$N^2$是N的真子集。

但N^2和N的浓度相等，因为可以建立两者的一一对应关系

如果有集合是N的超集，且无法建立起两者的一一对应关系，则它的浓度比N大，比如自然数的幂集P(N)={{0},{1},...,{0,1}...{0,1,2,3}...}。P(N)和实数R的浓度一样多

定义集合的方法

• 列出所有元素（有穷）
• 定义性质

子集

有序对

$(a,b)=_{df}{{a},{a,b}}$

$(a,b)\neq (b,a)$

笛卡尔积

$A\times B=_{df}{(a,b)|a\in A,b\in B}$

关系

二元关系

从集合A到集合B的关系，A叫做source，B叫做target，写成$R:A\to B=R\subseteq A\times B$，是笛卡尔积的子集

$A\to B$定义的是一个抽象的关系，会有具体的实例

任何二元关系是有序对的集合

定义域：针对A中元素a，如果至少存在一个B中元素b与之对应，则a在定义域内。定义域是from set的子集

值域：B中元素b，存在A中元素与之对应，则b在值域内。值域是to set的子集

对于关系来说，一对一、一对多、多对一都可以

函数

不允许一个元素对应于多个元素的关系。

$f:A\to B=_{df}f\subseteq A\times B\land (\forall x)(\forall y)(\forall z)((x\in A\land y\in B\land z\in B)\Rightarrow (((x,y)\in f\land (x,z)\in f)\Rightarrow y=z)$

没有限制多个元素对应一个元素

Injection

单射，只允许一对一

Surjection

满射，target中的每一个元素都被映射到。即值域和target相同。

没有限制其他条件

全射

source和定义域相同

Bijection

一一对应，Source和定义域相同，target和值域相同，且只允许一对一。全射、满射、单射都满足

第三课

基于状态的specification

先定义变量

不变式

不管状态怎么转移，都必须被遵守

赋初值

定义操作（前一个状态和后一个状态的关系）

定义询问

Z notation Specification的结构

• Introduction（自然语言的）
• specification中使用的类型
• 状态和不变量
• 初值
• 操作和询问
• 错误处理
• 最终版本合成

基本类型

自由类型

幂集中的元素一定是集合

Z语言中的集合

Membership

是集合的元素且在幂集元素内

Non-membership

x是集合X的元素但不在幂集元素S内

x如果根本不是集合X的元素，则根本无法讨论

幂集

所有的子集的集合

包含关系

并 Union

交 Intersect

差 Difference

S\T

多个集合交和并

不相交集合 Disjoint

分割 Partition

等价关系

(a,a)

对称关系

(a,b)=(b,a)

推移关系

(a,b),(b,c)=>(a,c)

分割

分割$P={A,B,C},\cup{A,B,C}=S,A\cap B=A\cap C=B\cap C=空集$

可以由分割导出等价类

例子

飞机乘客，没有座位号，先来先服务，固定容量，每个乘客可识别

基本类型

[PERSON] the set of all uniquely identified persons

变量 capacity:N_1(飞机座位容量) onboard:P PERSON(已经在飞机上的乘客的集合)

不变式

不管飞机状态怎么转移都遵守 $#onboard\leq capacity$

初始值

onboard'=空集(空集=onboard') Z里面没有赋值，所有内容都是静态的 '代表下一个状态。这里是指不管onboard之前的值，它下一个状态一定是空集

定义操作

上飞机

$p:PERSON$ $p\notin onboard$ $#onboard<capacity$ $onboard'=onboard\cup {p}$

下飞机

p:PERSON $p\in onboard$ $onboard'=onboard\setminus {p}$

询问操作 Enquiries

Number on board

numOnboard:N
numOnboard=#onboard
onboard'=onboard
最后一句代表新状态和老状态一样，每个询问都要写

Person on board

RESPONSE ::=yes|no

p:PERSON
reply:RESPONSE
$((p\in onboard\land reply=yes)\lor(p\notin onboard\land reply=no))$
onboard'=onboard

例子的缺陷

没有考虑到错误的情况

扩充

RESPONSE:=OK | twoErrors | onBoard | full | notOnBoard

来处理系统出现错误的时候的情况

上飞机操作

p:PERSON
reply:RESPONSE

$(p\notin onboard\land #onboard<capacity\land onboard'=onboard\cup {p}\land reply=OK)$ $\lor$ $(p\in onboard\land #onboard=capacity\land onboard'=onboard\land reply=twoErrors)$（双重错误，人已经在飞机上却还要上飞机，而且飞机已满） $\lor$ $(p\in onboard\land # onboard<capacity\land onboard'=onboard\land reply=onboard)$（人已经在飞机上还要上飞机，飞机没满） $\lor$ $(p\notin onboard\land # onboard=capacity\land onboard'=onboard\land reply=full)$（人不在飞机上上飞机，但飞机已满）

下飞机

只有一个错误：人不在飞机上还要下飞机 $(p\in onboard\land onboard'=onboard\setminus {p}\land reply=OK)$ $\lor$ $(p\notin onboard\land onboard'=onboard\land reply=notOnBoard)$

第五课

Schemas

文本形式：
$S==[a,b:N|a<b]$

性质：
$a\in N\land b\in N\land a<b$

通常形式：
|——SchemaName—— |Declarations 多个定义 |—————————— |Predicate 一个谓词 |——————————

==相当于定义

Name

定义之后在文档中任何地方都可使用

相当于类型名

定义

包含若干个变量和类型，它的辖域只在schema中

不同行定义用;分隔

之前定义的可以在后面使用

Signature

变量集合

Ex:$a:N;b:N$

谓词

并在一起的一个

无名schema

没有谓词的schema

局部变量

定义在schema内部的

全局变量

没有名字的schema用来定义全局变量

没有谓词的 |Declarations

或者有谓词的 |Declarations |———————————— |Predicate

Schema type

Schema calculue 演算

Decoration

新的状态也满足同样的条件

S'= |——S'—— |a',b':N |————— |a'<b' |————

Inclusion

把S写到另一个Schema的宣言里面，则该schema也要满足S的所有要求 |——IncludeS———— |c:N |S |———— |c<10 |————

= |——IncludeS—— |c:N |a,b:N |———— |c<10 |a<b (c<10且a<b) |————

Conjunction

相同名字的变量同时满足两个Schema的条件（这是故意让同名变量一样） |——T—— |b,c:N |———— |b<c |————

S and T= |——S and T—— |a,b,c:N |———— |a<b |b<c (a<b且b<c) |————

Disjunction

S or T= |——S or T—— |a,b,c:N |———— |a<b 或 b<c |————

Delta Convention

前一个状态和后一个状态的变量同时出现在Schema，还要满足一定关系 $\Delta S=_{df}S\ and\ S'$

$\Delta S$= |——$\Delta S$—— |a,b:N |a',b':N |———— |a<b |a'<b' |——————

Xi Convention

$\Xi S$代表S和S'的值没变

$\Xi S$= |——$\Xi S$—— |a,b:N |a',b':N |———— |a<b |a'<b' |a=a' |b=b' |————

Renaming 重命名

newSchemaName== oldSchemaName[newName1/oldName1,newName2/oldName2,...]

Ex: T=S[c/b]

Hiding 隐藏

把明白定义的变量变成隐含的变量，以谓词的方式引入约束变量

约束变量、自由变量

$\sum\limits^n_{k=1}kx+y$ 中k是约束变量，x，y是自由变量

BHidden==S\(b)

|BHidden———— |a:N |———— |$\exists b:N\cdot a<b$

Projection

newSchemaName==oldSchemaName $\uparrow$(varName) 隐藏所有没写出来的变量

AProjected==S$\uparrow$(a)

|——Aprojected—— |a:N |———— |$\exists b:N\cdot a<b$

Composition

合成

S;T 先有S的效果，在此效果之上才有T的效果

输入输出变量

输入

用问号?写在变量后面表示输入变量

输出

用惊叹号!写在变量后面表述输出变量

|Add———— |a?,b?:N |sum!:N |—————— |sum!=a?+b? |——————

输入的例子

页编辑 KEY::=home|return|left|right|up|down

|numLines:N |numColumns:N |—————— |$1\leq numLines$ |$1\leq numColumns$

$CursorControlKey==HomeKey\lor ReturnKey\lor LeftKey\lor RightKey\lor UpKey\lor DownKey$

|——Cursor |line:N |column:N |———— |$line\in 1..numLines$ |$column\in 1..numColumns$

|——HomeKey |$\Delta Cursor$ |key?:KEY |———— |key?=home |line'=1 |column'=1 |————

|——DownKeyNormal |$\Delta Cursor$ |key?:KEY |———— |key?=down |line<numLines |line'=line+1 |column'=column |————

|DownKeyAtBottom |$\Delta Cursor$ |key?:KEY |———— |key?=down |line=numLines |line'=1 |column'=column

|RightKey |$\Delta cursor$ |key?:KEY |___ |key?=right |$(column<numColumns\land column'=column+1\land line'=line)\lor$ |$(column=numLoculmns\land column'=1\land ((line<numLines\land line'=line+1)\lor ()))$

使用Schema描述飞机系统

The types

[PERSON] 所有可识别的人

The state

Initialization operation

|——Init—— |Aircraft' |———— |onboard'=空集

Operations

|——Board0(一般用0表示正常状态) |$\Delta Aircaft$ |p?:PERSON |———— |$p?\notin onboard$ |# onboard<capacity |$onboard'=onboard\cup {p?}$

Enquiry

|——Number |$\Xi Aircaft$ |numOnBoard!:N |———— |numOnboard!=#onboard |————

Dealing with errors

OKMessage==[rep!:RESPONSE | rep!=OK]

|——BoardError—— |$\Xi Aircraft$ |p?: PERSON |rep?: RESPONSE |———— |$((p?\in onboard\land #Onboard=capacity\land rep!=twoErrors))\lor$ |————

Final version of operations

$Board == (Board0)\land OKMessage)\lor BoardError$ $Disembark==(Disembark0\land OKMEssage)\lor DisembarkError$

谓词和量词

谓词

0元谓词，一个命题，不会改变

一元谓词，有一个参数，一个个体有什么性质

二元谓词，就是关系，两个个体之间满足的性质

量词

对谓词的限定

• 全称量词
• 存在量词
• 唯一量词

全称量词

$\forall$ for all

Z里的用法$\forall declaration(定义) | constraint(限制)\cdot predicate(谓词)$

|constraint可以省略

例子 $\forall i:N|i&lt;10\cdot i^2&lt;100$ 对所有比10小的i的平方要小于100，这是真的

如果限定的范围是空集，则认为这个量词式是真的 比如 $\forall i:N|0\leq i&lt;0\cdot i^2&lt;100$ 这是真的

存在量词

$\exists$ exists

至少有一个

如果限定的范围是空集，则认为这个量词式为假

$\exists i:N|i&lt;10\cdot i^2&lt;60 (0^2&lt;60\land \cdots 9^2&lt;60)$ 为真

$\exists i:N|0\leq i&lt;0\cdot i^2&lt;100$ 这是假的

唯一量词

$\exists_1$

有且只有一个符合

$\exists_1 i:N|6&lt;i&lt;10\cdot i^2&lt;60$ 为真 $\exists_1 i:N|5&lt;i&lt;10\cdot i^2&lt;60$ 为假

内含方法描述集合

${declaration~|~constraint\cdot expression}$

${x:Z|Even(x)\cdot x*x}$ 所有偶数的平方的集合

关系

source target R代表X到Y的关系表示法在Z里面如下 $R:X\leftrightarrow Y(X\leftrightarrow Y\in P(X\times Y))$

有序对

$\to$

$x R y==x\to y\in R== (x,y)\in R$

区分抽象关系和具体关系

抽象关系

[COUNTRY] [LANGUAGE]

$COUNTRY\leftrightarrow LANGUAGE$

具体关系

{(GB,English),(China,Chinese)}

Image 像

某一个定义域的子集对应到的值域部分

定义域的像是值域

Infix relation

_R_：$X\leftrightarrow Y$ 中缀表达

关系的逆

R^~^ 把关系的两个元素倒过来

有些关系的逆还是一样，有些不一样

Z中的限制Restriction操作

定义域限制 Domain restriction

$S\lhd R$ 把关系R限制到定义域的子集S对应的关系,新关系的定义域为S

值域限制

$R\rhd S$ 把关系R限制到值域的子集S对应的关系，新关系的值域为S

限制都是把留下的东西清晰地表示出来

标准集合论里没有这个演算

Subtraction 反限制

符号是限制符号中加一个横杠，无法表示，用<+代替

把不需要的东西表示出来

Domain subtraction

关系R中把定义域的子集S相关的关系减掉 S<+ R

Range subtraction

关系R中把值域的子集S相关的关系减掉 R+> S

例子

[COUNTRY] holidays:COUNTRY$\leftrightarrow$DATE EU:P COUNTRY $EU\lhd holidays$欧盟国家的假日 $EU&lt;+ holidays$非欧盟国家的假日

Summer:P DATE $holidays\rhd summer$所有国家夏天的假日 $holidays+&gt; summer$不在夏天的假日

关系的组合（合成）

在第一个关系的基础之上叠加第二个关系

向前合成 Forward composition

$R:X\leftrightarrow Y,Q:Y\leftrightarrow Z,~R;Q:X\leftrightarrow$ $\exists y:Y\cdot x R y\land yQ z$

传递闭包

通过关系的合成将所有关系都包含了 $R^+$ R;R;R... $R:X \leftrightarrow X$

自反关系

X和自己之间的关系 $id\ X={x:X\cdot x\to x}$

自反传递闭包

$R^*==R^+\cup id X$

家族关系的例子

[PERSON] father,mother:$PERSON\leftrightarrow PERSON$ c father代表c has f as father 双亲关系 parent:PERSON\leftright PERSON parent=father\cup mother

兄弟姐妹关系 sibling:PERSON\leftrightarrow PERSON sibling=(parent;parent^~^)\id PERSON

函数

函数本质上是关系

箭头上面画一个竖杠表示

f:X+->Y==f:X<->Y $\exists_1 y:Y\cdot x f y if x\in X$

部分函数

source里有部分没有定义

全函数

source里全部被定义

单射函数

只允许一对一，不能多对一

满射函数

target里所有值都在值域内

一一对应

既是单射也是满射 值域和定义域大小一致，且值域和target相同，定义域和source相同

函数的覆盖

见手工笔记

如何解释schema

Warehouse ITEM是存在仓库里的货物种类 carried是货物种类集合 level是部分函数，定义了仓库里有的货物的自然数个数

谓词部分定义了仓库里的货物和货物种类必须一致

没有更新，=解释成两个值应该相等

sequence 序列

描述顺序关系

特殊的函数，定义在自然数上 用<>

Z里面定义

s:seq X

相当于 s:N+-> X

定义域元素中间不能有间隔，必须是1,2,3,4这样连续的

不一定是单射

$seq_1 X$代表非空

s:iseq X不允许重复，表示单射

flight:seq CITY flight=<Geneva,Paris,London,NewYork> flight={(1,Geneva),(2,Paris),(3,London),(4,NewYork)}

Selection

s是函数，所以可以选择，根据序号挑出元素 $s\ 2=s_2$

Head

头 head s=s 1=s_1

Tail

尾部 从s2到sn

Last 尾

sn

Front 头部

连接Concatenation

s^t=<s1,s2,sm...t1,t2,tn> =<st1,st2,stm...st(m+n)>

过滤 Filtering

向上的箭头

见手工笔记

Restriction

Squash

Reverse 倒置

rev flight 反向

---

基于某些前提，按照逻辑得到结论（不管前提是否正确）

纯粹基于自然语言的逻辑称为普通逻辑

基于集合论、数学的逻辑称为形式化逻辑

演绎证明

1. 选择逻辑系统
2. 确定系统出发需求
3. 确定系统性质
4. 检查是否成立

基于语义的模型检查

Petri 网

相当于二部图

表达能力弱于程序设计语言

扩展petri网

加入禁止输入的条件

ACL Access Control List 访问控制列表

传统的UNIX用户组权限太简单

给一个文件添加一个列表，给每个用户独有的权限