原文地址：
类型是根据名称区分的。任何整数子区间类型的表达式都是合法的，一个整数表达式也是合法的（虽然这样做可能会导致运行时错误）。布尔类型和整数表达式是不兼容的。
（上边的第二句话原文为：Expressions of any integer subrange type
are legal wherever an integer expression is legal）在变量初始化之前使用变量是错误的，这个错误会在运行时检测。所有的运行时错误都是由验证器检测的。
越界使用数组也是错误的，同样，这个错误也是在运行时检测。
下边对表达式的语法进行说明。
指示符：
::= { . | \[ \] }
通常，"<designator>.<ID>"的形式代表选择记录中的一个域，而"<designator>[<expr>]"的形式代表选择数组中的一个元素。
表达式：
::= \( expr \) | | | \( \) -- a function call. | forall do endforall -- universal quantification. | exists do endexists -- existential quantification. | + | - | * -- multiplication. | / -- integer division. | % -- remainder. | ! -- logical negation. | | -- logical disjunction. | & -- logical conjunction. | -> -- logical implication. | < | <= | > | >= | = | != | ? : -- C-style conditional expression.
其中运算符有：
?: -> | & ! < <= = != >= > + - * / %
上边运算符的优先级是按照从低到高排序的，同一行的运算符具有相同的优先级。
- "+"，"-"，"*"，"/"，"%"，"<"，"<="，">="，">"仅仅为整数运算定义。
- "="和"!="仅仅为简单运算定义。
- "&"，"|"，"!"，和"->"仅仅为布尔运算定义。
- 对于"?:"运算符，测试条件必须是布尔表达式，两个候选者必须是类型兼容的。
- "+"，"-"，"*"，"/"，和"%"返回整数，其他均返回布尔类型，除"?:"之外。
"Forall"和"Exists"运算符：
以后我们会对这两个进行更加详细的介绍。现在对量词表达式（即使用了"forall"或者"exists"的表达式）中使用的<quantifier>进行说明。对于量词表达式，其子表达式必须是一个布尔表达式，它将对quantifier中的每一个值进行测试。"forall"表达式在其quantifier中的每一个值测试均为true的时候为true，"exists"表达式在其quantifier中的某些值测试为true的时候就为true。
表达式这一部分大家还是很熟悉的吧~也比较容易理解~
传送门：
