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

Я реализовал одно веб-приложение .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. Есть ли способ вызвать функцию calculate (cal: Calculation) без необходимости создавать новый объект Calculation и напрямую включать один «дочерний тип» (Calculation_Sum, Calculation_Rest и т. д.)?

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

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

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

Стоит ли изучать PHP в 2023-2024 годах?
Стоит ли изучать PHP в 2023-2024 годах?
Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.
Приемы CSS-макетирования - floats и Flexbox
Приемы CSS-макетирования - floats и Flexbox
Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...
Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest
В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...
Концепция локализации и ее применение в приложениях React ⚡️
Концепция локализации и ее применение в приложениях React ⚡️
Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...
Пользовательский скаляр GraphQL
Пользовательский скаляр GraphQL
Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
1
0
172
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

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

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 для хранения вашего byteStoredUsing16Bitstype. Без атрибута :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 также должны соответствовать указанному вами предикату.

Рустан

Другие вопросы по теме