Dafny 如何在 C# 及其层次结构中实现数据类型？

Question

我实现了一个 .Net Web 应用程序，它使用在 Dafny 中完全验证的 .dll 库。它运作良好，与图书馆的沟通并不困难。这真是棒极了。

不幸的是，有些部分代码看起来不太好，我想问一下是我没有很好地使用这个库还是使用它的正确方法。我说的是数据类型。为了提出问题，我提供了一个简单的示例。

module DafnyCalculation
{
    datatype Calculation = Sum(s1:int, s2:int) | Rest(r1:int, r2:int) 
                        | Mult(m1:int, m2:int) | Div (d1:int, d2:int)

    function method calculate(cal:Calculation): int
    {
        match cal
            case Sum(s1,s2) => s1+s2
            case Rest(r1,r2) => r1-r2
            case Mult(m1,m2) => m1*m2
            case Div(d1,d2) => 
                if(d2!=0) then d1/d2 
                else d1
    }
}

由于数据类型有多个构造函数，生成.dll时dafny会自动创建一些类：计算，Base_Calculation，Calculation_Sum，Calculation_Rest，Calculation_Mult 和 Calculation_Div 具有不同的参数。我在 C# 控制台应用程序中按以下方式使用 dll：

int result;
Base_Calculation cal;
Console.WriteLine("Enter first number: "); int x = int.Parse(Console.ReadLine());
Console.WriteLine("Enter second number: "); int y = int.Parse(Console.ReadLine());
Console.WriteLine("Choose operator:\n1)Sum\n2)Rest\n3)Mult\n4)Div\nOperator: "); 
int op = int.Parse(Console.ReadLine());
switch (op)
{
    case 1:
        cal = new Calculation_Sum((BigInteger)x, (BigInteger)y);
        break;
    case 2:
        cal = new Calculation_Rest((BigInteger)x, (BigInteger)y);
        break;
    case 3:
        cal = new Calculation_Mult((BigInteger)x, (BigInteger)y);
        break; 
    case 4 :
        cal = new Calculation_Div((BigInteger)x, (BigInteger)y);
        break;
    default:
        throw new Exception("Wrong option");
}
result = (int) _0_DafnyCalculation_Compile.__default.calculate(new Calculation(cal));
Console.WriteLine("Result: {0}", result);
Console.ReadLine();

我有一些基于示例的问题：

有没有什么方法可以调用函数 calculate(cal:Calculation) 而不必构造一个新的 Calculation 对象并直接包含一个 "child-types" (Calculation_Sum, Calculation_Rest, 等等)?
可以_0_DafnyCalculation_Compile.__default。避免？
是否需要导入System.Numerics并使用BigInteger来转换C# int和Dafny int？或者可以用其他方式完成吗？

在此先感谢您。我尽量做到说明和清楚，如果有任何不明白的地方，请随时与我联系。

Answer 1

感谢您的提问。

1) 是的，现在有了。今天，我检查了对编译器的更改，它允许您编写

Calculation.create_Sum(A, B)

代替之前的

new Calculation(new Calculation_Sum(A, B))

如果您的数据类型有类型参数，它们紧跟在类型名称之后。

2) 您可以通过 {:extern YourNameGoesHere} 提供您自己的名称，从而避免像 _0_DafnyCalculation_Compile 这样的错位名称，这些名称可以放在模块、类和方法等声明中。（如果某些声明在您需要的地方不支持 :extern，请将其作为错误提交。）

(我最近一直在研究一些编译器的变化。在很多情况下，我可能会自动删除 _0_ 前缀或 _Compile 后缀。我们会看到.)

3) 如果你使用 Dafny 的类型 int，那么你必须像你提到的那样使用 BigInteger。但是如果你想使用原生整数类型，你可以在 Dafny 中声明你自己的整数类型。例如，

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

声明一个 Dafny 类型 int32，其值在给定范围内。（在此示例中，x 被推断为 int 类型，但您也可以显式指定类型，如 newtype int32 = x: int | ...。）Dafny 编译器注意到此范围适合带符号的32 位整数（在 C# 中写成 int），因此会将 Dafny 类型 int32 编译成 C# 的 int。这适用于所有本机 .NET 整数类型。

如果出于某种原因您想使用比您的范围允许的更大的本机整数类型，那么您可以使用 :nativeType 属性指明您想要的。例如，

newtype {:nativeType "short"} byteStoredUsing16Bits = x | -128 <= x < 128

将使用 .NET short 来存储您的 byteStoredUsing16Bits 类型。如果没有 :nativeType 属性，Dafny 编译器将为 byteStoredUsing16Bits.

选择 .NET 类型 sbyte

您还可以使用 {:nativeType false} 和 newtype 来表示您不希望编译器使用本机整数（而是像往常一样使用 BigInteger）。

请注意，newtype 声明允许您定义自己的整数类型，但这些与 Dafny 的标准 int 不兼容。使用 newtype 而不是声明子集类型（通过使用关键字 type 而不是 newtype）的主要原因是允许编译器使用不同的表示。如果需要在各种整数类型之间进行转换，请使用 as 运算符。以下代码片段说明：

var x: int := 70;
var y: int32 := x as int32;
var z: byteStoredUsing16Bits := y as byteStoredUsing16Bits;
x := z as int;

在数学上，他 as 运算符是一个偏恒等函数。也就是说，as 永远不会更改值，验证器将检查您的转换是否来自目标类型中存在的值。（作为练习，将示例中的 70 更改为 700 并观察验证者的抱怨。）

此外，请注意 newtype 类型的所有中间表达式也必须遵守您指定的任何谓词。

鲁斯坦

Dafny 如何在 C# 及其层次结构中实现数据类型？

How does Dafny implement datatypes in C# and their hierarchy?

c#

implementation

hierarchy

dafny