Dafny type system

# Dafny Type System

Dafny语言参考的这一部分描述了Dafny编程语言中的类型。所描述的是Dafny版本1.9.3.20107中实现的内容，异步任务类型尚未进入主分支。

0. 基本类型 (opens new window) 0.0. 布尔值 (opens new window) 0.1. 数字类型 (opens new window) 0.2. 字符 (opens new window) 1. 类型参数 (opens new window) 2. 集合类型 (opens new window) 2.0. 集合 (opens new window) 2.1. 多集 (opens new window) 2.2. 序列 (opens new window) 2.2.0. 字符串 (opens new window) 2.3. 有限与无限图 (opens new window) 3. 象征类型 (opens new window) 3.0. 同义词类型 (opens new window) 3.1. 不透明类型 (opens new window) 4. 数据类型 (opens new window) 4.0. 归纳数据类型 (opens new window) 4.1. 元组类型 (opens new window) 4.2. 共同归纳类型 (opens new window) 5. 参照类型 (opens new window) 5.0. 类 (opens new window) 5.1. 数组 (opens new window) 5.1.0. 一维数组 (opens new window) 5.1.1. 多维数组 (opens new window) 5.2. 特征 (opens new window) 5.3. 类型 object (opens new window) 5.4. 迭代器类型 (opens new window) 5.5. 异步任务类型 (opens new window) 6. 函数类型 (opens new window) 6.0. Lambda表达式 (opens new window) 7. 新类型 (opens new window) 7.0. 数字转化操作 (opens new window) 8. 子集类型 (opens new window)

# 0. 基本类型

Dafny提供了三种基本类型，bool表示布尔，int表示整数，real表示实数。

# 0.0. Booleans

有两个布尔值，每个值在语言中都有一个对应的文本：false和true。

除了在所有类型上定义的相等（=）和disequality（！=），类型bool还支持以下操作：


操作符	描述

`<==>`	当且仅当

`==>`	蕴含
`<==`	反向蕴含

`&&`	连接(且)
`\|\|`	析取(或)

`!`	否定(非)

否定是一元的；其他的是二进制的。该表显示了一组结合力不断增强的运算符，等式结合比合取和析取强，比否定弱。在每个组中，不同的运算符不关联，因此需要使用括号。例如,

A && B || C    // error

将是不明确的，而必须写为

(A && B) || C

或

A && (B || C)

取决于预期的意思。

表达式A<=>B和A==B给出了相同的值，但请注意，<=>是关联的，=是链接的。所以

A <==> B <==> C

与下式相同

A <==> (B <==> C)

和

(A <==> B) <==> C

鉴于

A == B == C

只是下式的速记

A == B && B == C

合取是关联的，析取也是。这些运算符是短路（从左到右），这意味着只有在第一个操作数的计算不确定表达式的值时，才会计算它们的第二个参数。从逻辑上讲，表达式A&&B是在定义了A并且A的计算结果为false或B时定义的。定义A&&B时，其含义与普通的对称数学连词相同∧. | | |和∨.

含义是“右关联”，从左到右短路。反向蕴涵B<==A与A==>B完全相同，但可以按相反的顺序写入操作数。因此，反向含义是“左关联”，是从“右”到“左”的短路。为了说明关联性规则，以下四行中的每一行都表示了相同的属性，即bool类型的任何A、B和C：

A ==> B ==> C
A ==> (B ==> C)  // parentheses redundant, since ==> is right associative
C <== B <== A
(C <== B) <== A  // parentheses redundant, since <== is left associative

1
2
3
4

为了说明短路规则，请注意，表达式a.Length仅在a不为null时才为数组a定义 (见小节 5 (opens new window)), 这意味着以下两个表达式格式正确：

a != null ==> 0 <= a.Length
0 <= a.Length <== a != null

1
2

这两种表达的反作用是：

a.Length < 0 ==> a == null  // not well-formed
a == null <== a.Length < 0  // not well-formed

1
2

但这些表达式的格式不好，因为格式好要求左（和右）操作数a.Length<0本身格式良好。

蕴涵A==>B相当于析取！A | | B，但有时（尤其是在规范中）更清晰易读。由于||是从左向右短路，请注意

a == null || 0 <= a.Length

结构良好，而

0 <= a.Length || a == null  // not well-formed

结构较差。

此外，布尔语支持逻辑量词（forall和exists），在Dafny语言参考的另一部分中有描述。

# 0.1. 数字类型

