FSV3, FSUZ_Lightfoot_02, FSUZ_Lightfoot_03, FSUZ_Lightfoot_05

以状态为基础的规格说明方法

对系统状态的描述以状态过渡为中心。

系统的操作函数被它们如何改变系统的状态规格化。

步骤：

• 定义变量，描述目标系统的状态及其不变的属性
• 定义初始化操作，设置变量的值为一些合适的初始状态，满足固定需求
• 定义状态上的操作，改变状态但保持不变的属性
• 定义系统信息的查询，不改变系统的状态

Z 中的类型

类型化集合论：

• 一个类型化的集合中的所有成员都被认为有相同之处，即有相同类型
• 类型避免了数学悖论、允许检查
• Z 以类型化的集合论为基础

内置类型整型（Integer）：

• 无需声明
• 写法：ZZ
• • • • div mod
• m .. n（m ≤ n）
  • 3 .. 5 = {3, 4, 5}

标准类型自然数（Natural）：