2.2.3 Sort的可观察性

如果一个软件实体的状态和值可以被直接测试，那么我们就称它是可观察的。不然，它的状态和值不得不用其他方法进行检查，比如通过观察者。可观察性的语法如下：

<Observability> ::=

   is observable by <Op Id>

   | is unobservable

一个可观察实体的操作子必须是一个返回布尔值的二值函数，这个函数必须被定义在sort的signature里面。

2.3 signature的语法和语义

Signature确定软件实体的操作，有三种操作：constants，variables，operations。

<Signature> ::= {[<Constant>]|[<Variable>]|[<Operator>]}*

2.3.1 Constant

    一个constant的关键词是“Const”。

<Constant> ::= Const : <ConstList>;

<ConstList> ::= <Const ID> [, <ConstList>]

<Const ID> ::= <Identifer>

每一个constant identifier定义一个sort的特定constant。

2.3.2 Variable 

一个variable是一个可以改变它state的实体元素，因此被命名为“variable”。它的关键字是“Var”。Variable的sort定义了variable的状态空间，即为，sort。

<Variable> ::= Var <VarList>;

<VarList> ::= <VariableType> [; <VarList>]

<VariableType> ::= <Var IDs> : <Sort Name>

<Var IDs> ::= <Var ID> [, <Var IDs>]

<Var ID> ::= <Identifier> [ <index> ]

如果一个vairable有一个index，那么实际上它通过index values定义了一系列的variables。这个Index可以是一个一定区域内的自然数的连续集，这个集合可以既是一个特定自然数或者意着不确定的“*”，也可以是一个constants的枚举集合以标识符的形式被描述，也可以是上述两者的笛卡尔乘积。

<Index> ::= "[" <Index-set> "]"源]自=751-·论~文"网·www.751com.cn/

<Index set> ::= <Single_Index>[,<Index set>]

<Single_Index> ::=

    | <lower bound> "" <upper bound>

    | <Enumerate set>

<lower bound> ::= <nature number>

<upper bound> ::= <nature number> | "*"

<Enumerate set> ::= <enumerate ID> [, <Enumerate set> ]

<Enumerate ID> ::= <identifier>

2.3.3 Operation

    一个操作子定义一个由实体产生的操作，它在被使用时改变实体的状态，并且可能也会输出产出。一个操作子的输入被以domain的形式给出，而由调用产出的输出则是以co-domain的形式被给出。一个操作子经常访问实体的状态，而且可能改变它。因此，它被呈现给所有的操作子，后者的主main sort被称为上下文 sort。