Style Guide for Dafny Programmers

Dafny 文档 (opens new window)

• 命名约定
  • 方法前缀 (opens new window)
• 代码布局
  • Braces (opens new window)
  • Imports (opens new window)
• 缩进和换行
  • 制表符还是空格？ (opens new window)
  • 最大字符限制 (opens new window)
  • 换行符 (opens new window)
  • 函数、方法、谓词和引理 (opens new window)
• 需要避免的事情
  • 括号 (opens new window)
  • 空格
    • 类型声明 (opens new window)
    • 函数、方法、谓词和引理声明 (opens new window)
• 建议
  • Externs (opens new window)
  • 需要考虑的事项 (opens new window)

本样式指南提供了 Dafny 代码的编码约定。

此文档仍在进行中。 请随时添加更多建议。

命名约定

任何变量都以camelCase命名。

var minValue := 1;
var cipherMessage := "Hello World";

任何引理、谓词、函数、方法、类、模块、数据类型和新类型都以PascalCase命名。

method FindIndex(arr: seq<int>, k: int)
    ...

任何静态或全局 常量 都以 UPPERCASE_WITH_UNDERSCORES 命名。

static const MONTHS_IN_A_YEAR := 12

前缀方法

当变量或方法位于类/模块中时，避免使用冗余名称。

class Integer {

    // The following method converts the given integer
    // to a string.
    //
    // this method name can be simplified to ToString()
    // so that the method call is Integer.ToString(i)
    // instead of Integer.IntegerToString(i).

    // YES
    method ToString(i: int) returns (s: string)
        ...

    // NO
    method IntegerToString(i: int) returns (s: string)
        ...
}

代码布局

Braces

默认情况下，左大括号在同一行。

module M {
    ...
    method Met() {
        ...
    }
}

如果方法（或函数、引理等）签名太长而不能放在一行中，或者如果签名至少有一个规范子句，则左大括号将换行。

module M {
    ...
    method Met(i: int) returns (j: int)
        requires i % 2 == 0
        ensures j > 10
    {
        ...
    }
}

这适用于每个范围：module、class、predicate、if、while 等等。

Imports

默认情况下，导入模块而不打开它们。

import Coffee
...

但是，如果某个模块的某些成员非常频繁地使用，请使用 opened 导入它：

import opened Donut
...

当一个文件使用两个模块并且它们都定义同名的方法时，不要将它们导入 opened。

import MyModule
import YourModule
...
method MyMethod() {
    MyModule.foo();
    YourModule.foo();
}

在这种情况下，如果要缩短模块名称，请使用简写名称导入。

import M = MyModuleWithACumbersomeName
import Y = YourModuleWithACumbersomeName
...
method MyMethod() {
    M.foo();
    Y.foo();
}

常见的导入，例如 StandardLibrary 和 Native，应该组合在一起，然后是自定义模块导入，中间有一个空行。

import opened StandardLibrary
import opened Native

import opened Donut
import Coffee

虽然不是必需的，但建议保持 imports 和 includes 的字母顺序，除非将它们按逻辑分组更有意义。

缩进和换行

制表符还是空格?

空格优于制表符。 选项卡只能用于与包含选项卡的现有代码保持一致。

每个缩进使用 2 个空格。

最大字符限制

虽然没有特别的严格要求，但一般建议每行最多 120 个字符。

换行符

在连续的函数、方法、谓词和引理之间使用换行符，提高代码可读性。

以换行符结束每个文件。

函数、方法、谓词和引理

每个 Dafny 方法都有以下签名。

method {:<attributes>} MethodName(param1: Type, param2: Type) returns (ret: Type)
    requires P()
    modifies param2
    ensures Q()
    decreases param1

如果可能，将 MethodName 和 returns 语句放在同一行，因为关键字 returns 与其他方法规范子句不同，例如 requires、modifies、ensures 和 decreases ，应该按这个顺序出现。 每个方法规范子句应该在单独的行上，缩进。

如果 Method 签名太长，我们可以将其分解。

method {:<attributes>} MethodName(param1: Type, param2: Type,
        param3: Type, param4: Type, param5: Type)
    returns (ret1: Type, ret2: Type, ret3: Type, ret4: Type,
        ret5: Type)
    requires P1()
    requires P2()
    requires P3()
    modifies param2
    modifies param3
    ensures Q1()
    ensures Q2()
    decreases param1

多个 requires 或 ensures 可以合并为一个：

requires
    && P1()
    && P2()
    && P3()

相同的规则适用于 function、predicate 和 lemma 定义。

需要避免的事情

括号

在许多情况下，Dafny 不需要在表达式周围加上括号。 这里有些例子。

• If-Else-While 语句

// YES
var i := 1;
while i < 10 {
    ...
    if 1 < i {
        ...
    }
    ...
}

// NO
var i := 1;
while (i < 10) {
    ...
    if (1 < i) {
        ...
    }
    ...
}

• 带有表达式参数的语句

// YES
assert x < 100;
print x;

// NO
assert(x < 100);
print(x);

• 简单的布尔/算术表达式

// YES
method Collatz(num: nat)
    decreases *
{
    var n := num;
    while 1 < n
        decreases *
    {
        n := if n % 2 == 0 then n / 2 else n * 3 + 1;
    }
}

// NO
method Collatz(num: nat)
    decreases *
{
    var n := num;
    while (1 < n) // unnecessary parentheses
        decreases *
    {
        n := if ((n % 2) == 0) then (n / 2) else ((n * 3) + 1); // unnecessary parentheses
    }
}

空格

避免表达式中不必要的空格。

类型声明

类型声明应该具有variableName: variableType的形式。

// YES
const one: int := 1
class {:extern} Util {
    var {:extern} Exception: System.String
}

// NO
const one : int := 1 // unnecessary whitespace
class {:extern} Util {
    var {:extern} Exception : System.String // unnecessary whitespace
}

如果 Dafny 可以推断出该类型，请将其省略，除非您认为它在程序中提供了有用的文档。 所以，上面的常量 one 最好声明为

const one := 1

函数、方法、谓词和引理声明

function、method、predicate 和 lemma 定义应该具有 FunctionName(parameterName: parameterType, ...) 的形式。

// YES
function method Foo<int>(i: int): int

// NO
function method Foo<int> (i : int) : int // unnecessary whitespace

Avoid too little or too much whitespace that reduces the overall readability.

// YES
lemma MyLemma<A, B>(x: seq<seq<A>>, y: B) {
    ...
}

// NO
lemma MyLemma <A,B> ( x : seq<seq<A>> , y :B){
    ...
}

建议

本节描述了一些建议，这些建议可以帮助使代码更具可读性和易于遵循，尽管没有严格执行。

Externs

尽可能在 Dafny 和目标语言（例如 C#、Java 等）中将它们命名为相同的名称，这样在 Dafny 中我们只需编写 {:extern}，而不是 {:extern "<name>"}。

需要考虑的事项

在 Dafny 中设计/实施程序之前思考这些问题。

• 这个变量名/函数名X是个好名字吗？
• 这个方法M在模块X中有意义吗？ 它不应该在模块 Y 中吗？
• 定义X是否属于文件Y.dfy？
• X.dfy 是一个好的文件名吗？