表达式 Expressions

Dafny 中的表达式与类 Java 语言中的表达式非常相似。以下是一些值得注意的差异。

基本运算符

除了短路布尔运算符 && (and) 和 || （或），Dafny 有一个短路蕴涵运算符 ==> 和一个 if-and-only-if 运算符 <==>。

正如它们的宽度所暗示的那样，<==> 具有比 ==> 低的绑定力，而后者又比 && 和 || 具有更低的绑定力。

Dafny 比较表达式可以是链式的，这意味着“相同方向”的比较可以串在一起。例如，0 <= i < j <= a.Length == N

含义相同： 0 <= i && i < j && j <= a.Length && a.Length == N

请注意，布尔相等可以使用 ==和 <==> 来表示。这些之间有两个区别。首先，== 比 <==> 具有更高的约束力。其次，== 是链接，而 <==> 是关联的。也就是说，a == b == c 与 a == b && b == c 相同，而 a <==> b <==> c 与 a <==> (b <== > c)，这也与 (a <==> b) <==> c 相同。

整数运算

对整数的运算是常用的运算，除了 /（整数除法）和%（整数模）遵循欧几里德定义，这意味着% 总是导致非负数。

因此，当 / 或 % 的第一个参数为负数时，结果与您在 C、Java 或 C# 中得到的结果不同，请参阅 http://en.wikipedia.org/wiki/Modulo_operation。）

离散数学

Dafny 表达式包括全称量词和存在量词，其形式为：forall x :: Expr 和exists x :: Expr，其中x 是绑定变量（可以使用显式类型声明，如x: T 中所示），而Expr 是一个布尔表达式。

集合运算

集合上的操作包括+（并）、*（交）和-（集合差）、集合比较运算符<（真子集）、<=（子集）、它们的对偶> 和>=，以及!! （脱节）。 S 中的表达式 x 表示 x 是集合 S 的成员，而 x !in S 是一个方便的写法 !(x in S)。

要从某些元素创建一个集合，请将它们括在花括号中。例如，{x,y} 是由 x 和 y 组成的集合（如果 x == y，则为单例集），{x} 是包含 x 的单例集，{} 是空集。

序列运算

对序列的操作包括 +（连接）和比较运算符 <（适当的前缀）和 <=（前缀）。成员资格可以像集合一样检查：x in S 和 x !in S。序列 S 的长度表示为 |S|，并且此类序列的元素具有从 0 到小于 |S| 的索引。表达式 S[j] 表示序列 S 的索引 j 处的元素。表达式 S[m..n]，其中 0 <= m <= n <= |S|，返回一个序列，其元素是S 从索引 m 开始（即，从 S[m]、S[m+1]、……直到但不包括 S[n]）。表达式 S[m..]; （通常称为“drop m”）与 S[m..|S|] 相同；也就是说，它返回除 S 的前 m 个元素之外的所有元素的序列。表达式 S[..n] ; （通常称为“take n”）与 S[0..n] 相同，即它返回由 S 的前 n 个元素组成的序列。

如果 j 是序列 S 的有效索引，则表达式 S[j := x];是类似于 S 的序列，只是它在索引 j 处有 x。

最后，要从一些元素组成一个序列，请将它们括在方括号中。例如，[x,y] 是由两个元素 x 和 y 组成的序列，使得[x,y][0] == x 和 [x,y][1] == y，[x] 是唯一元素是 x 的单例序列，[] 是空序列。

if-then-else判断语句

if-then-else 表达式的形式为：if BoolExpr then Expr0 else Expr1

其中 Expr0 和 Expr1 是相同类型的任何表达式。与 if 语句不同，if-then-else 表达式使用 then 关键字，并且必须包含显式的 else 分支。

match匹配表达式

match 表达式类似于 match 语句并具有以下形式：

match Expr { case Empty => Expr0 case Node(l, d, r) => Expr1 }

大括号可用于标记匹配表达式的结束，但最常见的是不需要这样做，然后可以省略大括号。