形式化说明方法形式化说明方法的意义：用自然语言书写的系统规格说明书，可能存在矛盾、二义性、含糊性、不完整性及抽象层次混乱等问题。为了克服非形式化方法的缺点，人们把数学引入软件开发过程，创造了基于数学的形式化方法。常见的形式化方法工具(1)有穷状态机有穷状态机的概念在计算机系统中应用得非常广泛。例如，每个菜单驱动的用户界面都是一个有穷状态机的实现。一个菜单的显示和一个状态相对应，键盘输入或用鼠标选择一个图标是使系统进入其他状态的一个事件。状态的每个转换都具有下面的形式：⇒当前状态〔菜单〕＋事件〔所选择的项〕下个状态。为了对一个系统进行规格说明，通常都需要对有穷状态机做一个很有用的扩展，即在前述的5元组中加入第6个组件——谓词集P，从而把有穷状态机扩展为一个6元组，其中每个谓词都是系统全局状态Y的函数。转换函数T现在是一个从(J－F)×K×P到J的函数。现在的转换规则形式如下：⇒当前状态〔菜单〕＋事件〔所选择的项〕＋谓词下个状态。自动门是一个典型的有穷状态机：它有“开”和“关”两种状态，这就是它的状态集，也就是上面所说的J。人可以从自动门进来或出去，当人进来或出去的时候，自动门会自动打开，如果在规定的时间内没有人进出，自动门会自动关上。人的进来、出去和超时三个事件是自动门的非空输入集，也就是上面所说的K。而自动门在当前状态下，对事件的响应，会引起状态的变化，这就是状态转换函数，也就是上面所说的T。自动门刚安装好的时候，我们可以认为它是关上的，所以关闭状态是自动门的初始状态。在理想情况下，自动门会一直运行，所以它没有终止状态，终止状态集F是空集。有穷状态机的形式定义很精确，文字描述比较通俗，而图形表示则比较直观。通用建模语言(UML)里的状态图是状态机的常用图形表示方法。简单的状态图包括一些状态，用圆角方框表示，里面有状态的名称。状态之间的转换，用箭头表示，上面可以加转换条件。自动门的状态机可以用图3.17表示：(2)Petri网图3.18Petri网的组成一组位置P为{P1，P2，P3，P4}，在图中用圆圈代表位置。一组转换T为{t1，t2}，在图中用短直线表示转换。两个用于转换的输入函数，用由位置指向转换的箭头表示，它们是：I(t1)＝{P2，P4}I(t2)＝{P2}两个用于转换的输出函数，用由转换指向位置的箭头表示，它们是：O(t1)＝{P1}O(t2)＝{P3，P3}注意，输出函数O(t2)中有两个P3，是因为有两个箭头由t2指向P3。更形式化的Petri网结构，是一个四元组C＝(P，T，I，O)。其中，P＝{P1，…，Pn}是一个有穷位置集，n≥0。T＝{t1，…，tm}是一个有穷转换集，m≥0，且T和P不相交。I：T→P为输入函数，是由转换到位置无序单位组的映射。O：T→P为输出函数，是由转换到位置无序单位组的映射。例如，图3.19是红绿灯的petri网。其中P＝{Red，Yellow，Green}，T＝{RtoG，GtoY，YtoR}，I(RtoG)＝{Red}，I(GtoY)＝{Green}，I(YtoR)＝{Yellow}，O(RtoG)＝{Green}，O(GtoY)＝{Yellow}，O(YtoR)＝{Red}(3)Z语言2.状态定义一个Z规格说明由若干个“格(schema)”组成，每个格含有一组变量说明和一系列限定变量取值范围的谓词。例如，格S的格式如图3.20所示图3.21Z格Botton_State在电梯问题中，Button有4个子集，即floor_buttons(楼层按钮的集合)、elevator_buttons(电梯按钮的集合)、buttons(电梯问题中所有按钮的集合)以及pushed(所有被按的按钮的集合，即所有处于打开状态的按钮的集合)。图3.21描述了格Button_State，其中，符号P表示幂集(即给定集的所有子集)。约束条件声明，floor_buttons集与elevator_buttons集不相交，而且它们共同组成buttons集(在下面的讨论中并不需要floor_buttons集和elevator_buttons集，把它们放于图3.21中只是用来说明Z格包含的内容)。3.初始状态抽象的初始状态是指系统第一次开启时的状态。对于电梯问题来说，抽象的初始状态为：Button_Init≙〔Button_State|pushed＝Φ〕上式表示，当系统首次开启时pushed集为空，即所有按钮都处于关闭状态。4.操作如果一个原来处于关闭状态的按钮被按下，则该按钮开启，这个按钮就被添加到pushed集中。图3.22定义了操作Push_Button(按按钮)。Z语言的语法规定，当一个格被用到另一个格中时，要在它的前面加上三角形符号