Dafny 支持两种 numeric 类型，integer-based，包括所有整数的基本类型 int，和 real-based，包括所有实数的基本类型 real。用户定义的基于 int 和 real 的数字类型，称为 newtypes，在第 [7] 节(http://leino.science/papers/krml243.html#sec-newtypes) 中有描述。此外，代表 int 的非负子范围的 subset type nat 在第 [8] 节（http://leino.science/papers/krml243.html#sec-subset-types）中进行了描述 . 该语言包含每个非负整数的文字，例如“0”、“13”和“1985”。整数也可以使用前缀“0x”以十六进制书写，如“0x0”、“0xD”和“0x7c1”（始终使用小写“x”，但十六进制数字本身不区分大小写）。允许使用前导零。要形成负整数，请使用一元减号运算符。一些非负实数也有文字。这些被写成一个小数点，两边都有一个非空的十进制数字序列。例如，“1.0”、“1609.344”和“0.5772156649”。对于整数（十进制和十六进制形式）和实数，文字中的任何两位数字都可以用下划线分隔，以提高文字的可读性。例如：

1_000_000        // easier to read than 1000000
0_12_345_6789    // strange but legal formatting of 123456789
0x8000_0000      // same as 0x80000000 -- hex digits are often placed in groups of 4
0.000_000_000_1  // same as 0.0000000001 -- 1 Ångström

1
2
3
4

除了相等和不相等之外，数值类型还支持以下关系运算：


operator	description

<	less than
`<=`	at most
`>=`	at least
`>`	greater than

就像相等和不相等一样，这些运算符是链接的，只要它们链接在“相同的方向”。那就是说，

A <= B < C == D <= E

is simply a shorthand for

A <= B && B < C && C == D && D <= E

而

A < B > C

不被允许。每种数字类型也有运算符：


操作符	描述

`+`	加
`-`	减

`*`	乘
`/`	除
`%`	取模

`-`	否定 (一元减)

二元运算符是左结合的，它们在两组中相互关联。这些组按绑定能力增加的顺序列出，等式绑定比乘法运算符更强，比一元运算符弱。仅基于整数的数值类型支持模数。整数除法和模数是欧几里得除法和模数。这意味着无论两个操作数的符号如何，模数始终返回非负数。更准确地说，对于任何整数a和非零整数b，

a == a / b * b + a % b
0 <= a % b < B

1
2

其中“B”表示“b”的绝对值。基于实数的数值类型有一个成员 Trunc，它返回实数值的 floor，即不超过实数值的最大整数。例如，对于任何类型为“real”的“r”和“r”，以下属性成立：

3.14.Trunc == 3
(-2.5).Trunc == -3
-2.5.Trunc == -2
real(r.Trunc) <= r
r <= r' ==> r.Trunc <= r'.Trunc

1
2
3
4
5

请注意，在第三行中，成员访问（如 .Trunc）的绑定比一元减号更强。第四行使用从 int 到 real 的转换函数 real，如第 [7.0] 节 (http://leino.science/papers/krml243.html#sec-numeric-conversions) 中所述

# 0.2. 字符

Dafny 支持 characters 的 char 类型。字符文字用单引号括起来，如 'D'。要将单引号写成字符文字，必须使用转义序列。转义序列也可用于写入其他字符。支持的转义序列如下：


转义字符	含义

`\'`	字符 `'`
`\"`	字符 "
`\\`	字符 `\`
`\0`	空字符，同 `\u0000`
`\n`	换行
`\r`	回车
`\t`	水平制表
`\uxxxx`	十六进制编码通用字符 `xxxx`

双引号的转义序列是多余的，因为 '"' 和 '"' 表示相同的字符——提供这两种形式是为了支持与字符串文字相同的转义序列（第 [2.2.0] 节（http: //leino.science/papers/krml243.html#sec-string))。在 \u*xxxx* 形式中，u 总是小写，但四个十六进制数字不区分大小写。字符值是有序的，可以使用标准关系运算符进行比较：


操作符	描述

`<`	少于
`<=`	至多
`>=`	至少
`>`	大于

字符序列表示字符串，如第 2.2.0 节所述。(http://leino.science/papers/krml243.html#sec-string).

# 1. 类型参数

Dafny 中的许多类型（以及函数和方法）都可以通过类型进行参数化。这些类型参数通常在尖括号内声明，可以代表任何类型。有时需要限制这些类型参数，以便它们只能由某些类型的系列实例化。因此，Dafny 不仅在幽灵上下文中而且在编译上下文中区分支持相等操作的类型。为了表明一个类型参数被限制为这种支持平等的类型，类型参数的名称采用后缀“(==)”。[0](http://leino.science/papers/krml243. html#fn-fn-type-mode) 例如，

method Compare〈T(==)〉(a: T, b: T) returns (eq: bool)
{
  if a == b { eq := true; } else { eq := false; }
}

1
2
3
4

是一种方法，其类型参数仅限于支持相等的类型。同样，请注意 all 类型在 ghost 上下文中支持相等；区别仅适用于非幽灵（即编译）代码。共归纳数据类型、函数类型以及带有幻像参数的归纳数据类型是不支持等式的类型的示例。 Dafny 有一些推理支持，可以使某些签名不那么混乱（在 Dafny 语言参考的不同部分中进行了描述）。在某些情况下，这种支持会推断出必须将类型参数限制为支持相等的类型，在这种情况下，Dafny 会自动添加“(==)”。

# 2. 集合类型

Dafny 提供了几种内置的集合类型。

# 2.0. 集合

对于任何类型 T，set〈T〉 类型的每个值都是 T 值的有限集合。集合成员资格由类型 T 中的相等性确定，因此只有当T 支持相等性时，set〈T〉 才能在非幽灵上下文中使用。可以使用 set display 表达式形成一个集合，该表达式可能是一个空的、无序的、不区分重复的表达式列表，用花括号括起来。为了显示，

{}        {2, 7, 5, 3}        {4+2, 1+5, a*b}

是设置显示的三个示例。还有一个 set comprehension 表达式（带有活页夹，就像在逻辑量化中一样），在 Dafny 语言参考的不同部分进行了描述。除了相等和不相等之外，集合类型还支持以下关系运算：


操作符	描述

`<`	真子集
`<=`	子集
`>=`	超集
`>`	真超集

与算术关系运算符一样，这些运算符是链接的。集合支持以下二元运算符，按绑定能力递增的顺序列出：


操作符	描述

`!!`	不相交

`+`	设置联合
`-`	设置差异

`*`	设置交点

+、- 和 * 的结合性规则类似于同名算术运算符的结合性规则。表达式A !! B，它的约束力与相等性相同（但它既不与相等性联系也不连锁），说集合A和B没有共同的元素，也就是说，它等价于

A * B == {}

但是，不相交运算符是链式的，所以 A !! B !! C !! D表示：

A * B == {} && (A + B) * C == {} && (A + B + C) * D == {}

此外，对于任何set〈T〉类型的集合s和任何T类型的表达式e，集合支持以下操作：


表达式	描述

\|s\|	集合基数
`e in s`	集合成员
`e !in s`	集合非成员

表达式 e !in s 是 !(e in s) 的语法简写。

# 2.1. Multisets

multiset 类似于集合，但跟踪每个元素的多重性，而不仅仅是它的存在或不存在。对于任何类型 T，multiset〈T〉 类型的每个值都是从 T 值到表示每个元素的多重性的自然数的映射。 Dafny 中的多重集是有限的，也就是说，它们包含有限数量的每个有限元素。换句话说，多重集仅将有限数量的元素映射到非零（有限）多重性。与集合一样，多集成员资格由类型“T”中的相等性确定，因此只有当“T”支持相等时，“多集〈T〉”才能在非幽灵上下文中使用。可以使用 multiset display 表达式来形成多重集，该表达式可能是一个空的、无序列的表达式列表，包含在关键字 multiset 后面的花括号中。为了显示，

multiset{}    multiset{0, 1, 1, 2, 3, 5}    multiset{4+2, 1+5, a*b}

是多组显示的三个示例。没有多集理解表达式。除了相等和不相等之外，多重集类型还支持以下关系运算：


操作符	描述

<	真多集子集
`<=`	多集子集
`>=`	多集超集
`>`	真多集超集

与算术关系运算符一样，这些运算符是链接的。多重集支持以下二元运算符，按绑定能力递增的顺序列出：


操作符	描述

`!!`	多集不相交

`+`	多集联合
`-`	多集差异

`*`	多集交集

+、- 和 * 的结合性规则类似于同名算术运算符的结合性规则。表达式'A !! B表示多重集A和B` 没有共同的元素，也就是说，它等价于

A * B == multiset{}

与类似的集合运算符一样，!! 是链式的。此外，对于任何类型为multiset〈T〉的多重集s、类型为T的表达式e和基于非负整数的数字n，多重集支持以下操作：


表达式	描述

\|s\|	多集基数
`e in s`	多集成员
`e !in s`	多集非成员
`s[e]`	`e` 在 `s` 中的多样性
`s[e := n]`	多集更新 (多样性变化)

当且仅当 s[e] != 0 时，表达式 e in s 才会返回 true。表达式 e !in s 是 !(e in s) 的语法简写。表达式 s[e := n] 表示类似于 s 的多重集，但元素 e 的多重性是 n。请注意，多重集更新 s[e := 0] 会产生类似 s 的多重集，但不会出现任何 e（无论 s 首先是否出现过e）。作为另一个示例，请注意 s - multiset{e} 等价于：

if e in s then s[e := s[e] - 1] else s

# 2.2. 序列

对于任何类型“T”，“seq〈T〉”类型的值表示“T”元素的序列，即从连续自然数的有限集合（称为indicies）到“T”的映射 `价值观。（将其视为一个映射，因此序列是多重集的对偶。）可以使用 sequence display 表达式形成序列，该表达式可能是一个包含在方括号中的空的、有序的表达式列表。为了阐释，

[]        [3, 1, 4, 1, 5, 9, 3]        [4+2, 1+5, a*b]

是顺序显示的三个示例。没有序列理解表达式。除了相等和不相等之外，序列类型还支持以下关系运算：


操作符	描述

<	真前缀
`<=`	前缀

与算术关系运算符一样，这些运算符是链接的。注意没有>和>=。序列支持以下二元运算符：


操作符	描述

`+`	连接

运算符 + 是关联的，就像同名的算术运算符一样。此外，对于任何类型为“seq〈T〉”的序列“s”，类型为“T”的表达式“e”，基于整数的数字“i”满足“0 <= i < |s|”，以及整数- 基于数字 lo 和 hi 满足 0 <= lo <= hi <= |s|，序列支持以下操作：


表达式	描述

\|s\|	序列长度
`s[i]`	序列选择
`s[i := e]`	序列更新
`e in s`	序列成员
`e !in s`	序列非成员
`s[lo..hi]`	子序列
`s[lo..]`	drop
`s[..hi]`	take
`s[slices]`	切片
`multiset(s)`	序列转换为 `multiset〈T〉`

表达式 s[i := e] 返回一个类似 s 的序列，除了索引 i 处的元素是 e。表达式 e in s 表示存在一个索引 i 使得 s[i] == e。仅当元素类型“T”支持相等时，才允许在非幽灵上下文中使用。表达式 e !in s 是 !(e in s) 的语法简写。

表达式 s[lo..hi] 产生一个序列，该序列通过获取第一个 hi 元素然后删除第一个 lo 元素而形成。因此，结果序列的长度为“hi - lo”。请注意，s[0..|s|] 等于 s。如果省略上限，则默认为 |s|，因此 s[lo..] 会生成通过删除 s 的第一个 lo 元素形成的序列。如果省略下限，则默认为 0，因此 s[..hi] 产生由 s 的第一个 hi 元素形成的序列。

在序列切片操作中，slices 是一个长度指示符的非空列表，由冒号分隔并可选地终止，并且至少有一个冒号。每个长度指示符都是一个基于非负整数的数字，其总和不大于|s|。如果有 k 个冒号，则该操作会从 s 生成 k 个连续子序列，每个长度由相应的长度指示符指示，并将这些作为序列序列返回。1 (opens new window) 如果 slices 以冒号结尾，那么最后一个切片的长度会一直延伸到 s 的末尾，即它的长度是|s|减去给定长度指示符的总和。例如，对于任何长度至少为 10 的序列 s ，以下等式成立：

var t := [3.14, 2.7, 1.41, 1985.44, 100.0, 37.2][1:0:3];
assert |t| == 3 && t[0] == [3.14] && t[1] == [];
assert t[2] == [2.7, 1.41, 1985.44];
var u := [true, false, false, true][1:1:];
assert |u| == 3 && u[0][0] && !u[1][0] && u[2] == [false, true];
assert s[10:][0] == s[..10];
assert s[10:][1] == s[10..];

1
2
3
4
5
6
7

操作multiset(s)产生序列s的元素的多重集。仅当元素类型“T”支持相等时，才允许在非幽灵上下文中使用。

# 2.2.0. 字符串

序列类型的一个特例是seq〈char〉，Dafny 提供了一个同义词：string。字符串与其他序列类似，但为序列显示表达式提供了额外的语法，即字符串文字。字符串文字有两种语法形式：标准形式和逐字形式。

标准形式的字符串文字用双引号括起来，如 "Dafny"。要在这样的字符串文字中包含双引号，必须使用转义序列。转义序列也可用于包含其他字符。支持的转义序列与字符文字相同，请参阅第 [0.2] 节(http://leino.science/papers/krml243.html#sec-char)。例如，Dafny 表达式 "say \"yes\"" 表示字符串 say "yes"。单引号的转义序列是多余的，因为 "'" 和 "'" 表示相同的字符串——提供这两种形式是为了支持与字符文字相同的转义序列。

逐字形式的字符串文字用 @" 和 " 括起来，如 @"Dafny"。要在这样的字符串文字中包含双引号，必须使用转义序列“”，即两次写入字符。在逐字形式中，没有其他转义序列。甚至像换行符这样的字符也可以写在字符串文字中（因此在程序文本中跨越多行）。例如，以下三个表达式表示相同的字符串：

"C:\\tmp.txt"
@"C:\tmp.txt"
['C', ':', '\\', 't', 'm', 'p', '.', 't', 'x', 't']

1
2
3

由于字符串是序列，因此在它们上定义了关系运算符 < 和 <=。但是请注意，这些运算符仍然分别表示正确的前缀和前缀，而不是可能需要的某种字母比较，例如，在对字符串进行排序时。

# 2.3. 有限与无限图

对于任何类型T和U，map〈T，U〉类型的值表示从T到U的*（有限）映射*。换句话说，它是一个由T索引的查找表。地图的 domain 是一组有限的 T 值，它们具有关联的 U 值。由于域中的键是使用 T 类型中的相等性进行比较的，因此只有当T 支持相等性时，类型map〈T,U〉 才能在非幽灵上下文中使用。

类似地，对于任何类型 T 和 U，imap⟨T,U⟩ 类型的值表示*（可能）无限映射*。在大多数情况下，imap<T,U> 类似于 map<T,U>，但是 imap<T,U> 类型的映射允许有一个无限域。

可以使用 map display 表达式形成地图，该表达式可能是一个空的、有序的 maplets 列表，每个 maplet 具有 t := u 的形式，其中 t 是 T 类型的表达式，并且 u 是U 类型的表达式，放在关键字map 后面的方括号中。为了显示，

map[]    map[20 := true, 3 := false, 20 := false]    map[a+b := c+d]

是地图显示的三个示例。通过使用关键字 imap 而不是 map，生成的地图将是 imap<T,U> 类型而不是 map<T,U>。请注意，允许无限映射 (imap) 具有有限域，而不允许有限映射 (map) 具有无限域。如果同一个键出现多次，则结果映射中只出现最后一次出现。2 (opens new window) 还有一个 * 地图理解表达式*，在 Dafny 语言参考的不同部分进行了解释。

对于map<T,U>类型的任何映射fm，map<T,U>或imap<T,U>类型的任何映射m，类型的任何表达式t T，U类型的任何表达式u，以及m域中的任何d（即满足d in m`），映射支持以下操作：


表达式	描述

\|fm\|	地图基数
`m[d]`	地图选择
`m[t := u]`	地图更新
`t in m`	映射域成员
`t !in m`	映射域非成员

|fm| 表示fm 中的映射个数，即fm 的域的基数。请注意，无限映射不支持基数运算符。表达式 m[d] 返回 m 与 d 关联的 U 值。表达式 m[t := u] 是一个类似于 m 的映射，除了键 t 处的元素是 u。

表达式 t in m 表示 t 在 m 的域中，而 t !in m 是 !(t in m) 的语法简写。 3 (opens new window) 这是一个小例子，其中类型为 map<int,real> 的地图 cache 用于缓存 Joule-Thomson 系数的计算值给定温度下的一些固定气体：

if K in cache {  // check if temperature is in domain of cache
  coeff := cache[K];  // read result in cache
} else {
  coeff := ComputeJouleThomsonCoefficient(K);  // do expensive computation
  cache := cache[K := coeff];  // update the cache
}

1
2
3
4
5
6

# 3. 象征类型

有时通过多个名称了解一个类型或抽象地处理一个类型很有用。

# 3.0. 同义词类型

类型同义词声明：

type Y〈T〉 = G

声明 Y〈T〉 是类型 G 的同义词。这里，T 是一个类型参数的非空列表（每个参数都可选地用后缀“(==)”指定），它可以用作G 中的自由类型变量。如果同义词没有类型参数，则删除“〈T〉”。在所有情况下，类型同义词只是同义词。也就是说，除了可能产生的错误消息之外，Y〈T〉 和 G 之间从来没有区别。

例如，以下类型同义词的名称可能会提高程序的可读性：

type Replacements〈T〉 = map〈T,T〉
type Vertex = int

1
2

如第 2.2.0 (opens new window) 中所述，string 是seq〈char〉 的内置类型同义词，好像它将被宣布如下：

type string = seq〈char〉

# 3.1. 不透明类型

类型同义词的一个特例是未指定的。这样的类型简单地通过以下方式声明：

type Y〈T〉

它被称为不透明类型。它的定义可以在精炼模块中显示。为了表明 Y 表示支持相等的类型，可以在名称“Y”之后紧跟“(==)”。

例如，声明

type T
function F(t: T): T

1
2

可用于在某个任意类型“T”上建模未解释的函数“F”。作为另一个例子，

type Monad〈T〉

可以抽象地用于表示任意参数化的 monad。

# 4. 数据类型

Dafny 提供了两种代数数据类型，一种是归纳定义的，另一种是协归纳定义的。每个数据类型的显着属性是该类型的每个值唯一标识数据类型的构造函数之一，并且每个构造函数的参数都是单射的。

# 4.0. 归纳类型

归纳数据类型的值可以看作是有限树，其中叶子是基本类型、数值类型、引用类型、共归纳数据类型或函数类型的值。实际上，可以使用 Dafny 有根据的 < 排序来比较归纳数据类型的值。

归纳数据类型声明如下：

datatype D〈T〉 = Ctors

其中 *Ctors* 是一个非空的 | 分隔的 (datatype) 构造函数 的数据类型列表。每个构造函数都有以下形式：

C(params)

其中 *params* 是一个逗号分隔的类型列表，前面可选参数名称和冒号，前面可选关键字 ghost。如果构造函数没有参数，则可以省略构造函数名称后面的括号。如果没有构造函数接受参数，则该类型通常称为枚举；例如：

datatype Friends = Agnes | Agatha | Jermaine | Jack

对于每个构造函数 C，Dafny 定义了一个 discriminator C?，它是一个返回 true 的成员，当且仅当数据类型值是使用 C 构造的。对于构造函数 C 的每个命名参数 p，Dafny 定义了一个 destructor p，它是从用于构造数据类型值的 C 调用返回 p 参数的成员；它的使用要求 C? 成立。例如，对于标准的 List 类型

datatype List〈T〉 = Nil | Cons(head: T, tail: List〈T〉)

以下成立：

Cons(5, Nil).Cons? && Cons(5, Nil).head == 5

注意表达式

Cons(5, Nil).tail.head

格式不正确，因为 Cons(5, Nil).tail 不满足 Cons?。

析构函数的名称在数据类型的所有构造函数中必须是唯一的。构造函数可以与封闭数据类型同名；这对于通常称为记录类型的单构造函数数据类型特别有用。例如，黑白像素的记录类型可能表示如下：

datatype Pixel = Pixel(x: int, y: int, on: bool)

要调用构造函数，通常只需要提及构造函数的名称，但如果这不明确，则始终可以通过数据类型的名称来限定构造函数的名称。比如上面的Cons(5, Nil)可以写成

List.Cons(5, List.Nil)

作为显式调用数据类型构造函数的替代方法，可以使用 datatype update 表达式将数据类型值构造为一个参数从给定数据类型值的变化。对于任何类型为数据类型的“d”，该数据类型包括构造函数“C”，该构造函数具有名为“f”的类型为“T”的参数（析构函数），以及任何类型为“T”的表达式“t”，

d[f := t]

构造一个类似于 d 但其 f 参数是 t 的值。该操作要求 d 满足 C?。例如，以下等式成立：

Cons(4, Nil)[tail := Cons(3, Nil)] == Cons(4, Cons(3, Nil))

# 4.1. 元组类型

Dafny 构建了对应于元组的记录类型，并为它们提供了一种方便的特殊语法，即括号。例如，可能已声明为：

datatype Pair〈T,U〉 = Pair(0: T, 1: U)

Dafny 提供了类型 (T, U) 和构造函数 (t, u)，好像数据类型的名称是“”，并且它的类型参数在圆括号中给出，并且好像构造函数名称是“” . 请注意，析构函数名称是“0”和“1”，它们是成员的合法标识符名称。例如，显示元组析构函数的使用，这里有一个包含 2 元组的属性（即 pairs）：

(5, true).1 == true

Dafny 声明 n 元组，其中 n 为 0 或 2 或更高。没有 1 元组，因为围绕单个类型或单个值的括号没有语义意义。 0 元组类型 () 通常被称为 unit 类型，它的单个值，也写作 ()，被称为 unit。

# 4.2. 共同归纳类型

尽管 Dafny 坚持认为有一种方法可以从头开始构造每个归纳数据类型值，但 Dafny 还支持 co-inductive datatypes，其构造函数被延迟评估，因此允许无限结构。使用关键字“codatatype”声明共归纳数据类型；除此之外，它像归纳数据类型一样被声明和使用。

例如,

codatatype IList〈T〉 = Nil | Cons(head: T, tail: IList〈T〉)
codatatype Stream〈T〉 = More(head: T, tail: Stream〈T〉)
codatatype Tree〈T〉 = Node(left: Tree〈T〉, value: T, right: Tree〈T〉)

1
2
3

分别声明可能无限的列表（即可以是有限或无限的列表）、无限流（即始终无限的列表）和无限二叉树（即每个分支永远存在的树）。

# 5. 参照类型

Dafny 提供了许多参考类型。这些代表对程序堆中动态分配的对象的引用。要访问对象的成员，对对象的引用（即指针或对象标识）被取消引用。

特殊值 null 是每个引用类型的一部分。4 (opens new window)

# 5.0. 类

class C 是一个引用类型，声明如下：

class C〈T〉 extends J
{
  members
}

1
2
3
4

其中类型参数列表T是可选的，“extends J”也是如此，它表示该类扩展了一个特征“J”。类的成员是 fields、functions 和 methods。这些是通过取消引用对“C”实例的引用来访问或调用的。除非函数或方法声明为 static，否则函数或方法会在 C 的 instance 上调用。机械地，这只是意味着该方法采用隐式 receiver 参数，即用于访问成员的实例。在实例函数或方法的规范和主体中，接收器参数可以通过关键字 this 显式引用。但是，在这样的地方，this的成员也可以无条件地被提及。为了说明，合格的 this.f 和不合格的 f 在以下示例中指的是同一对象的同一字段：

class C {
  var f: int;
  method Example() returns (b: bool)
  {
    b := f == this.f;
  }
}

1
2
3
4
5
6
7

所以方法体总是将 true 分配给输出参数 b。对同一接收者和成员的合格和不合格访问之间没有语义差异。

一个 C 实例是使用 new 创建的，例如：

c := new C;

请注意，new 只是分配一个 C 对象并返回对它的引用；其字段的初始值是它们各自类型的任意值。因此，通常在创建后立即调用称为 initialization method 的方法，例如：

c := new C;
c.InitFromList(xs, 3);

1
2

当初始化方法没有out-parameter并且修改不超过this时，那么上面的两个语句可以合并为一个：

c := new C.InitFromList(xs, 3);

请注意，一个类可以包含多个初始化方法，这些方法可以随时调用，而不仅仅是作为new的一部分，并且new不需要在创建时调用初始化方法。

要编写结构化的面向对象程序，通常依赖于仅以特定方式构造对象。为此，Dafny 提供了 constructor (method)s，这是一种受限形式的初始化方法。构造函数是用关键字constructor而不是method声明的。当一个类包含构造函数时，对该类的每次调用 new 都必须伴随对构造函数之一的调用。此外，不能在其他时间调用构造函数，只能在对象创建期间调用。除了这些限制之外，使用普通初始化方法和使用构造函数之间没有语义上的区别。

Dafny 设计允许命名构造函数，这促进了使用上面的“InitFromList”之类的名称。尽管如此，许多类只有一个构造函数或有一个典型的构造函数。因此，Dafny 允许一个匿名构造函数，即名称本质上是“”的构造函数。例如：

class Item {
  constructor (x: int, y: int)
  // ...
}

1
2
3
4

调用此构造函数时，会删除“.”，如下所示：

m := new Item(45, 29);

请注意，匿名构造函数只是命名构造函数的一种方式；也可以有其他构造函数。

# 5.1. 数组

Dafny 支持任何正维度的可变固定长度数组类型。数组类型是引用类型。

# 5.1.0. 一维数组

n T 元素的一维数组创建如下：

a := new T[n];

数组元素的初始值是“T”类型的任意值。使用不可变的 Length 成员检索数组的长度。例如上面分配的数组满足：

a.Length == n

对于 0 <= i < a.Length 范围内的任何基于整数的数字 i，array selection 表达式 a[i] 检索元素 i（即，前面有 i 数组中的元素）。可以使用数组更新语句将存储在 i 的元素更改为值 t：

a[i] := t;

警告：由new T[n]创建的数组类型是array〈T〉。一个容易犯的错误是在 new 后面写 array<T> 而不是 T。例如，考虑以下情况：

var a := new array〈T〉;
var b := new array〈T〉[n];
var c := new array〈T〉(n);  // resolution error
var d := new array(n);  // resolution error

1
2
3
4

第一条语句分配了一个类型为 array〈T〉的数组，但长度未知。第二个分配一个长度为“n”的“array〈array〈T〉〉”类型的数组，即一个包含“n”类型的“array〈T〉”值的数组。第三条语句分配一个类型为array〈T〉的数组，然后尝试调用这个数组的匿名构造函数，传递参数n。由于array没有构造函数，更不用说匿名构造函数了，这个语句会产生错误。如果对于需要类型参数的类型省略了类型参数列表，Dafny 将尝试填写这些，因此只要可以推断出array类型参数，就可以省略“〈T〉 ” 在上面的第四个语句中。但是，与第三条语句一样，array` 没有匿名构造函数，因此会生成错误消息。

一维数组支持将一系列连续元素转换为序列的操作。对于任何类型为array〈T〉的数组a，基于整数的数字lo和hi满足0 <= lo <= hi <= a.Length，以下操作各自产生一个seq 〈T〉：


表达式	描述

`a[lo..hi]`	子数组转为序列
`a[lo..]`	drop
`a[..hi]`	take
`a[..]`	数组转换为序列

表达式 a[lo..hi] 获取数组的第一个 hi 元素，然后删除其中的第一个 lo 元素并返回剩余的序列。因此，结果序列的长度为“hi - lo”。其他操作是第一个操作的特殊实例。如果省略 lo，则默认为 0，如果省略 hi，则默认为 a.Length。在最后一个操作中，lo 和 hi 都被省略了，因此 a[..] 返回由 a 的所有数组元素组成的序列。

子数组操作在规范中特别有用。例如，使用变量“lo”和“hi”来划分仍然可以找到搜索“key”的子数组的二分搜索算法的循环不变量可以表示如下：

key !in a[..lo] && key !in a[hi..]

另一个用途是说某个范围的数组元素自方法开始以来没有改变：

a[lo..hi] == old(a[lo..hi])

或从循环开始：

ghost var prevElements := a[..];
while // ...
  invariant a[lo..hi] == prevElements[lo..hi];
{
  // ...
}

1
2
3
4
5
6

注意这个例子中的prevElements的类型是seq<T>，如果a的类型是array<T>。

子数组操作的最后一个示例在于表示数组的元素是方法开头的数组元素的排列，就像在大多数排序算法中所做的那样。在这里，子数组操作与序列到多集的转换相结合：

multiset(a[..]) == multiset(old(a[..]))

# 5.1.1. 多维数组

2 维或更多维的数组大多类似于一维数组，不同之处在于 new 需要更多长度参数（每个维度一个），并且数组选择表达式和数组更新语句需要更多索引。例如：

matrix := new T[m, n];
matrix[i, j], matrix[x, y] := matrix[x, y], matrix[i, j];

1
2

创建一个二维数组，其维度的长度分别为“m”和“n”，然后交换“i,j”和“x,y”处的元素。 matrix 的类型是 array2<T>，对于高维数组（array3<T>、array4<T> 等）也是如此。但是请注意，没有类型 array0<T>，本来可以是 array1<T> 的东西实际上只是命名为 array<T>。

上面的 new 操作要求 m 和 n 是基于非负整数的数字。可以使用不可变字段 Length0 和 Length1 检索这些长度。例如，以下保存了上面创建的数组：

matrix.Length0 == m && matrix.Length1 == n

高维数组类似（Length0、Length1、Length2、...）。数组选择表达式和数组更新语句要求索引在范围内。例如，上面的交换语句只有在以下情况下才是格式正确的：

0 <= i < matrix.Length0 && 0 <= j < matrix.Length1 &&
0 <= x < matrix.Length0 && 0 <= y < matrix.Length1

1
2

与一维数组相比，没有将元素的延伸从多维数组转换为序列的操作。

# 5.2. 特征

trait 是一个“抽象超类”，或者称它为“接口”或“mixin”。特征对 Dafny 来说是新的，并且可能会发展一段时间。一个 trait 的声明很像一个类的声明：

trait J
{
  members
}

1
2
3
4

其中 *members* 可以包含字段、函数和方法，但不能包含构造函数方法。允许将函数和方法声明为“静态”。

扩展特征“J”的引用类型“C”可以分配给“J”，但不能反过来。 J 的成员可以作为C 的成员使用。 J 中的成员不允许在C 中重新声明，除非该成员是在J 中没有主体的非static 函数或方法。通过这样做，类型“C”可以为成员提供更强大的规范和主体。

new 不允许与特征一起使用。因此，没有分配类型是特征的对象。但是当然可以有一个类 C 的对象实现了一个特征 J ，并且对这样一个 C 对象的引用可以用作类型 J 的值。

例如，以下特征表示可移动的几何形状：

trait Shape
{
  function method Width(): real
    reads this
  method Move(dx: real, dy: real)
    modifies this
  method MoveH(dx: real)
    modifies this
  {
    Move(dx, 0.0);
  }
}

1
2
3
4
5
6
7
8
9
10
11
12

成员 Width 和 Move 是 abstract （即无主体），并且可以由扩展 trait 的不同类以不同方式实现。方法 MoveH 的实现在 trait 中给出，因此被所有扩展 Shape 的类使用。这里有两个类，每个类都扩展了“Shape”：

class UnitSquare extends Shape
{
  var x: real, y: real;
  function method Width(): real {  // note the empty reads clause
    1.0
  }
  method Move(dx: real, dy: real)
    modifies this
  {
    x, y := x + dx, y + dy;
  }
}
class LowerRightTriangle extends Shape
{
  var xNW: real, yNW: real, xSE: real, ySE: real;
  function method Width(): real
    reads this
  {
    xSE - xNW
  }
  method Move(dx: real, dy: real)
    modifies this
  {
    xNW, yNW, xSE, ySE := xNW + dx, yNW + dy, xSE + dx, ySE + dy;
  }
}

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

请注意，类可以声明其他成员，它们为特征的抽象成员提供实现，它们重复成员签名，并且它们负责提供自己的成员规范，这些规范既加强了特征中的相应规范，又是对提供的机构感到满意。最后，这是一些创建两个类实例并将它们一起用作形状的代码:

var myShapes: seq〈Shape〉;
var A := new UnitSquare;
myShapes := [A];
var tri := new LowerRightTriangle;
myShapes := myShapes + [tri];  // myShapes contains two Shape values, of different classes
myShapes[1].MoveH(myShapes[0].Width());  // move shape 1 to the right by the width of shape 0

1
2
3
4
5
6

# 5.3. 类型 `object`

有一个内置的引用类型object，它就像所有引用类型的超类型。5 (opens new window) type object 是为了启用对动态帧的统一处理。特别是，保留类型为 set〈object〉的幽灵字段（通常命名为Repr` 表示“表示”）很有用。

# 5.4. 迭代器类型

iterator 为编写迭代返回元素的代码提供了编程抽象。这些 CLU 风格的迭代器是协同例程，因为它们跟踪自己的程序计数器，并且控制可以传入和传出迭代器主体。

迭代器声明如下：

iterator Iter〈T〉(in-params) yields (yield-params)
  specification
{
  body
}

1
2
3
4
5

其中 T 是类型参数的列表（通常，如果没有类型参数，则省略“〈T〉”）。这个声明产生了一个同名的引用类型，Iter〈T〉。在签名中，in-parameters 和 yield-parameters 是迭代器对方法的 in-parameters 和 out-parameters 的模拟。不同之处在于，方法的输出参数只返回给调用者一次，而迭代器的 yield 参数在迭代器主体执行 yield 时返回。规范的详细信息在 Dafny 语言参考的不同部分中进行了描述。主体由语句组成，就像在方法主体中一样，但也可以使用 yield 语句。

从迭代器客户端的角度来看，iterator 声明可以理解为生成具有各种成员的类Iter〈T〉，下面将描述其简化版本。

`Iter〈T〉类包含一个匿名构造函数，其参数是迭代器的内参数：

predicate Valid()
constructor (in-params)
  modifies this
  ensures Valid()

1
2
3
4

使用 new 和这个匿名构造函数创建了一个迭代器。例如，一个愿意从 start 返回十个连续整数的迭代器可以声明如下：

iterator Gen(start: int) yields (x: int)
{
  var i := 0;
  while i < 10 {
    x := start + i;
    yield;
    i := i + 1;
  }
}

1
2
3
4
5
6
7
8
9

这个迭代器的一个实例是使用以下方法创建的：

iter := new Gen(30);

谓词“Valid()”表示迭代器何时处于可以尝试计算更多元素的状态。它是构造函数的后置条件，出现在“MoveNext”成员的规范中：

method MoveNext() returns (more: bool)
  requires Valid()
  modifies this
  ensures more ==> Valid()

1
2
3
4

请注意，只要 MoveNext 返回 true，迭代器仍然有效。一旦 MoveNext 返回 false，就不能再调用 MoveNext 方法。请注意，客户端没有义务继续调用 MoveNext 直到它返回 false，并且允许迭代器的主体永远保持返回元素。

迭代器的输入参数存储在迭代器类的不可变字段中。为了根据上面的示例进行说明，迭代器类“Gen”包含以下字段：

var start: int;

产量参数也导致迭代器的成员 class:

var x: int;

这些字段由“MoveNext”方法设置。如果 MoveNext 返回 true，则这些字段中提供了最新的收益率值，客户端可以从那里读取它们。

为了帮助编写规范，迭代器类还包含保留“MoveNext”返回值的历史记录的幽灵成员。这些幽灵字段的名称跟在 yield 参数的名称之后，并在名称后面附加了一个“s”（表示复数）。名称检查规则确保这些名称不会引起歧义。因此，上述“Gen”的迭代器类包含：

ghost var xs: seq〈int〉;

这些历史字段由“MoveNext”自动更改，但不能由用户代码分配。

最后，迭代器类包含一些用于规范的特殊字段。特别是，迭代器规范记录在以下不可变字段中：

ghost var _reads: set〈object〉;
ghost var _modifies: set〈object〉;
ghost var _decreases0: T0;
ghost var _decreases1: T1;
// ...

1
2
3
4
5

其中，迭代器的 decreases 子句的每个组件都有一个 _decreases*i*: T*i* 字段。 [6](http://leino.science/papers/krml243.html#fn-fn-iterator -field-names) 另外还有一个字段：

ghost var _new: set〈object〉;

代表迭代器主体分配的任何对象都将添加到其中。迭代器主体可以从 _new 集中删除元素，但不能通过赋值给 _new 添加任何元素。

请注意，在迭代器的前提条件中，即坚持构造迭代器，内参数确实是内参数，而不是 this 的字段。

# 5.5. 异步任务类型

Dafny 中另一个可能会经历一些演变的实验性功能是异步方法。调用异步方法时，它不会返回 out-parameters 的值，而是返回 *async-task 类型 * 的实例。在C类中声明的异步方法，具有以下签名：

async method AM〈T〉(in-params) returns (out-params)

也产生了一个异步任务类型AM〈T〉（在封闭类之外，类型的名称需要限定C.AM〈T〉）。 async-task 类型是一个引用类型，可以理解为一个有各种成员的类，下面介绍它的简化版本。异步方法的每个类型为X的参数x都会产生一个异步任务类型的不可变幽灵字段：

ghost var x: X;

每个Y类型的输出参数y都会产生一个字段

var y: Y;

这些字段会在异步方法成功等待时自动更改，但不能由用户代码分配。

async-task 类型还有一些特殊字段，用于跟踪依赖关系、未完成的任务、新分配的对象等。随着异步方法设计的发展，这些字段将被更详细地描述。

# 6. 函数类型

函数是 Dafny 中的一等值。函数类型具有 (T) -> U 的形式，其中 T 是一个以逗号分隔的类型列表，而 U 是一个类型。 T 被称为函数的 domain type(s) 并且 U 是它的 range type。例如，函数的类型

function F(x: int, b: bool): real

是(int, bool) -> real。参数不允许为ghost。

为了简化函数域由一个类型列表组成的基本情况的外观，在这种情况下可以删除域类型周围的括号，如 T -> U。在一种类型是元组类型的情况下，这种无害的简化需要额外的解释，因为元组类型也是用括号括起来的。如果函数接受一个元组参数，则需要额外的一组括号。例如，函数

function G(pair: (int, bool)): real

类型为 ((int, bool)) -> real。注意必要的双括号。类似地，不带参数的函数与带 0 元组作为参数的函数不同。例如，函数

function NoArgs(): real
function Z(unit: ()): real

1
2

分别有 () -> real 和 (()) -> real 类型。

函数箭头 -> 是右结合的，所以 A -> B -> C 表示 A -> (B -> C)。另一个关联需要显式括号：(A -> B) -> C。

请注意，命名函数的接收器参数不是类型的一部分。相反，它在查找函数时使用，然后可以被认为是被捕获到函数定义中。例如，假设上面的函数“F”在类“C”中声明，而“c”引用了一个“C”类型的对象；那么，以下是正确的类型：

var f: (int, bool) -> real := c.F;

而写如下内容是不正确的：

var f': (C, int, bool) -> real := F;  // not correct

在其类型签名之外，每个函数值都具有三个属性，如下所述。

每个函数都隐含地将堆作为参数。然而，没有任何函数依赖于整个堆。函数的一个属性是它在给定输入所依赖的堆位置集上声明的上限。这让验证者可以确定某些堆修改对某个函数返回的值没有影响。对于函数f: T -> U和T类型的值t，依赖集表示为f.reads(t)并且具有set〈object〉类型。

函数的第二个属性源于每个函数都可能是部分的。换句话说，函数的属性是它的前提条件。对于函数f: T -> U，T类型的参数值t的f的前提条件表示为f.requires(t)并且具有bool类型。

函数的第三个属性更为明显——函数体。对于函数“f: T -> U”，该函数对“T”类型的输入“t”产生的值表示为“f(t)”，并且具有“U”类型。

请注意，f.reads 和 f.requires 本身就是函数。假设 f 的类型为 T -> U，而 t 的类型为 T。那么，f.reads 是 T -> set〈object〉 类型的函数，其 reads 和 requires 属性是：

f.reads.reads(t) == f.reads(t)
f.reads.requires(t) == true

1
2

f.requires 是 T -> bool 类型的函数，其 reads 和 requires 属性为：

f.requires.reads(t) == f.reads(t)
f.requires.requires(t) == true

1
2

# 6.0. Lambda表达式

除了命名函数之外，Dafny 还支持定义函数的表达式。这些被称为 lambda (expression)s（一些语言将它们称为 匿名函数）。 lambda 表达式具有以下形式：

(params) specification => body

其中 *params* 是以逗号分隔的参数声明列表，每个参数声明的形式为 x 或 x: T。参数的类型‘T’在可以推断时可以省略。如果不需要标识符x，可以用“_”代替。如果 *params* 包含一个没有明确类型的参数 x（或 _），则可以删除括号；例如，返回给定整数的后继的函数可以写成以下 lambda 表达式：

x => x + 1

*specification* 是 requires E 或 reads W 的子句列表，其中 E 是布尔表达式， W 是框架表达式。

*body* 是定义函数返回值的表达式。对于满足前提条件的参数的所有可能值，主体必须格式正确（就像命名函数和方法的主体一样）。在某些情况下，这意味着有必要编写明确的 requires 和 reads 子句。例如，lambda 表达式

x requires x != 0 => 100 / x

如果省略 requires 子句，则格式不正确，因为可能会被零除。

在函数不能是部分的并且对读取堆没有限制的设置中，函数 F: T -> U 的 eta 扩展（即，将 F 包装在这样的 lambda 表达式中） lambda 表达式等价于 F) 的方式将写作 x => F(x)。在 Dafny 中，eta 扩展还必须考虑函数的前提条件和读取集，因此 F 的 eta 扩展如下所示：

x requires F.requires(x) reads F.reads(x) => F(x)

# 7. 新类型

可以使用 newtype 声明7 (opens new window) 声明新的数字类型

newtype N = x: M | Q

其中“M”是数字类型，“Q”是布尔表达式，可以将“x”用作自由变量。如果M是一个基于整数的数值类型，那么N也是；如果“M”是实数，那么“N”也是如此。如果可以从 Q 推断出类型 M，则可以省略“:M”。如果 Q 只是 true，那么声明可以简单地给出：

newtype N = M

类型“M”被称为“N”的基本类型。

newtype 是一种数字类型，它支持与其基本类型相同的操作。 newtype 与其他数字类型不同且不兼容；特别是，如果没有显式转换，它就不能分配给它的基本类型。对 newtype 的操作与其基类型的操作之间的一个重要区别是 newtype 操作仅在结果满足谓词 Q 时才被定义，对于 newtype 的字面量也是如此。 [8](http:// /leino.science/papers/krml243.html#fn-fn-newtype-design-question）

例如，假设 lo 和 hi 是基于整数的数字，它们满足 0 <= lo <= hi 并考虑以下代码片段：

var mid := (lo + hi) / 2;

如果 lo 和 hi 的类型为 int，那么代码片段是合法的；特别是，它永远不会溢出，因为 int 没有上限。相反，如果 lo 和 hi 是新类型 int32 的变量，声明如下：

newtype int32 = x | -0x80000000 <= x < 0x80000000

那么代码片段是错误的，因为加法的结果可能无法满足int32定义中的谓词。代码片段可以重写为

var mid := lo + (hi - lo) / 2;

在这种情况下，int 和 int32 都是合法的。

由于 newtype 与其基类型不兼容，并且由于 newtype 操作的所有结果都是 newtype 的成员，因此 Dafny 的编译器可以自由地专门化 newtype 的运行时表示。例如，通过仔细检查上面 int32 的定义，编译器可能会决定在目标硬件中使用带符号的 32 位整数来存储 int32 值。

请注意，Q 中的绑定变量x 的类型为M，而不是N。 n因此，可能无法就“N”值说明“Q”。例如，考虑以下类型的 8 位 2 的补码整数：

newtype int8 = x: int | -128 <= x < 128

并考虑一个类型为int8的变量c。表达式

-128 <= c < 128

定义不明确，因为比较要求每个操作数的类型为“int8”，这意味着文字“128”被检查为“int8”类型，但事实并非如此。编写此表达式的正确方法是在 c 上使用转换操作，如下所述，将其转换为基本类型：

-128 <= int(c) < 128

有一个限制，即值0必须是每个新类型的一部分。9 (opens new window)

# 7.0. 数字转换操作

对于每个数字类型N，都有一个同名的转换函数。它是一个部分恒等函数。它是在给定值（可以是任何数字类型）是转换为的类型的成员时定义的。当从基于实数的数值类型转换为基于整数的数值类型时，该操作要求基于实数的参数没有小数部分。（要将基于实数的数值向下舍入到最接近的整数，请使用 .Trunc 成员，请参阅第 [0.1] 节（http://leino.science/papers/krml243.html#sec-numeric-types）。 )

使用上面的例子来说明，如果 lo 和 hi 的类型是 int32，那么代码片段可以合法地写成如下

var mid := (int(lo) + int(hi)) / 2;

其中mid的类型被推断为int。由于除法的结果值是 int32 类型的成员，因此可以引入另一种转换操作，使 mid 的类型为 int32：

var mid := int32((int(lo) + int(hi)) / 2);

如果编译器确实专门针对int32的运行时表示，那么这些语句的代价是两个或三个运行时转换。

# 8. 子集类型

子集类型是对现有类型的限制使用，称为子集类型的基本类型。子集类型就像基类型和基类型上的谓词的组合使用。

始终允许从子集类型到其基本类型的赋值。如果分配的值确实满足子集类型的谓词，则允许从基本类型到子集类型的另一个方向的分配。（注意，相比之下，newtype 和它的基类型之间的赋值是不允许的，即使赋值是目标类型的值。对于这样的赋值，必须使用显式转换，参见第 [7.0]（http: //leino.science/papers/krml243.html#sec-numeric-conversions)。) Dafny 支持一种子集类型，即内置类型 nat，其基本类型为 int。[10](http: //leino.science/papers/krml243.html#fn-fn-more-subset-types）

类型nat指定int的非负子范围。一个很好地使用子集类型“nat”的简单示例是标准斐波那契函数：

function Fib(n: nat): nat
{
  if n < 2 then n else Fib(n-2) + Fib(n-1)
}

1
2
3
4

此函数的等效但笨拙的公式（以调用站点产生的任何错误消息的措辞为模）将使用类型int并在前置条件和后置条件中编写限制谓词：

function Fib(n: int): int
  requires 0 <= n  // the function argument must be non-negative
  ensures 0 <= Fib(n)  // the function result is non-negative
{
  if n < 2 then n else Fib(n-2) + Fib(n-1)
}

1
2
3
4
5
6

类型推断永远不会将变量的类型推断为子集类型。相反，它会将类型推断为子集类型的基本类型。例如，x 的类型

forall x :: P(x)

将是 int，即使谓词 P 声明其参数的类型为 nat。

# 参考资料

由于 Nadia Polikarpova 和 Paqui Lucio 的评论，本文档得到了改进。

支持平等只是人们可以想象的丰富类型系统中的类型拥有的众多模式之一。例如，其他模式可能包括具有总订单、可零初始化以及可能无人居住。如果 Dafny 将来支持更多模式，“( )”后缀语法可能会被扩展。目前，后缀只能表示支持平等的模式。 ↩ (opens new window)
现在Dafny支持内置元组，打算把序列切片操作改成返回不是子序列的序列，而是子序列的元组。 ↩ (opens new window)
这可能会在未来发生变化，不允许多次出现相同的键。 ↩ (opens new window)
这在未来可能会改变如下：in和!in 地图将不再支持操作。相反，对于任何地图 m，m.Domain 将返回其域作为一个集合，而 m.Range 将返回，也作为一个集合，在其域下的 m 的图像。 ↩ (opens new window)
这将在 Dafny 的未来版本中发生变化，它将同时支持可空和（默认情况下）非 -null 引用类型。 ↩ (opens new window)
很快，object 将成为一个内置的 trait 而不是内置的特殊班级。发生这种情况时，将不再可能执行“新对象”。 object 不能用作类型参数的当前编译器限制也将消失。 ↩ (opens new window)
将特殊字段_reads和_modifies重命名为相同是有意义的名称作为相应的关键字，“读取”和“修改”，就像对函数值所做的那样。此外，各种 _decreases*i* 字段可以组合成一个名为 decreases 的字段，其类型是 n 元组。 ↩ (opens new window)
是否应该将newtype重命名为numtype？ ↩ (opens new window)
自动定义“谓词N”有用吗？(m:M){Q} `? ↩ (opens new window)
限制是由于当前编译器的限制。这将在未来发生变化，也将为子集类型和非空引用类型开辟可能性。 ↩ (opens new window)
Dafny 的未来版本将支持用户定义的子集类型。 ↩ (opens new window)

编辑

上次更新: 2022/03/26, 19:35:15

← 在集合上迭代 Style Guide for Dafny programs→

Dafny type system

# Dafny Type System

# 0. 基本类型

# 0.0. Booleans

# 0.1. 数字类型

# 0.2. 字符

# 1. 类型参数

# 2. 集合类型

# 2.0. 集合

# 2.1. Multisets

# 2.2. 序列

# 2.2.0. 字符串

# 2.3. 有限与无限图

# 3. 象征类型

# 3.0. 同义词类型

# 3.1. 不透明类型

# 4. 数据类型

# 4.0. 归纳类型

# 4.1. 元组类型

# 4.2. 共同归纳类型

# 5. 参照类型

# 5.0. 类

# 5.1. 数组

# 5.1.0. 一维数组

# 5.1.1. 多维数组

# 5.2. 特征

# 5.3. 类型 object

# 5.4. 迭代器类型

# 5.5. 异步任务类型

# 6. 函数类型

# 6.0. Lambda表达式

# 7. 新类型

# 7.0. 数字转换操作

# 8. 子集类型

# 参考资料

# 5.3. 类型 `object`