Как Dafny реализует типы данных в C # и их иерархию? - PullRequest
Новая
       13

Как Dafny реализует типы данных в C # и их иерархию?

0 голосов
/ 18 декабря 2018

Я реализовал одно веб-приложение .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();

У меня есть несколько вопросов на основе примера:

  1. Есть ли способ позвонитьли выполнять функцию вычисления (cal: Calculation) без необходимости создания нового объекта Calculation и включения непосредственно одного «дочернего типа» (Calculation_Sum, Calculation_Rest и т. д.)?

  2. Может _0_DafnyCalculation_Compile .__ по умолчанию.следует избегать?

  3. Необходимо ли импортировать System.Numerics и использовать BigInteger для приведения C # int и Dafny int?или это можно сделать другим способом?

Спасибо заранее.Я старался быть наглядным и понятным, если какая-то часть не понятна, не стесняйтесь обращаться ко мне.

1 Ответ

0 голосов
/ 16 февраля 2019

Спасибо за ваши вопросы.

1) Да, есть сейчас.Сегодня я зарегистрировал изменение в компиляторе, которое позволяет писать 

Calculation.create_Sum(A, B)

вместо предыдущего 

new Calculation(new Calculation_Sum(A, B))

Если тип данных имеет параметры типа, они идут сразу после имени типа.

2) Вы можете избежать искаженных имен, таких как _0_DafnyCalculation_Compile, предоставив свои собственные через {:extern YourNameGoesHere}, которые можно размещать в объявлениях, таких как модули, классы и методы.(Если некоторые объявления не поддерживают :extern там, где вам это нужно, пожалуйста, сообщите об этом как об ошибке.)

(В последнее время я работал над некоторыми изменениями компилятора. Возможно, я смогуво многих случаях автоматически удаляем префикс _0_ или суффикс _Compile. Посмотрим.)

3) Если вы используете тип Дафни int, то вы должны использовать BigInteger какупоминается.Но если вы хотите использовать собственные целочисленные типы, вы можете объявить свои собственные целочисленные типы в Dafny.Например, 

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

объявляет тип Дафни int32, значения которого находятся в данном диапазоне.(В этом примере x подразумевается как тип int, но вы также можете явно указать тип, например newtype int32 = x: int | ....) Компилятор Dafny замечает, что этот диапазон помещается в 32-разрядное целое число со знаком (записываетсяint в C #) и, следовательно, скомпилирует ваш тип Dafny int32 в C # int.Это работает для всех собственных целочисленных типов .NET.

Если по какой-то причине вы хотите использовать больший собственный целочисленный тип, чем позволяет ваш диапазон, то вы можете указать, что вы хотите, с помощью атрибута :nativeType.Например, 

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

будет использовать .NET short для хранения вашего типа byteStoredUsing16Bits.Без атрибута :nativeType компилятор Dafny выберет тип .NET sbyte для byteStoredUsing16Bits.

Вы также можете использовать {:nativeType false} с newtype, чтобы сказать, что вы не хотитекомпилятор должен использовать собственное целое число (но вместо этого использовать BigInteger как обычно).

Обратите внимание, что объявление newtype позволяет вам определять ваши собственные целочисленные типы, но они несовместимы со стандартом Дафни 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 должны также соответствовать любому предикатууказать.

Растан

...