Я реализовал одно веб-приложение .Net, которое использует библиотеку .dll, полностью проверенную в Dafny. Он работает хорошо, и общение с библиотекой несложно. Это чудесно.
К сожалению, некоторые части кода кажутся некрасивыми, и я хотел бы спросить, правильно ли я использовал библиотеку или это правильный способ ее использования. Я говорю о типах данных. Я включил простой пример, чтобы задавать вопросы.
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 с различными параметрами. Я использую dll в консольном приложении C# следующим образом:
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 .__ по умолчанию. избегать?
Нужно ли импортировать System.Numerics и использовать BigInteger для преобразования C# int и Dafny int? или можно по-другому?
Заранее благодарю. Я старался быть иллюстративным и ясным, если какая-либо часть непонятна, не стесняйтесь обращаться ко мне.
Спасибо за вопросы.
1) Да, теперь есть. Сегодня я проверил изменения в компиляторе, который позволяет писать
Calculation.create_Sum(A, B)
вместо предыдущего
new Calculation(new Calculation_Sum(A, B))
Если ваш тип данных имеет параметры типа, они идут сразу после имени типа.
2) Вы можете избежать искаженных имен, таких как _0_DafnyCalculation_Compile
, предоставив свои собственные через {:extern YourNameGoesHere}
, которые можно разместить в объявлениях, таких как модули, классы и методы. (Если некоторые объявления не поддерживают :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-битному целому числу со знаком (записанному int
на C#) и будет поэтому скомпилируйте ваш Dafny type int32
в C# int
. Это работает для всех целочисленных типов .NET.
Если по какой-то причине вы хотите использовать собственный целочисленный тип большего размера, чем позволяет ваш диапазон, вы можете указать, что вы хотите, с помощью атрибута :nativeType
. Например,
newtype {:nativeType "short"} byteStoredUsing16Bits = x | -128 <= x < 128
будет использовать .NET short
для хранения вашего byteStoredUsing16Bits
type. Без атрибута :nativeType
компилятор Dafny выбрал бы тип .NET sbyte
для byteStoredUsing16Bits
.
Вы также можете использовать {:nativeType false}
с newtype
, чтобы сказать, что вы не хотите, чтобы компилятор использовал родное целое число (вместо этого используйте BigInteger
как обычно).
Обратите внимание, что объявление newtype
позволяет вам определять ваши собственные целочисленные типы, но они несовместимы со стандартным int
Dafny. Основная причина использования 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
также должны соответствовать указанному вами предикату.
Рустан