У меня есть следующий код
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?
Где описаны классы?
Я только что понял проблему. отсутствует { }
в конструкторе. Тупой.
Обычно компилятор Dafny будет жаловаться, что вы объявили что-то без тела, в данном случае конструктор без тела. Но вы пометили свой конструктор с помощью {:axiom}
, который сообщает компилятору, что вы намеренно оставили его вне тела. Вот почему ошибка, которую вы видите, исходит от компилятора C#, а не от компилятора Dafny.
Атрибут {:axiom}
, который встречается редко, был разработан для лемм без тела. Если вы действительно хотите опустить код для конструктора или метода, вы, вероятно, захотите вместо этого использовать атрибут :extern
, который позволяет реализовать метод на другом языке .NET.
это похоже на ошибку C#?