FSV4, FSUZ_Lightfoot_06

模式 （Schemas）

Schema：结构化的规格说明

schema 的图表形式：

• schema 名称、声明、谓词

|--- Schema Name ---
|    Declarations
|-------------------
|    Predicate
|___________________

schema 的文字形式：

• SchemaName == [ Declarations | Predicate ]
• == 即“代表”

声明和谓词：

• 每行声明被视为以分号结束，若干行构成一个序列
• 若干行谓词被视为以运算符连接

匿名模式：

• 没有名称

不含谓词部分的模式：

• 只声明新变量，不施加约束谓词

局部变量：

• 模式里声明的变量，在其他模式里引用时需要明确包含定义的模式

全局变量：

• 在规格说明始终可以引用，以公理定义声明