【发布时间】：2018-12-18 14:56:07
【问题描述】：
我实现了一个 .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 会自动创建一些类：Calculation、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 对象并直接包含一个“子类型”（Calculation_Sum、Calculation_Rest 等）？
可以 _0_DafnyCalculation_Compile.__default。可以避免吗？
是否需要导入 System.Numerics 并使用 BigInteger 转换 C# int 和 Dafny int？还是可以用其他方式完成？
提前谢谢你。我试图说明和清楚，如果任何部分无法理解，请随时与我联系。
【问题讨论】：
标签： c# hierarchy implementation dafny