Отсутствует ссылка на сборку при использовании класса

Question

У меня есть следующий код

class clazz
{
    constructor {:axiom} () requires true

    method su(x: int, y:int) returns (r: int) 
    {
       r := x + y;
    }
}

method {:main} Main() {
   var c := new clazz();
   var s := c.su(2,3);
   print(s);
}

Как можно использовать класс clazz?Это конкретная ошибка:

error CS1061: Type `__default.ClassRoomExample' does not contain a definition for `__ctor'and no extension method `__ctor' of type `__default.ClassRoomExample' could be found. Are you missing an assembly reference?

Answer 1

Обычно компилятор Dafny будет жаловаться, что вы объявили что-то без тела, в данном случае конструктор без тела.Но вы пометили свой конструктор {:axiom}, что говорит компилятору о том, что вы намеренно ушли из тела.Вот почему эта ошибка возникает из-за компилятора C #, а не компилятора Dafny.

Необычный атрибут {:axiom} был разработан для лемм без тела.Если вы действительно хотите опустить код для конструктора или метода, вы, вероятно, захотите использовать вместо него атрибут :extern, который позволит вам реализовать метод на другом языке .NET.

Answer 2

Я только что понял проблему.отсутствует { } в конструкторе.Тупой.