基础学习

提示

​ 此页面说明了 Dafny 中许多最常见的语言功能。 为了让您更快上手，这里的描述被简化了——这个页面不是语言参考。例如，此页面不会涉及模块、迭代器或细化，除非您在 Dafny 中编写更大或更高级的程序，否则您将不需要这些。

Dafny是什么样？

Dafny程序长这样：xxxxx.dfy，Dafny文件是以.dfy结尾的。

程序主要包含以下几部分：

1. 类型(types)

2. 方法(methods)

3. 函数(functions)

4. 用户自定义的类型包括类（class）和归纳数据类型(inductive class)

5. 类class本身也包含一组声明(declarations)、介绍字段（introducing fields）、方法(methods)和函数(functions)。

   如果有main方法那就从main开始验证程序，没有也没关系，main不是必须的。

注释：// 双斜杠 或者 /* xxxxx */

基本定义

在类中，定义字段x为数据类型(types)T：

var x: T

注意事项：

• 数据类型必需手动申明的，不会被自动推断。

• 通过在声明前加上关键 ghost 可以将该字段声明为幽灵（即用于规范而不是执行）字段。

Dafny 的9种数据类型包括：

• bool：布尔值
• int：无界整数
• string: 字符串
• class/inductive class: 用户自定义的类和归纳类、
• set<T>：不可变的无序集合
• seq<T>：不可变的有序集合
• array<T>、array2<T>、array3<T>: 多维数组类型
• object：所有类型的超类
• nat：范围是int一半，非负整数。