第五章 软件工程中的形式化方法
形式化方法基本概念
形式规约
当规格说明用非形式化方法描述时，可称之为“规格说明”，当规格说明用形式化方法描述时，可称之为“形式规约”。
形式证明与验证
形式证明与验证技术主要包括模型检测和定理证明。模型检测是一种基于有限状态模型并检验该模型的性质的技术。定理证明采用逻辑公式来表示系统规约及其性质。
程序求精
程序求精是将自动推理和形式化方法相结合，从抽象的形式规约推演出具体的面向计算机的程序代码的全过程。程序求精的基本思想是用一个抽象程度低、过程性强的程序去代替一个抽象程度高、过程弱的程序，并保持它们之间功能的一致性。
时态逻辑
Kripke结构 三元组M=（W，R，L）称为模型逻辑的一个模型，或者Kripke结构，其中W是可能世界的非空集合；R包含于W×W是可能世界W上的二元关系；L：W→2^p（P是原子公式集合）是标记函数，它是对各可能世界的真值指派，即对每个模态逻辑公式，指明它在每个可能世界中取真值还是假值。
一阶线性时态逻辑
一阶线性时态逻辑公式，简称FOLTL公式，定义如下：
①原子谓词公式是FOLTL公式；
②如果A、B是FOLTL公式，那么（
A）、（A∧B）、（A∨B）、（A→B）、（A↔B）是FOLTL公式；
③如果A是FOLTL公式，x是A中出现的变量（个体变元），则彐x·A、
x·A是FOLTL公式；
④如果A、B是FOLTL公式，那么（◇A）、（□A）（○A）、（A?B）是FOLTL公式；
⑤当且仅当有限次地使用①②③④所组成的符号串是FOLTL公式。
计算树逻辑
计算树逻辑（CTL）是一种离散、分支时间、命题时态逻辑。一般讲CTL和CTL*统称为计算树逻辑。
计算树逻辑公式，简称CTL公式，定义如下：
①原子命题（命题变量或变量）是CTL公式；
②如果φ、ψ是CTL公式，那么（φ）、（φ∧ψ）、（φ∨ψ）、（φ→ψ）、（φ↔ψ）是CTL公式；
③如果φ、ψ是CTL公式，那么（A○ψ）、（E○ψ）、（A◇ψ）、（A□ψ）、（E□ψ）、（A（φ?ψ））、（E（φ?ψ））是CTL公式；
④当且仅当有限次使用①②③所组成的符号串是CTL公式。
模型检测
标记算法是模型检验的一个简单算法，其基本原理在于：对于给定的CTL*公式φ，将其列写成A◇，E◇，E○，∧，，nil(假)连接的等值CTL*公式Φ；对Kripke结构中Φ的子公式满足的状态进行标记，直到Φ得到标记；所有标记为Φ的状态就是φ得到满足的状态。
Z语言
Z语言为系统建立基于状态的模型。模型的三个主要组成部分是输入、输出和状态，它们均有相应的数学概念来描述。Z语言形式规约由数学语言描述和自然语言注释两部分组成。其中数学语言描述部分是核心，它是精确、简练地描述系统性质和自动推理的保证。自然注释部分则用于解释说明数学部分的内容。
Z语言表示
1.集合、关系及函数
集合、幂集、元组和笛卡儿积、关系与函数、队列和包
2.自由类型和模式
Petri网
Petri网结构
Petri网结构是一个三元组N=（P，T，F），其中，
①P={p1,p2,...,pn}是有限库所集合；
②T={t1,t2,...,tn}是有限变迁集合（P∪T≠∅，P∩T=∅）；
③F包含于（P×T）∪（T×P）为流关系。
前集和后集
对于一个Petri网结构N=（P,T,F），设x∈（P∪T），令
·x={y|彐y:(y,x)∈F}
x·={y|彐y:(x,y)∈F}
那么称·x为x的前集或输入集，称x·为x的后集或输出集。
顺序关系：若Petri网中存在变迁t1和t2，在某一时刻，t1就绪，而t2未就绪，且t1点火引发t2就绪，即t2的就绪以t1的点火为条件，则t1和t2具有顺序关系。
并发关系：若Petri网中存在变迁t1和t2，在某一时刻，t1，t2同时就绪，它们中任一变迁的点火都不会影响另一个变迁的就绪，则称t1和t2具有并发关系。
冲突关系：若Petri网中存在变迁t1和t2，在某一时刻，t1，t2同时就绪，它们中任一变迁的点火都会导致另一个变迁离开就绪状态，则称t1和t2具有冲突关系。
混惑关系：在某些情况下，一个Petri网中可能同时存在并发和冲突，并且并发变迁的点火会引起冲突的消失或出现。。